feat: lake: postUpdate? + test

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,59 +40,6 @@ def loadDepPackage (wsDir : FilePath) (dep : MaterializedDep)
     remoteUrl? := dep.remoteUrl?
   }
 
-/--
-Rebuild the workspace's Lake manifest and materialize missing dependencies.
-
-Packages are updated to latest specific revision matching that in `require`
-(e.g., if the `require` is `@master`, update to latest commit on master) or
-removed if the `require` is removed. If `tuUpdate` is empty, update/remove all
-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
-  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
-      for entry in (← Manifest.loadOrEmpty ws.manifestFile) do
-        unless entry.inherited || toUpdate.contains entry.name do
-          let dep ← entry.materialize ws.dir ws.relPkgsDir
-          modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
-    buildAcyclic (·.1.name) (ws.root, FilePath.mk ".") fun (pkg, relPkgDir) resolve => do
-      let inherited := pkg.name != ws.root.name
-      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
-      -- Materialize this package's dependencies first
-      let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
-        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir
-      -- Load dependency packages and materialize their locked dependencies
-      let deps ← deps.mapM fun dep => do
-        if let .some pkg := (← getThe (NameMap Package)).find? dep.name then
-          return (pkg, dep.relPkgDir)
-        else
-          -- Load the package
-          let depPkg ← loadDepPackage ws.dir dep pkg.leanOpts dep.opts reconfigure
-          if depPkg.name ≠ dep.name then
-            logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
-          -- Materialize locked dependencies
-          for entry in (← Manifest.loadOrEmpty depPkg.manifestFile) do
-            unless (← getThe (OrdNameMap MaterializedDep)).contains entry.name do
-              let entry := entry.setInherited.inDirectory dep.relPkgDir
-              let dep ← entry.materialize ws.dir ws.relPkgsDir
-              modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
-          modifyThe (NameMap Package) (·.insert dep.name depPkg)
-          return (depPkg, dep.relPkgDir)
-      -- Resolve dependencies's dependencies recursively
-      return {pkg with opaqueDeps := ← deps.mapM (.mk <$> resolve ·)}
-  match res with
-  | (.ok root, deps) =>
-    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)
-  | (.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.
@@ -137,6 +84,65 @@ def Workspace.finalize (ws : Workspace) : LogIO Workspace := do
       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.
+
+Packages are updated to latest specific revision matching that in `require`
+(e.g., if the `require` is `@master`, update to latest commit on master) or
+removed if the `require` is removed. If `tuUpdate` is empty, update/remove all
+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 := 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
+      for entry in (← Manifest.loadOrEmpty ws.manifestFile) do
+        unless entry.inherited || toUpdate.contains entry.name do
+          let dep ← entry.materialize ws.dir ws.relPkgsDir
+          modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
+    buildAcyclic (·.1.name) (ws.root, FilePath.mk ".") fun (pkg, relPkgDir) resolve => do
+      let inherited := pkg.name != ws.root.name
+      let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
+      -- Materialize this package's dependencies first
+      let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
+        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir
+      -- Load dependency packages and materialize their locked dependencies
+      let deps ← deps.mapM fun dep => do
+        if let .some pkg := (← getThe (NameMap Package)).find? dep.name then
+          return (pkg, dep.relPkgDir)
+        else
+          -- Load the package
+          let depPkg ← loadDepPackage ws.dir dep pkg.leanOpts dep.opts reconfigure
+          if depPkg.name ≠ dep.name then
+            logWarning s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
+          -- Materialize locked dependencies
+          for entry in (← Manifest.loadOrEmpty depPkg.manifestFile) do
+            unless (← getThe (OrdNameMap MaterializedDep)).contains entry.name do
+              let entry := entry.setInherited.inDirectory dep.relPkgDir
+              let dep ← entry.materialize ws.dir ws.relPkgsDir
+              modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
+          modifyThe (NameMap Package) (·.insert dep.name depPkg)
+          return (depPkg, dep.relPkgDir)
+      -- Resolve dependencies's dependencies recursively
+      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 (·.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}"
+
 /--
 Resolving a workspace's dependencies using a manifest,
 downloading and/or updating them as necessary.
@@ -200,9 +206,7 @@ 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
 
@@ -210,5 +214,5 @@ def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace
 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
+