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