Documentation

Lake.DSL.Targets

DSL for Targets & Facets #

Macros for declaring Lake targets and facets.

Facet Declarations #

@[reducible, inline]
Equations
    Instances For
      @[reducible, inline]
      Equations
        Instances For
          @[reducible, inline]
          Equations
            Instances For

              Custom Target Declaration #

              @[reducible, inline]
              abbrev Lake.DSL.mkTargetDecl (α : Type) (pkgName target : Lean.Name) [OptDataKind α] [FormatQuery α] [FamilyDef (CustomData pkgName) target α] (f : NPackage pkgNameFetchM (Job α)) :
              Equations
                Instances For

                  Lean Library & Executable Target Declarations #

                  @[reducible, inline]
                  abbrev Lake.DSL.mkConfigDecl (pkg name kind : Lean.Name) (config : ConfigType kind pkg name) [FamilyDef (CustomData pkg) name (ConfigTarget kind)] [FamilyDef DataType kind (ConfigTarget kind)] :
                  Equations
                    Instances For
                      def Lake.DSL.mkConfigDeclDef (tyName attr kind : Lean.Name) [ConfigInfo tyName] [delTyName : TypeName (KConfigDecl kind)] (doc? : Option DocComment) (attrs? : Option Attributes) (nameStx? : Option IdentOrStr) (cfg : OptConfig) :
                      Equations
                        Instances For
                          @[reducible, inline]

                          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 -/
                          
                          Equations
                            Instances For
                              @[reducible, inline]

                              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 -/
                              
                              Equations
                                Instances For
                                  @[reducible, inline]

                                  Define a new input file target for the package. Can optionally be provided with a configuration of type InputFileConfig.

                                  Equations
                                    Instances For
                                      @[reducible, inline]

                                      Define a new input directory target for the package. Can optionally be provided with a configuration of type InputDirConfig.

                                      Equations
                                        Instances For

                                          External Library Target Declaration #

                                          @[reducible, inline]
                                          Equations
                                            Instances For