From d231aaef04c523747d0fda384f650bbff4fd438f Mon Sep 17 00:00:00 2001 From: tydeu Date: Mon, 23 May 2022 19:47:29 -0400 Subject: [PATCH] feat: save resolved packages in a manifest closes #31 --- Lake/CLI/Main.lean | 30 +++++++++++-- Lake/Config/Manifest.lean | 32 +++++++++++++ Lake/Config/Resolve.lean | 92 +++++++++++++++++++++++++++++--------- Lake/Config/Workspace.lean | 7 +++ 4 files changed, 136 insertions(+), 25 deletions(-) create mode 100644 Lake/Config/Manifest.lean diff --git a/Lake/CLI/Main.lean b/Lake/CLI/Main.lean index 83bbea2..4fadc03 100644 --- a/Lake/CLI/Main.lean +++ b/Lake/CLI/Main.lean @@ -7,6 +7,7 @@ Authors: Mac Malone import Lake.Config.Load import Lake.Config.SearchPath import Lake.Config.InstallPath +import Lake.Config.Manifest import Lake.Config.Resolve import Lake.Config.Util import Lake.Util.Error @@ -17,7 +18,7 @@ import Lake.CLI.Help import Lake.CLI.Build open System -open Lean (Name Json toJson) +open Lean (Name Json toJson fromJson?) namespace Lake @@ -38,11 +39,15 @@ namespace Cli -- ## Basic Actions -/-- Print out a line wih the given message and then exit with an error code. -/ +/-- Print out a error line with the given message and then exit with an error code. -/ protected def error (msg : String) (rc : UInt32 := 1) : MainM α := do IO.eprintln s!"error: {msg}" |>.catchExceptions fun _ => pure () exit rc +/-- Print out a warning line wih the given message. -/ +def warning (msg : String) : MainM PUnit := do + IO.eprintln s!"warning: {msg}" |>.catchExceptions fun _ => pure () + instance : MonadError MainM := ⟨Cli.error⟩ instance : MonadLift IO MainM := ⟨MonadError.runIO⟩ @@ -89,10 +94,27 @@ def loadPkg (args : List String := []) : CliStateM Package := do setupLeanSearchPath (← getLeanInstall?) (← getLakeInstall?) Package.load dir args (dir / file) -def loadWorkspace (args : List String := []) : CliStateM Workspace := do +def loadWorkspace (args : List String := []) (updateDeps := true) : CliStateM Workspace := do let pkg ← loadPkg args let ws := Workspace.ofPackage pkg - let packageMap ← resolveDeps ws pkg |>.run LogMethods.eio (m := IO) + let manifest ← do + if let Except.ok contents ← IO.FS.readFile ws.manifestFile |>.toBaseIO then + match Json.parse contents with + | Except.ok json => + match fromJson? json with + | Except.ok (manifest : Manifest) => + pure manifest.toMap + | Except.error e => + warning s!"improperly formatted package manifest: {e}" + pure {} + | Except.error e => + warning s!"invalid JSON in package manifest: {e}" + pure {} + else + pure {} + let (packageMap, resolveMap) ← + resolveDeps ws pkg updateDeps |>.run manifest |>.run LogMethods.eio (m := IO) + IO.FS.writeFile ws.manifestFile <| Json.pretty <| toJson <| Manifest.fromMap resolveMap let packageMap := packageMap.insert pkg.name pkg return {ws with packageMap} diff --git a/Lake/Config/Manifest.lean b/Lake/Config/Manifest.lean new file mode 100644 index 0000000..3fd331e --- /dev/null +++ b/Lake/Config/Manifest.lean @@ -0,0 +1,32 @@ +/- +Copyright (c) 2022 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +import Lean.Data.Json + +open Lean + +namespace Lake + +/-- An entry for a package in the manifest. -/ +structure PackageEntry where + name : String + url : String + rev : String + deriving Inhabited, Repr, FromJson, ToJson + +/-- Manifest file format. -/ +structure Manifest where + version : Nat := 1 + packages : Array PackageEntry + deriving Inhabited, Repr, FromJson, ToJson + +namespace Manifest + +def toMap (self : Manifest) : NameMap PackageEntry := + self.packages.foldl (fun map entry => map.insert entry.name entry) {} + +def fromMap (map : NameMap PackageEntry) : Manifest := { + packages := map.fold (fun a k v => a.push v) #[] +} diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean index 4aac201..a5ac22f 100644 --- a/Lake/Config/Resolve.lean +++ b/Lake/Config/Resolve.lean @@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone -/ import Lake.Util.Git import Lake.Config.Load +import Lake.Config.Manifest import Lake.Config.Workspace import Lake.Build.Recursive @@ -13,44 +14,92 @@ open Lean (Name NameMap) namespace Lake -open Git in +section +open Git + +/-- Update the Git package in `dir` if necessary. -/ +def updateGitPkg (name : String) +(dir : FilePath) (url rev : String) : (LogT IO) PUnit := do + if (← headRevision dir) == rev then return + logInfo s!"{name}: updating {dir} to revision {rev}" + unless ← revisionExists rev dir do fetch dir + checkoutDetach rev dir + +/-- Clone the Git package as `dir`. -/ +def cloneGitPkg (name : String) +(dir : FilePath) (url rev : String) : (LogT IO) PUnit := do + logInfo s!"{name}: cloning {url} to {dir}" + clone url dir + let hash ← parseOriginRevision rev dir + checkoutDetach hash dir + +abbrev ResolveM := StateT (NameMap PackageEntry) <| LogT IO + /-- -Materializes a Git package in the given `dir`, -cloning and/or updating it as necessary. +Materializes a Git package in `dir`, cloning and/or updating it as necessary. + +Attempts to reproduce the `PackageEntry` in the manifest (if one exists) unless +`shouldUpdate` is true. Otherwise, produces the package based on `url` and `rev` +and saves the result to the manifest. -/ -def materializeGit -(name : String) (dir : FilePath) (url rev : String) : (LogT IO) PUnit := do - if ← dir.isDir then - let hash ← parseOriginRevision rev dir - if (← headRevision dir) == hash then return - logInfo s!"{name}: trying to update {dir} to revision {rev}" - unless ← revisionExists hash dir do fetch dir - checkoutDetach hash dir +def materializeGitPkg (name : String) +(dir : FilePath) (url rev : String) (shouldUpdate := true) : ResolveM PUnit := do + if let some entry := (← get).find? name then + if (← dir.isDir) then + if url = entry.url then + if shouldUpdate then + let rev ← parseOriginRevision rev dir + updateGitPkg name dir url rev + modify (·.insert name {entry with rev}) + else + updateGitPkg name dir url entry.rev + else if shouldUpdate then + logInfo s!"{name}: URL changed, deleting {dir} and cloning again" + IO.FS.removeDirAll dir + cloneGitPkg name dir url rev + let rev ← parseOriginRevision rev dir + modify (·.insert name {entry with url, rev}) + else + if shouldUpdate then + cloneGitPkg name dir url rev + let rev ← parseOriginRevision rev dir + modify (·.insert name {entry with url, rev}) + else + cloneGitPkg name dir entry.url entry.rev else - logInfo s!"{name}: cloning {url} to {dir}" - clone url dir - let hash ← parseOriginRevision rev dir - checkoutDetach hash dir + if (← dir.isDir) then + let rev ← parseOriginRevision rev dir + modify (·.insert name {name, url, rev}) + if (← headRevision dir) == rev then return + updateGitPkg name dir url rev + else + cloneGitPkg name dir url rev + let rev ← parseOriginRevision rev dir + modify (·.insert name {name, url, rev}) + +end /-- Materializes a `Dependency` relative to the given `Package`, downloading and/or updating it as necessary. -/ -def materializeDep (ws : Workspace) (pkg : Package) (dep : Dependency) : (LogT IO) FilePath := +def materializeDep (ws : Workspace) +(pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM FilePath := match dep.src with | Source.path dir => return pkg.dir / dir | Source.git url rev => do let name := dep.name.toString (escape := false) let depDir := ws.packagesDir / name - materializeGit name depDir url rev + materializeGitPkg name depDir url rev shouldUpdate return depDir /-- Resolves a `Dependency` relative to the given `Package` in the same `Workspace`, downloading and/or updating it as necessary. -/ -def resolveDep (ws : Workspace) (pkg : Package) (dep : Dependency) : (LogT IO) Package := do - let dir ← materializeDep ws pkg dep +def resolveDep (ws : Workspace) +(pkg : Package) (dep : Dependency) (shouldUpdate := true) : ResolveM Package := do + let dir ← materializeDep ws pkg dep shouldUpdate let depPkg ← Package.load (dir / dep.dir) dep.args unless depPkg.name == dep.name do throw <| IO.userError <| @@ -62,9 +111,10 @@ def resolveDep (ws : Workspace) (pkg : Package) (dep : Dependency) : (LogT IO) P Resolves the package's dependencies, downloading and/or updating them as necessary. -/ -def resolveDeps (ws : Workspace) (pkg : Package) : (LogT IO) (NameMap Package) := do +def resolveDeps (ws : Workspace) (pkg : Package) +(shouldUpdate := true) : ResolveM (NameMap Package) := do let resolve dep resolve := do - let pkg ← resolveDep ws pkg dep + let pkg ← resolveDep ws pkg dep shouldUpdate pkg.dependencies.forM fun dep => discard <| resolve dep return pkg let (res, map) ← RBTopT.run <| pkg.dependencies.forM fun dep => diff --git a/Lake/Config/Workspace.lean b/Lake/Config/Workspace.lean index 0a36167..4d2a3ba 100644 --- a/Lake/Config/Workspace.lean +++ b/Lake/Config/Workspace.lean @@ -13,6 +13,9 @@ open Lean (Name NameMap LeanPaths) namespace Lake +/-- The file name of a workspace's package manifest (i.e., `manifest.json`). -/ +def manifestFileName := "manifest.json" + /-- A Lake workspace -- the top-level package directory. -/ structure Workspace where /-- The root package of the workspace. -/ @@ -60,6 +63,10 @@ def config (self : Workspace) : WorkspaceConfig := def packagesDir (self : Workspace) : FilePath := self.dir / self.config.packagesDir +/-- The workspace's JSON manifest of packages. -/ +def manifestFile (self : Workspace) : FilePath := + self.packagesDir / manifestFileName + /-- The `List` of packages to the workspace. -/ def packageList (self : Workspace) : List Package := self.packageMap.revFold (fun pkgs _ pkg => pkg :: pkgs) []