feat: lake: create manifest on load if missing

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
 

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'

src/lake/tests/autoManifest/.gitignore

@@ -0,0 +1,2 @@
+lakefile.olean
+lake-manifest.json

src/lake/tests/autoManifest/clean.sh

@@ -0,0 +1 @@
+rm -f lake-manifest.json lakefile.olean foo/lakefile.olean

src/lake/tests/autoManifest/foo/lakefile.lean

@@ -0,0 +1,4 @@
+import Lake
+open Lake DSL
+
+package foo

src/lake/tests/autoManifest/lakefile.lean

@@ -0,0 +1,5 @@
+import Lake
+open Lake DSL
+
+package bar
+require foo from "foo"

src/lake/tests/autoManifest/test.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+set -euxo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+./clean.sh
+
+# Tests that build produces a manifest if there is none.
+# Related: https://github.com/leanprover/lean4/issues/2549
+
+$LAKE build
+test -f lake-manifest.json