structure Lake.ExternLibConfig (pkgName name : Lean.Name) : Type

A external library's declarative configuration.

• getPath : Job (CustomData (pkgName, name.str "static")) → Job System.FilePath

  The library's build data.

instance Lake.instInhabitedExternLibConfig {a✝ a✝¹ : Lean.Name} : Inhabited (ExternLibConfig a✝ a✝¹)

Equations

• Lake.instInhabitedExternLibConfig = { default := { getPath := default } }

structure Lake.ExternLibDecl : Type

A dependently typed configuration based on its registered package and name.

• pkg : Lean.Name
• name : Lean.Name
• config : ExternLibConfig self.pkg self.name