feat: lake: postUpdate? + test

Author: tydeu

RELEASES.md

@@ -14,6 +14,7 @@ v4.3.0 (development in progress)
 * The derive handler for `DecidableEq` [now handles](https://github.com/leanprover/lean4/pull/2591) mutual inductive types.
 * [Show path of failed import in Lake](https://github.com/leanprover/lean4/pull/2616).
 * [Fix linker warnings on macOS](https://github.com/leanprover/lean4/pull/2598).
+* **Lake:** Add `postUpdate?` package configuration option. Used by a package to specify some code which should be run after a successful `lake update` of the package or one of its downstream dependencies. ([lake#185](https://github.com/leanprover/lake/issues/185))
 
 v4.2.0
 ---------

src/lake/Lake/Config/Package.lean

@@ -90,6 +90,32 @@ structure PackageConfig extends WorkspaceConfig, LeanConfig where
   /-- An `Array` of target names to build whenever the package is used. -/
   extraDepTargets : Array Name := #[]
 
+  /--
+  A post-`lake update` hook. The monadic action is run after a successful
+  `lake update` execution on this package or one of its downstream dependents.
+  Defaults to `none`.
+
+  As an example, Mathlib can use this feature to synchronize the Lean toolchain
+  and run `cache get`:
+
+  ```
+  package mathlib where
+    postUpdate? := some do
+      let some pkg ← findPackage? `mathlib
+        | error "mathlib is missing from workspace"
+      let wsToolchainFile := (← getRootPackage).dir / "lean-toolchain"
+      let mathlibToolchain ← IO.FS.readFile <| pkg.dir / "lean-toolchain"
+      IO.FS.writeFile wsToolchainFile mathlibToolchain
+      let some exe := pkg.findLeanExe? `cache
+        | error s!"{pkg.name}: cache is missing from the package"
+      let exeFile ← runBuild (exe.build >>= (·.await))
+      let exitCode ← env exeFile.toString #["get"]
+      if exitCode ≠ 0 then
+        error s!"{pkg.name}: failed to fetch cache"
+  ```
+  -/
+  postUpdate? : Option (LakeT LogIO PUnit) := none
+
   /--
   Whether to compile each of the package's module into a native shared library
   that is loaded whenever the module is imported. This speeds up evaluation of
@@ -263,6 +289,10 @@ namespace Package
 @[inline] def extraDepTargets (self : Package) : Array Name :=
   self.config.extraDepTargets
 
+/-- The package's `postUpdate?` configuration. -/
+@[inline] def postUpdate? (self : Package) :=
+  self.config.postUpdate?
+
 /-- The package's `releaseRepo?` configuration. -/
 @[inline] def releaseRepo? (self : Package) : Option String :=
   self.config.releaseRepo?

src/lake/Lake/Load/Main.lean

@@ -40,6 +40,50 @@ def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
     remoteUrl? := dep.remoteUrl?
   }
 
+/--
+Load a `Workspace` for a Lake package by elaborating its configuration file.
+Does not resolve dependencies.
+-/
+def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
+  Lean.searchPathRef.set config.env.leanSearchPath
+  let configEnv ← importConfigFile config.rootDir config.rootDir
+    config.configOpts config.leanOpts config.configFile config.reconfigure
+  let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
+  let root := {
+    configEnv, leanOpts := config.leanOpts
+    dir := config.rootDir, config := pkgConfig
+  }
+  return {
+    root, lakeEnv := config.env
+    moduleFacetConfigs := initModuleFacetConfigs
+    packageFacetConfigs := initPackageFacetConfigs
+    libraryFacetConfigs := initLibraryFacetConfigs
+  }
+
+/--
+Finalize the workspace's root and its transitive dependencies
+and add them to the workspace.
+-/
+def Workspace.finalize (ws : Workspace) : LogIO Workspace := do
+  have : MonadStore Name Package (StateT Workspace LogIO) := {
+    fetch? := fun name => return (← get).findPackage? name
+    store := fun _ pkg => modify (·.addPackage pkg)
+  }
+  let (res, ws) ← EStateT.run ws do
+    buildTop (·.name) ws.root fun pkg load => do
+      let depPkgs ← pkg.deps.mapM load
+      set <| ← IO.ofExcept <| (← get).addFacetsFromEnv pkg.configEnv pkg.leanOpts
+      let pkg ← pkg.finalize depPkgs
+      return pkg
+  match res with
+  | Except.ok root =>
+    return {ws with root}
+  | Except.error cycle => do
+    let cycle := cycle.map (s!"  {·}")
+    error <|
+      s!"oops! dependency load cycle detected (this likely indicates a bug in Lake):\n" ++
+      "\n".intercalate cycle
+
 /--
 Rebuild the workspace's Lake manifest and materialize missing dependencies.
 
@@ -51,7 +95,7 @@ root dependencies. Otherwise, only update the root dependencies specified.
 If `reconfigure`, elaborate configuration files while updating, do not use OLeans.
 -/
 def buildUpdatedManifest (ws : Workspace)
-(toUpdate : NameSet := {}) (reconfigure := true) : LogIO (Workspace × Manifest) := do
+(toUpdate : NameSet := {}) (reconfigure := true) : LogIO Workspace := do
   let res ← StateT.run (s := mkOrdNameMap MaterializedDep) <| EStateT.run' (mkNameMap Package) do
     -- Use manifest versions of root packages that should not be updated
     unless toUpdate.isEmpty do
@@ -86,57 +130,19 @@ def buildUpdatedManifest (ws : Workspace)
       return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
   match res with
   | (.ok root, deps) =>
+    let ws : Workspace ← {ws with root}.finalize
+    LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
+      if let some postUpdate := pkg.postUpdate? then
+        logInfo s!"{pkg.name}: running post-update hook"
+        postUpdate
     let manifest : Manifest := {name? := ws.root.name, packagesDir? := ws.relPkgsDir}
-    let manifest := deps.foldl (fun m d => m.addPackage d.manifestEntry) manifest
-    return ({ws with root}, manifest)
+    let manifest := deps.foldl (·.addPackage ·.manifestEntry) manifest
+    manifest.saveToFile ws.manifestFile
+    return ws
   | (.error cycle, _) =>
     let cycle := cycle.map (s!"  {·}")
     error s!"dependency cycle detected:\n{"\n".intercalate cycle}"
 
-/--
-Load a `Workspace` for a Lake package by elaborating its configuration file.
-Does not resolve dependencies.
--/
-def loadWorkspaceRoot (config : LoadConfig) : LogIO Workspace := do
-  Lean.searchPathRef.set config.env.leanSearchPath
-  let configEnv ← importConfigFile config.rootDir config.rootDir
-    config.configOpts config.leanOpts config.configFile config.reconfigure
-  let pkgConfig ← IO.ofExcept <| PackageConfig.loadFromEnv configEnv config.leanOpts
-  let root := {
-    configEnv, leanOpts := config.leanOpts
-    dir := config.rootDir, config := pkgConfig
-  }
-  return {
-    root, lakeEnv := config.env
-    moduleFacetConfigs := initModuleFacetConfigs
-    packageFacetConfigs := initPackageFacetConfigs
-    libraryFacetConfigs := initLibraryFacetConfigs
-  }
-
-/--
-Finalize the workspace's root and its transitive dependencies
-and add them to the workspace.
--/
-def Workspace.finalize (ws : Workspace) : LogIO Workspace := do
-  have : MonadStore Name Package (StateT Workspace LogIO) := {
-    fetch? := fun name => return (← get).findPackage? name
-    store := fun _ pkg => modify (·.addPackage pkg)
-  }
-  let (res, ws) ← EStateT.run ws do
-    buildTop (·.name) ws.root fun pkg load => do
-      let depPkgs ← pkg.deps.mapM load
-      set <| ← IO.ofExcept <| (← get).addFacetsFromEnv pkg.configEnv pkg.leanOpts
-      let pkg ← pkg.finalize depPkgs
-      return pkg
-  match res with
-  | Except.ok root =>
-    return {ws with root}
-  | Except.error cycle => do
-    let cycle := cycle.map (s!"  {·}")
-    error <|
-      s!"oops! dependency load cycle detected (this likely indicates a bug in Lake):\n" ++
-      "\n".intercalate cycle
-
 /--
 Resolving a workspace's dependencies using a manifest,
 downloading and/or updating them as necessary.
@@ -200,15 +206,13 @@ def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
   if updateDeps then
-    let (ws, manifest) ← buildUpdatedManifest ws {} rc
-    manifest.saveToFile ws.manifestFile
-    ws.finalize
+    buildUpdatedManifest ws {} rc
   else
     ws.materializeDeps (← Manifest.loadOrEmpty ws.manifestFile) rc
 
 /-- Updates the manifest for the loaded Lake workspace (see `buildUpdatedManifest`). -/
 def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
-  let (ws, manifest) ← buildUpdatedManifest ws toUpdate rc
-  manifest.saveToFile ws.manifestFile
+  discard <| buildUpdatedManifest ws toUpdate rc
+

src/lake/README.md

@@ -164,6 +164,7 @@ Lake provides a large assortment of configuration options for packages.
 
 ### Build & Run
 
+* `postUpdate?`: A post-`lake update` hook. The monadic action is run after a successful `lake update` execution on this package or one of its downstream dependents. Defaults to `none`. See the option's docstring for a complete example.
 * `precompileModules`:  Whether to compile each module into a native shared library that is loaded whenever the module is imported. This speeds up the evaluation of metaprograms and enables the interpreter to run functions marked `@[extern]`. Defaults to `false`.
 * `moreServerArgs`:  Additional arguments to pass to the Lean language server (i.e., `lean --server`) launched by `lake serve`.
 * `buildType`: The `BuildType` of targets in the package (see [`CMAKE_BUILD_TYPE`](https://stackoverflow.com/a/59314670)). One of `debug`, `relWithDebInfo`, `minSizeRel`, or `release`. Defaults to `release`.

src/lake/tests/postUpdate/.gitignore

@@ -0,0 +1,3 @@
+lakefile.olean
+lake-manifest.json
+toolchain

src/lake/tests/postUpdate/clean.sh

@@ -0,0 +1,2 @@
+rm -rf dep/build dep/lakefile.olean dep/toolchain
+rm -f lake-manifest.json lakefile.olean toolchain

src/lake/tests/postUpdate/dep/hello.lean

@@ -0,0 +1,2 @@
+def main (args : List String) : IO Unit := do
+  IO.println s!"post-update hello w/ arguments: {args}"

src/lake/tests/postUpdate/dep/lakefile.lean

@@ -0,0 +1,18 @@
+import Lake
+open Lake DSL
+
+package dep where
+  postUpdate? := some do
+    let some pkg ← findPackage? `dep
+      | error "dep is missing from workspace"
+    let wsToolchainFile := (← getRootPackage).dir / "toolchain"
+    let depToolchain ← IO.FS.readFile <| pkg.dir / "toolchain"
+    IO.FS.writeFile wsToolchainFile depToolchain
+    let some exe := pkg.findLeanExe? `hello
+      | error s!"{pkg.name}: hello is missing from the package"
+    let exeFile ← runBuild (exe.build >>= (·.await))
+    let exitCode ← env exeFile.toString #["get"]
+    if exitCode ≠ 0 then
+      error s!"{pkg.name}: failed to fetch hello"
+
+lean_exe hello

src/lake/tests/postUpdate/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open Lake DSL
+
+package test
+require dep from "dep"

src/lake/tests/postUpdate/test.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+./clean.sh
+
+# Test the `postUpdate?` configuration option and the docstring example.
+# If the Lake API experiences changes, this test and the docstring should be
+# updated in tandem.
+
+echo "root" > toolchain
+echo "dep" > dep/toolchain
+$LAKE update | grep -F "post-update hello w/ arguments: [get]"
+test "`cat toolchain`" = dep
+