Supressing compilation to executable code in a file or in a section

Currently, the compiler may spend a lot of time trying to produce executable code for complicated definitions. This is a waste of resources for definitions in area of mathematics that will never lead to executable code. The command suppress_compilation is a hack to disable code generation on all definitions (in a section or in a whole file). See the issue mathlib4#7103

To compile a definition even when suppress_compilation is active, use unsuppress_compilation in def foo : .... This is activated by default on notations to make sure that they work properly.

Note that suppress_compilation does not work with notation3. You need to prefix such a notation declaration with unsuppress_compilation if suppress_compilation is active.

def elabSuppressCompilationDecl : Lean.Elab.Command.CommandElab

Replacing def and instance by noncomputable def and noncomputable instance, designed to disable the compiler in a given file or a given section. This is a hack to work around mathlib4#7103.

Equations

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

def commandUnsuppress_compilationIn_ : Lean.ParserDescr

The command unsuppress_compilation in def foo : ... makes sure that the definition is compiled to executable code, even if suppress_compilation is active.

Equations

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

def expandSuppressCompilationNotation : Lean.Macro

Make sure that notations are compiled, even if suppress_compilation is active, by prepending them with unsuppress_compilation.

Equations

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

def commandSuppress_compilation : Lean.ParserDescr

Replacing def and instance by noncomputable def and noncomputable instance, designed to disable the compiler in a given file or a given section. This is a hack to work around mathlib4#7103. Note that it does not work with notation3. You need to prefix such a notation declaration with unsuppress_compilation if suppress_compilation is active.

Equations

• commandSuppress_compilation = Lean.ParserDescr.node `commandSuppress_compilation 1024 (Lean.ParserDescr.symbol "suppress_compilation")