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
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.
Instances For
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
- commandSuppress_compilation = Lean.ParserDescr.node `commandSuppress_compilation 1024 (Lean.ParserDescr.symbol "suppress_compilation")