Documentation

Mathlib.Tactic.SuppressCompilation

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

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

    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

      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

        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
        Instances For