Documentation

Lake.DSL.Targets

DSL for Targets & Facets #

Macros for declaring Lake targets and facets.

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

    Facet Declarations #

    Define a new module facet. Has one form:

    module_facet «facet-name» (mod : Module) : α :=
      /- build term of type `IndexBuildM (BuildJob α)` -/
    

    The mod parameter (and its type specifier) is optional.

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

      Define a new package facet. Has one form:

      package_facet «facet-name» (pkg : Package) : α :=
        /- build term of type `IndexBuildM (BuildJob α)` -/
      

      The pkg parameter (and its type specifier) is optional.

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

        Define a new library facet. Has one form:

        library_facet «facet-name» (lib : LeanLib) : α :=
          /- build term of type `IndexBuildM (BuildJob α)` -/
        

        The lib parameter (and its type specifier) is optional.

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

          Custom Target Declaration #

          Define a new custom target for the package. Has one form:

          target «target-name» (pkg : NPackage _package.name) : α :=
            /- build term of type `IndexBuildM (BuildJob α)` -/
          

          The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

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

            Lean Library & Executable Target Declarations #

            Define a new Lean library target for the package. Can optionally be provided with a configuration of type LeanLibConfig. Has many forms:

            lean_lib «target-name»
            lean_lib «target-name» { /- config opts -/ }
            lean_lib «target-name» where /- config opts -/
            lean_lib «target-name» := /- config -/
            
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Define a new Lean binary executable target for the package. Can optionally be provided with a configuration of type LeanExeConfig. Has many forms:

              lean_exe «target-name»
              lean_exe «target-name» { /- config opts -/ }
              lean_exe «target-name» where /- config opts -/
              lean_exe «target-name» := /- config -/
              
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                External Library Target Declaration #

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

                  Define a new external library target for the package. Has one form:

                  extern_lib «target-name» (pkg : NPackage _package.name) :=
                    /- build term of type `IndexBuildM (BuildJob FilePath)` -/
                  

                  The pkg parameter (and its type specifier) is optional. It is of type NPackage _package.name to provably demonstrate the package provided is the package in which the target is defined.

                  The term should build the external library's static library.

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