Documentation

Lake.DSL.Package

Package Declarations #

DSL definitions for packages and hooks.

source
def Lake.DSL.packageDeclName :
Lean.Name

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

Equations
source
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.
source
@[reducible, inline]
abbrev Lake.DSL.PackageDecl :
Type
Equations
Instances For
source
instance Lake.DSL.instCoePackageDeclCommand :
Coe Lake.DSL.PackageDecl Lean.Command
Equations
source
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.