feat: save resolved packages in a manifest

closes leanprover/lake#31

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}
 

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) #[]
+}

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 =>

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) []