Commands to assert and check the (non-)existence of declarations or imports

These commands can be used to enforce the independence of different parts of a library.

• #import_path Foo prints the transitive import chain that brings Foo into scope.
• assert_not_exists Foo fails if Foo is in scope (used for dependency management).
• assert_not_imported Module fails if Module is transitively imported.
• #check_assertions verifies that all asserted declarations/modules eventually exist.

def Lean.Environment.importPath (env : Environment) (imported : Name) : Array Name

Find the dependency chain, starting at a module that imports imported, and ends with the current module.

The path only contains the intermediate steps: it excludes imported and the current module.

Equations

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

structure Lean.Elab.Command.AssertExists : Type

AssertExists is the structure that carries the data to check whether a declaration or an import is meant to exist somewhere in a library.

• isDecl : Bool

  The type of the assertion: true means declaration, false means import.

• givenName : Name

  The fully qualified name of a declaration that is expected to exist.

• modName : Name

  The name of the module where the assertion was made.

def Lean.Elab.Command.instBEqAssertExists.beq : AssertExists → AssertExists → Bool

Equations

• Lean.Elab.Command.instBEqAssertExists.beq { isDecl := a, givenName := a_1, modName := a_2 } { isDecl := b, givenName := b_1, modName := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Elab.Command.instBEqAssertExists.beq x✝¹ x✝ = false

instance Lean.Elab.Command.instBEqAssertExists : BEq AssertExists

Equations

• Lean.Elab.Command.instBEqAssertExists = { beq := Lean.Elab.Command.instBEqAssertExists.beq }

instance Lean.Elab.Command.instHashableAssertExists : Hashable AssertExists

Equations

• Lean.Elab.Command.instHashableAssertExists = { hash := Lean.Elab.Command.instHashableAssertExists.hash }

def Lean.Elab.Command.instHashableAssertExists.hash : AssertExists → UInt64

Equations

• Lean.Elab.Command.instHashableAssertExists.hash { isDecl := a, givenName := a_1, modName := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

opaque Lean.Elab.Command.assertExistsExt : SimplePersistentEnvExtension AssertExists (Std.HashSet AssertExists)

Defines the assertExistsExt extension for adding a HashSet of AssertExists entries to the environment.

def Lean.Elab.Command.addAssertExistsEntry (isDecl : Bool) (declName mod : Name) : CommandElabM Unit

addAssertExistsEntry isDecl declName mod extends the AssertExists environment extension with the data isDecl, declName, mod. This information is used to capture declarations and modules that are forbidden from existing/being imported at some point, but should eventually exist/be imported.

Equations

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

def Lean.Elab.Command.getSortedAssertExists (env : Environment) : Array AssertExists

getSortedAssertExists env returns the array of AssertExists, placing first all declarations, in alphabetical order, and then all modules, also in alphabetical order.

Equations

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

def Lean.Elab.Command.importPathMessage (env : Environment) (idx : ModuleIdx) : MessageData

importPathMessage env idx produces a message laying out an import chain from idx to the current module. The output is of the form

Lean.Init,
  which is imported by Lean.Elab.Command,
  which is imported by Lean.Elab.AssertExists,
  which is imported by this file.

if env is an Environment and idx is the module index of Lean.Init.

Equations

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

def Lean.Elab.Command.elabImportPath : CommandElab

#import_path Foo prints the transitive import chain that brings the declaration Foo into the current file's scope.

This is useful for understanding why a particular declaration is available, especially when debugging unexpected dependencies.

Equations

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

def Lean.Elab.Command.elabAssertNotExists : CommandElab

assert_not_exists d₁ d₂ ... dₙ is a command that asserts that the declarations named d₁ d₂ ... dₙ do not exist in the current import scope.

Be careful to use names (e.g. Rat) rather than notations (e.g. ℚ).

It may be used (sparingly!) to enforce plans that certain files are independent of each other.

If you encounter an error on an assert_not_exists command while developing a library, it is probably because you have introduced new import dependencies to a file. In this case, you should refactor your work (for example by creating new files rather than adding imports to existing files). You should not delete the assert_not_exists statement without careful discussion ahead of time.

assert_not_exists statements should generally live at the top of the file, after the module doc.

Equations

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

def Lean.Elab.Command.elabAssertNotImported : CommandElab

assert_not_imported m₁ m₂ ... mₙ checks that each one of the modules m₁ m₂ ... mₙ is not among the transitive imports of the current file.

The command does not currently check whether the modules m₁ m₂ ... mₙ actually exist.

Equations

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

def Lean.Elab.Command.elabCheckAssertions : CommandElab

#check_assertions retrieves all declarations and all imports that were declared not to exist so far (including in transitively imported files) and reports their current status:

• ✓ means the declaration or import exists,
• × means the declaration or import does not exist.

This means that the expectation is that all checks succeed by the time #check_assertions is used, typically once all of the library has been built.

If all declarations and imports are available when #check_assertions is used, then the command logs an info message. Otherwise, it emits a warning.

The variant #check_assertions! only prints declarations/imports that are not present in the environment. In particular, it is silent if everything is imported, making it useful for testing.

Equations

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