The linter for sorry declarations and the sorryful attribute

This module defines an attribute sorryful and a linter noSorry.

The attribute sorryful adds the declaration to an environment extension sorryfulExtension which can be used to create TODO entries.

The linter noSorry checks for declarations that contain the sorryAx axiom if and only if it has the sorryful attribute.

Coloring sorryful

It is possible to color the sorryful attribute in VSCode. This is part of the .vscode/settings.json file, but requires the TODO Highlight extension to be downloaded.

The sorryful environment extension

structure SorryfulInfo : Type

The information for stored for a decleration marked with sorryful.

• name : Lean.Name

  Name of result.

• docstring : String

  The docstring of the result.

• fileName : Lean.Name

  The file name where the note came from.

• line : Nat

  The line from where the note came from.

opaque sorryfulExtension : Lean.SimplePersistentEnvExtension SorryfulInfo (Array SorryfulInfo)

An enviroment extension containing the information of declerations which carry the sorryful attribute.

def addSorryfulEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) (docString : String) (fileName : Lean.Name) (line : Nat) : m Unit

Adds an entry to sorryfulExtension.

Equations

• One or more equations did not get rendered due to their size.

The psudo environment extension

structure PseudoInfo : Type

The information for stored for a decleration marked with pseudo.

• name : Lean.Name

  Name of result.

opaque pseudoExtension : Lean.SimplePersistentEnvExtension PseudoInfo (Array PseudoInfo)

An enviroment extension containing the information of declerations which carry the pseudo attribute.

def addPseudofulEntry {m : Type → Type} [Lean.MonadEnv m] (declName : Lean.Name) : m Unit

Adds an entry to pseudoExtension.

Equations

• addPseudofulEntry declName = Lean.modifyEnv fun (x : Lean.Environment) => Lean.PersistentEnvExtension.addEntry pseudoExtension x { name := declName }

The sorryful attribute

def Sorryful_attr : Lean.ParserDescr

The sorryful attribute allows declerations to contain the sorryAx axiom. In converse, a decleration with the sorryful attribute must contain the sorryAx axiom.

Equations

• Sorryful_attr = Lean.ParserDescr.node `Sorryful_attr 1024 (Lean.ParserDescr.nonReservedSymbol "sorryful" false)

The pseudo attribute

def Pseudo_attr : Lean.ParserDescr

The pseudo attribute allows declerations to contain the Lean.ofReduceBool axiom. In converse, a decleration with the pseudo attribute must contain the Lean.ofReduceBool axiom.

Equations

• Pseudo_attr = Lean.ParserDescr.node `Pseudo_attr 1024 (Lean.ParserDescr.nonReservedSymbol "pseudo" false)

The noSorry linter

def PhysLean.Linter.noSorry : Batteries.Tactic.Lint.Linter

The noSorry linter. This checks the following:

• A declaration contains the sorryAx axiom if and only if it has the sorryful attribute.
• A declaration contains the Lean.ofReduceBool axiom if and only if it has the pseudo attribute.

Equations

• One or more equations did not get rendered due to their size.