Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor: change postUpdate? config to a decl #2723

Merged
merged 1 commit into from
Oct 21, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions RELEASES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
4 changes: 4 additions & 0 deletions src/lake/Lake/Build/Index.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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
51 changes: 21 additions & 30 deletions src/lake/Lake/Config/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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. -/
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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. -/
Expand All @@ -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?
Expand Down
3 changes: 3 additions & 0 deletions src/lake/Lake/DSL/Attributes.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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"

Expand Down
42 changes: 42 additions & 0 deletions src/lake/Lake/DSL/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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?]?)
19 changes: 15 additions & 4 deletions src/lake/Lake/DSL/Script.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
8 changes: 4 additions & 4 deletions src/lake/Lake/Load/Main.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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!" {·}")
Expand Down
13 changes: 11 additions & 2 deletions src/lake/Lake/Load/Package.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
}

/--
Expand Down
23 changes: 10 additions & 13 deletions src/lake/tests/postUpdate/dep/lakefile.lean
Original file line number Diff line number Diff line change
@@ -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"