From 2ec2dac3e9904a9f355bc3314d539ec25f0aa473 Mon Sep 17 00:00:00 2001 From: tydeu Date: Fri, 20 Oct 2023 18:07:34 -0400 Subject: [PATCH] refactor: change `postUpdate?` config to a decl --- RELEASES.md | 2 + src/lake/Lake/Build/Index.lean | 4 ++ src/lake/Lake/Config/Package.lean | 51 +++++++++------------ src/lake/Lake/DSL/Attributes.lean | 3 ++ src/lake/Lake/DSL/Package.lean | 42 +++++++++++++++++ src/lake/Lake/DSL/Script.lean | 19 ++++++-- src/lake/Lake/Load/Main.lean | 8 ++-- src/lake/Lake/Load/Package.lean | 13 +++++- src/lake/tests/postUpdate/dep/lakefile.lean | 23 ++++------ 9 files changed, 112 insertions(+), 53 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 2d1a2c3045b2..f14978116770 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -10,6 +10,8 @@ Please check the [releases](https://github.com/leanprover/lean4/releases) page f v4.3.0 (development in progress) --------- +* **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. diff --git a/src/lake/Lake/Build/Index.lean b/src/lake/Lake/Build/Index.lean index c065840cf573..51daf995821c 100644 --- a/src/lake/Lake/Build/Index.lean +++ b/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 diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean index 825e4c010342..e3170323c61f 100644 --- a/src/lake/Lake/Config/Package.lean +++ b/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? diff --git a/src/lake/Lake/DSL/Attributes.lean b/src/lake/Lake/DSL/Attributes.lean index 3f0ec39945e0..2d2af9a4d538 100644 --- a/src/lake/Lake/DSL/Attributes.lean +++ b/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" diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean index 2898cf1577ea..6aead21854eb 100644 --- a/src/lake/Lake/DSL/Package.lean +++ b/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 @@ -32,3 +36,41 @@ doc?:optional(docComment) attrs?:optional(Term.attributes) let ty := mkCIdentFrom (← getRef) ``PackageConfig let attrs := #[attr] ++ expandAttrs attrs? mkConfigDecl 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?]?) diff --git a/src/lake/Lake/DSL/Script.lean b/src/lake/Lake/DSL/Script.lean index 0bfa583cdd7f..f7a5b5717603 100644 --- a/src/lake/Lake/DSL/Script.lean +++ b/src/lake/Lake/DSL/Script.lean @@ -7,6 +7,10 @@ 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 @@ -14,11 +18,18 @@ 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) diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean index b3200830d443..4c1907d9130d 100644 --- a/src/lake/Lake/Load/Main.lean +++ b/src/lake/Lake/Load/Main.lean @@ -131,13 +131,13 @@ def Workspace.updateAndMaterialize (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!" {·}") diff --git a/src/lake/Lake/Load/Package.lean b/src/lake/Lake/Load/Package.lean index 3ba6b69b8b27..ccd0d85da8c0 100644 --- a/src/lake/Lake/Load/Package.lean +++ b/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 } /-- diff --git a/src/lake/tests/postUpdate/dep/lakefile.lean b/src/lake/tests/postUpdate/dep/lakefile.lean index 96430764a369..5c326bd5e70a 100644 --- a/src/lake/tests/postUpdate/dep/lakefile.lean +++ b/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"