Package Declarations

DSL definitions for packages and hooks.

def Lake.DSL.packageDeclName : Lean.Name

The name given to the definition created by the package syntax.

Equations

• Lake.DSL.packageDeclName = `_package

def Lake.DSL.packageDecl : Lean.ParserDescr

Defines the configuration of a Lake package. Has many forms:

package «pkg-name»
package «pkg-name» { /- config opts -/ }
package «pkg-name» where /- config opts -/

There can only be one package declaration per Lake configuration file. The defined package configuration will be available for reference as _package.

Equations

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

def Lake.DSL.elabPackageDecl : Lean.Elab.Command.CommandElab

Equations

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

@[reducible, inline]

abbrev Lake.DSL.PackageDecl : Type

Equations

• Lake.DSL.PackageDecl = Lean.TSyntax `Lake.DSL.packageDecl

instance Lake.DSL.instCoePackageDeclCommand : Coe PackageDecl Lean.Command

Equations

• Lake.DSL.instCoePackageDeclCommand = { coe := fun (x : Lake.DSL.PackageDecl) => { raw := x.raw } }

def Lake.DSL.postUpdateDecl : Lean.ParserDescr

Declare a post-lake update hook for the package. Runs the monadic action is after a successful lake update execution in this package or one of its downstream dependents.

Example

This feature enables Mathlib to synchronize the Lean toolchain and run cache get after a lake update:

lean_exe cache
post_update pkg do
  let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
  let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
  IO.FS.writeFile wsToolchainFile mathlibToolchain
  let exeFile ← runBuild cache.fetch
  let exitCode ← env exeFile.toString #["get"]
  if exitCode ≠ 0 then
    error s!"{pkg.name}: failed to fetch cache"

Equations

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

def Lake.DSL.expandPostUpdateDecl : Lean.Macro

Equations

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