refactor: change postUpdate? config to a decl

Author: tydeu

RELEASES.md

@@ -11,6 +11,11 @@ v4.3.0 (development in progress)
 ---------
 
 * [Cancel outstanding tasks on document edit in the language server](https://github.com/leanprover/lean4/pull/2648).
+* **Lake:** Changed `postUpdate?` configuration option to a `post_update` declaration. See the `post_update` syntax docstring for more information on the new syntax.
+
+* [Lake: A manifest is automatically created on workspace load if one does not exists.](https://github.com/leanprover/lean4/pull/2680).
+
+* **Lake:** The `:=` syntax for configuration declarations (i.e., `package`, `lean_lib`, and `lean_exe`) has been deprecated. For example, `package foo := {...}` is deprecated.
 
 v4.2.0
 ---------

src/lake/Lake/Build/Index.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Build.Targets
 import Lake.Build.Executable
 import Lake.Build.Topological
 
@@ -104,5 +105,8 @@ export BuildInfo (build)
 @[inline] protected def LeanExe.build (self : LeanExe) : BuildM (BuildJob FilePath) :=
   self.exe.build
 
+@[inline] protected def LeanExeConfig.build (self : LeanExeConfig) : BuildM (BuildJob FilePath) := do
+  (← self.get).build
+
 @[inline] protected def LeanExe.fetch (self : LeanExe) : IndexBuildM (BuildJob FilePath) :=
   self.exe.fetch

src/lake/Lake/Config/Package.lean

@@ -90,32 +90,6 @@ 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
@@ -197,6 +171,9 @@ deriving Inhabited
 /-! # Package -/
 --------------------------------------------------------------------------------
 
+
+declare_opaque_type OpaquePostUpdateHook (pkg : Name)
+
 /-- A Lake package -- its location plus its configuration. -/
 structure Package where
   /-- The path to the package's directory. -/
@@ -231,6 +208,8 @@ structure Package where
   (i.e., on a bare `lake run` of the package).
   -/
   defaultScripts : Array Script := #[]
+  /-- Post-`lake update` hooks for the package. -/
+  postUpdateHooks : Array (OpaquePostUpdateHook config.name) := #[]
 
 instance : Nonempty Package :=
   have : Inhabited Environment := Classical.inhabited_of_nonempty inferInstance
@@ -263,6 +242,22 @@ instance : CoeDep Package pkg (NPackage pkg.name) := ⟨⟨pkg, rfl⟩⟩
 /-- The package's name. -/
 abbrev NPackage.name (_ : NPackage n) := n
 
+/--
+The type of a post-update hooks monad.
+`IO` equipped with logging ability and information about the Lake configuration.
+-/
+abbrev PostUpdateFn (pkgName : Name) := NPackage pkgName → LakeT LogIO PUnit
+
+structure PostUpdateHook (pkgName : Name) where
+  fn : PostUpdateFn pkgName
+  deriving Inhabited
+
+hydrate_opaque_type OpaquePostUpdateHook PostUpdateHook name
+
+structure PostUpdateHookDecl where
+  pkg : Name
+  fn : PostUpdateFn pkg
+
 namespace Package
 
 /-- The package's direct dependencies. -/
@@ -289,10 +284,6 @@ 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/DSL/Attributes.lean

@@ -14,6 +14,9 @@ initialize packageAttr : OrderedTagAttribute ←
 initialize packageDepAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `package_dep "mark a definition as a Lake package dependency"
 
+initialize postUpdateAttr : OrderedTagAttribute ←
+  registerOrderedTagAttribute `post_update "mark a definition as a Lake package post-update hook"
+
 initialize scriptAttr : OrderedTagAttribute ←
   registerOrderedTagAttribute `script "mark a definition as a Lake script"
 

src/lake/Lake/DSL/Package.lean

@@ -10,6 +10,10 @@ import Lake.DSL.DeclUtil
 namespace Lake.DSL
 open Lean Parser Command
 
+/-! # Package Declarations
+DSL definitions for packages and hooks.
+-/
+
 /-- The name given to the definition created by the `package` syntax. -/
 def packageDeclName := `_package
 
@@ -33,3 +37,40 @@ doc?:optional(docComment) attrs?:optional(Term.attributes)
   let ty := mkCIdentFrom (← getRef) ``PackageConfig
   let attrs := #[attr] ++ expandAttrs attrs?
   mkConfigStructDecl packageDeclName doc? attrs ty sig
+
+/--
+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.build >>= (·.await)
+  let exitCode ← env exeFile.toString #["get"]
+  if exitCode ≠ 0 then
+    error s!"{pkg.name}: failed to fetch cache"
+```
+-/
+scoped syntax (name := postUpdateDecl)
+optional(docComment) optional(Term.attributes)
+"post_update " (ppSpace simpleBinder)? (declValSimple <|> declValDo) : command
+
+macro_rules
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? do $seq $[$wds?]?) =>
+  `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?]?)
+| `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?]?) => do
+  let pkg ← expandOptSimpleBinder pkg?
+  let pkgName := mkIdentFrom pkg `_package.name
+  let attr ← withRef kw `(Term.attrInstance| «post_update»)
+  let attrs := #[attr] ++ expandAttrs attrs?
+  `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl :=
+    {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?]?)

