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

A external library's declarative configuration.

• getJob : Lake.CustomData (pkgName, Lean.Name.str name "static") → Lake.BuildJob Lake.FilePath

  The library's build data.

instance Lake.instInhabitedExternLibConfig : {a a_1 : Lake.Name} → Inhabited (Lake.ExternLibConfig a a_1)

Equations

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

structure Lake.ExternLibDecl : Type

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

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