From e435a45af76a99efff8183148b61c9b68dcdfa4e Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 12 Oct 2023 19:36:51 -0400
Subject: [PATCH] feat: lake: create manifest on load if missing

---
 src/lake/Lake/Load/Main.lean     | 11 ++++---
 src/lake/Lake/Load/Manifest.lean | 52 +++++++++++++++++++++++---------
 2 files changed, 44 insertions(+), 19 deletions(-)

diff --git a/src/lake/Lake/Load/Main.lean b/src/lake/Lake/Load/Main.lean
index bdb7438675..b3200830d4 100644
--- a/src/lake/Lake/Load/Main.lean
+++ b/src/lake/Lake/Load/Main.lean
@@ -94,7 +94,7 @@ root dependencies. Otherwise, only update the root dependencies specified.
 
 If `reconfigure`, elaborate configuration files while updating, do not use OLeans.
 -/
-def buildUpdatedManifest (ws : Workspace)
+def Workspace.updateAndMaterialize (ws : Workspace)
 (toUpdate : NameSet := {}) (reconfigure := true) : LogIO Workspace := do
   let res ← StateT.run (s := mkOrdNameMap MaterializedDep) <| EStateT.run' (mkNameMap Package) do
     -- Use manifest versions of root packages that should not be updated
@@ -206,13 +206,16 @@ def loadWorkspace (config : LoadConfig) (updateDeps := false) : LogIO Workspace
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
   if updateDeps then
-    buildUpdatedManifest ws {} rc
+    ws.updateAndMaterialize {} rc
+  else if let some manifest ← Manifest.load? ws.manifestFile then
+    ws.materializeDeps manifest rc
   else
-    ws.materializeDeps (← Manifest.loadOrEmpty ws.manifestFile) rc
+    ws.updateAndMaterialize {} rc
+
 
 /-- Updates the manifest for the loaded Lake workspace (see `buildUpdatedManifest`). -/
 def updateManifest (config : LoadConfig) (toUpdate : NameSet := {}) : LogIO Unit := do
   let rc := config.reconfigure
   let ws ← loadWorkspaceRoot config
-  discard <| buildUpdatedManifest ws toUpdate rc
+  discard <| ws.updateAndMaterialize toUpdate rc
 
diff --git a/src/lake/Lake/Load/Manifest.lean b/src/lake/Lake/Load/Manifest.lean
index 2f454203f7..f536b8354a 100644
--- a/src/lake/Lake/Load/Manifest.lean
+++ b/src/lake/Lake/Load/Manifest.lean
@@ -8,6 +8,11 @@ import Lake.Util.Log
 
 open System Lean
 
+/-! # Lake Manifest
+The data structure of a Lake manifest and the definitions needed
+to create, modify, serialize, and deserialize it.
+-/
+
 namespace Lake
 
 instance [ToJson α] : ToJson (NameMap α) where
@@ -71,6 +76,7 @@ def empty : Manifest := {}
 @[inline] def isEmpty (self : Manifest) : Bool :=
   self.packages.isEmpty
 
+/-- Add a package entry to the end of a manifest. -/
 def addPackage (entry : PackageEntry) (self : Manifest) : Manifest :=
   {self with packages := self.packages.push entry}
 
@@ -107,26 +113,42 @@ protected def fromJson? (json : Json) : Except String Manifest := do
 
 instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 
-def loadFromFile (file : FilePath) : IO Manifest := do
-  let contents ← IO.FS.readFile file
-  match Json.parse contents with
+/-- Parse a `Manifest` from a string. -/
+def parse (s : String) : Except String Manifest := do
+  match Json.parse s with
   | .ok json =>
     match fromJson? json with
-    | .ok manifest =>
-      return manifest
-    | .error e =>
-      throw <| IO.userError <| s!"improperly formatted manifest: {e}"
-  | .error e =>
-    throw <| IO.userError <| s!"invalid JSON in manifest: {e}"
+    | .ok manifest => return manifest
+    | .error e => throw s!"improperly formatted manifest: {e}"
+  | .error e => throw s!"invalid JSON: {e}"
 
+/--
+Parse the manifest file. Returns `none` if the file does not exist.
+Errors if the manifest is ill-formatted or the read files for other reasons.
+-/
+def load? (file : FilePath) : IO (Option Manifest) := do
+  match (← IO.FS.readFile file |>.toBaseIO) with
+  | .ok contents =>
+    match inline <| Manifest.parse contents with
+    | .ok a => return some a
+    | .error e => error s!"{file}: {e}"
+  | .error (.noFileOrDirectory ..) => pure none
+  | .error e => throw e
+
+/--
+ Parse the manifest file or return an empty one.
+ Warn on any IO/parse errors if the file exists.
+-/
 def loadOrEmpty (file : FilePath) : LogIO Manifest := do
-  match (← loadFromFile file |>.toBaseIO) with
-  | .ok a => return a
-  | .error e =>
-    unless e matches .noFileOrDirectory .. do
-      logWarning (toString e)
-    return {}
+  match (← IO.FS.readFile file |>.toBaseIO) with
+  | .ok contents =>
+    match inline <| Manifest.parse contents with
+    | .ok a => return a
+    | .error e => logWarning s!"{file}: {e}"; pure {}
+  | .error (.noFileOrDirectory ..) => pure {}
+  | .error e => logWarning (toString e); pure {}
 
+/-- Save the manifest as JSON to a file. -/
 def saveToFile (self : Manifest) (manifestFile : FilePath) : IO PUnit := do
   let jsonString := Json.pretty self.toJson
   IO.FS.writeFile manifestFile <| jsonString.push '\n'