# Suppressing 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 https://github.com/leanprover-community/mathlib4/issues/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.

source
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 https://github.com/leanprover-community/mathlib4/issues/7103.

Equations

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

Instances For

source
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.

Instances For

source
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.

Instances For

source
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 https://github.com/leanprover-community/mathlib4/issues/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")

Instances For