src/lake/Lake/DSL/Script.lean

@@ -7,18 +7,29 @@ import Lake.Config.Package
 import Lake.DSL.Attributes
 import Lake.DSL.DeclUtil
 
+/-! # Script Declarations
+DSL definitions to define a Lake script for a package.
+-/
+
 namespace Lake.DSL
 open Lean Parser Command
 
 syntax scriptDeclSpec :=
   ident (ppSpace simpleBinder)? (declValSimple <|> declValDo)
 
 /--
-Define a new Lake script for the package. Has two forms:
+Define a new Lake script for the package.
 
-```lean
-script «script-name» (args) do /- ... -/
-script «script-name» (args) := ...
+**Example**
+
+```
+/-- Display a greeting -/
+script «script-name» (args) do
+  if h : 0 < args.length then
+    IO.println s!"Hello, {args[0]'h}!"
+  else
+    IO.println "Hello, world!"
+  return 0
 ```
 -/
 scoped syntax (name := scriptDecl)

src/lake/Lake/Load/Main.lean

@@ -131,13 +131,13 @@ def buildUpdatedManifest (ws : Workspace)
   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
+    LakeT.run ⟨ws⟩ <| ws.packages.forM fun pkg => do
+      unless pkg.postUpdateHooks.isEmpty do
+        logInfo s!"{pkg.name}: running post-update hooks"
+        pkg.postUpdateHooks.forM fun hook => hook.get.fn pkg
     return ws
   | (.error cycle, _) =>
     let cycle := cycle.map (s!"  {·}")

src/lake/Lake/Load/Package.lean

@@ -69,7 +69,7 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
   let opts := self.leanOpts
   let strName := self.name.toString (escape := false)
 
-  -- Load Script, Facet, & Target Configurations
+  -- Load Script, Facet, Target, and Hook Configurations
   let scripts ← mkTagMap env scriptAttr fun scriptName => do
     let name := strName ++ "/" ++ scriptName.toString (escape := false)
     let fn ← IO.ofExcept <| evalConstCheck env opts ScriptFn ``ScriptFn scriptName
@@ -98,12 +98,21 @@ def Package.finalize (self : Package) (deps : Array Package) : LogIO Package :=
         error s!"target was defined as `{decl.pkg}/{decl.name}`, but was registered as `{self.name}/{name}`"
     | .error e => error e
   let defaultTargets := defaultTargetAttr.getAllEntries env
+  let postUpdateHooks ← postUpdateAttr.getAllEntries env |>.mapM fun name =>
+    match evalConstCheck env opts PostUpdateHookDecl ``PostUpdateHookDecl name with
+    | .ok decl =>
+      if h : decl.pkg = self.config.name then
+        return OpaquePostUpdateHook.mk ⟨h ▸ decl.fn⟩
+      else
+        error s!"post-update hook was defined in `{decl.pkg}`, but was registered in `{self.name}`"
+    | .error e => error e
 
   -- Fill in the Package
   return {self with
     opaqueDeps := deps.map (.mk ·)
     leanLibConfigs, leanExeConfigs, externLibConfigs
-    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts
+    opaqueTargetConfigs, defaultTargets, scripts, defaultScripts,
+    postUpdateHooks
   }
 
 /--

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

@@ -1,18 +1,15 @@
 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"
+package dep
 
 lean_exe hello
+
+post_update pkg do
+  let wsToolchainFile := (← getRootPackage).dir / "toolchain"
+  let depToolchain ← IO.FS.readFile <| pkg.dir / "toolchain"
+  IO.FS.writeFile wsToolchainFile depToolchain
+  let exeFile ← runBuild hello.build >>= (·.await)
+  let exitCode ← env exeFile.toString #["get"]
+  if exitCode ≠ 0 then
+    error s!"{pkg.name}: failed to fetch hello"