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.

Instances For

• Lake.instInhabitedExternLibConfig

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

Equations

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