feat: lake: local package overrides

src/lake/Lake/CLI/Help.lean

@@ -46,6 +46,7 @@ BASIC OPTIONS:
   --old                 only rebuild modified modules (ignore transitive deps)
   --rehash, -H          hash all files for traces (do not trust `.hash` files)
   --update, -U          update dependencies on load (e.g., before a build)
+  --packages=file       JSON file of package entries that override the manifest
   --reconfigure, -R     elaborate configuration files instead of using OLeans
   --keep-toolchain      do not update toolchain on workspace update
   --no-build            exit immediately if a build target is not up-to-date

src/lake/Lake/CLI/Main.lean

@@ -34,6 +34,7 @@ structure LakeOptions where
   leanInstall? : Option LeanInstall := none
   lakeInstall? : Option LakeInstall := none
   configOpts : NameMap String := {}
+  packageOverrides : Array PackageEntry := #[]
   subArgs : List String := []
   wantsHelp : Bool := false
   verbosity : Verbosity := .normal
@@ -79,6 +80,7 @@ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=
     lakeEnv := ← opts.computeEnv
     wsDir := opts.rootDir
     relConfigFile := opts.configFile
+    packageOverrides := opts.packageOverrides
     lakeOpts := opts.configOpts
     leanOpts := Lean.Options.empty
     reconfigure := opts.reconfigure
@@ -196,6 +198,11 @@ def lakeLongOption : (opt : String) → CliM PUnit
   modifyThe LakeOptions ({· with failLv})
 | "--ansi"        => modifyThe LakeOptions ({· with ansiMode := .ansi})
 | "--no-ansi"     => modifyThe LakeOptions ({· with ansiMode := .noAnsi})
+| "--packages"    => do
+  let file ← takeOptArg "--packages" "package overrides file"
+  let overrides ← Manifest.loadEntries file
+  modifyThe LakeOptions fun opts =>
+    {opts with packageOverrides := opts.packageOverrides ++ overrides}
 | "--dir"         => do
   let rootDir ← takeOptArg "--dir" "path"
   modifyThe LakeOptions ({· with rootDir})

src/lake/Lake/Config/Workspace.lean

@@ -74,6 +74,10 @@ namespace Workspace
 @[inline] def manifestFile (self : Workspace) : FilePath :=
   self.root.manifestFile
 
+/-- The path to the workspace file used to configure automatic package overloads. -/
+@[inline] def packageOverridesFile (self : Workspace) : FilePath :=
+  self.lakeDir / "package-overrides.json"
+
 /-- Add a package to the workspace. -/
 def addPackage (pkg : Package) (self : Workspace) : Workspace :=
   {self with packages := self.packages.push pkg, packageMap := self.packageMap.insert pkg.name pkg}

src/lake/Lake/Load/Config.lean

@@ -6,10 +6,8 @@ Authors: Mac Malone
 prelude
 import Lean.Data.Name
 import Lean.Data.Options
-import Lake.Config.Defaults
 import Lake.Config.Env
-import Lake.Util.Log
-import Lake.Util.Version
+import Lake.Load.Manifest
 
 namespace Lake
 open System Lean
@@ -30,6 +28,8 @@ structure LoadConfig where
   relPkgDir : FilePath := "."
   /-- The package's Lake configuration file (relative to the package directory). -/
   relConfigFile : FilePath := defaultConfigFile
+  /-- Additional package overrides for this workspace load. -/
+  packageOverrides : Array PackageEntry := #[]
   /-- A set of key-value Lake configuration options (i.e., `-K` settings). -/
   lakeOpts : NameMap String := {}
   /-- The Lean options with which to elaborate the configuration file. -/

src/lake/Lake/Load/Manifest.lean

@@ -9,8 +9,7 @@ import Lake.Util.Name
 import Lake.Util.FilePath
 import Lake.Util.JsonObject
 import Lake.Util.Version
-import Lake.Load.Config
-import Lake.Config.Workspace
+import Lake.Config.Defaults
 
 open System Lean
 
@@ -191,37 +190,44 @@ protected def toJson (self : Manifest) : Json :=
 
 instance : ToJson Manifest := ⟨Manifest.toJson⟩
 
-protected def fromJson? (json : Json) : Except String Manifest := do
-  let obj ← JsonObject.fromJson? json
+def getVersion (obj : JsonObject) : Except String SemVerCore := do
+  let ver : Json ← obj.get "version" <|> obj.get "schemaVersion"
   let ver : SemVerCore ←
-    match (← obj.get "version" : Json) with
+    match ver with
     | (n : Nat) => pure {minor := n}
     | (s : String) => StdVer.parse s
-    | ver => throw s!"unknown manifest version format '{ver}'; \
+    | ver => throw s!"invalid version '{ver}'; \
       you may need to update your 'lean-toolchain'"
   if ver.major > 1 then
-    throw s!"manifest version '{ver}' is of a higher major version than this \
+    throw s!"schema version '{ver}' is of a higher major version than this \
       Lake's '{Manifest.version}'; you may need to update your 'lean-toolchain'"
   else if ver < {minor := 5} then
     throw s!"incompatible manifest version '{ver}'"
   else
-    let name ← obj.getD "name" Name.anonymous
-    let lakeDir ← obj.getD "lakeDir" defaultLakeDir
-    let packagesDir? ← obj.get? "packagesDir"
-    let packages ←
-      if ver < {minor := 7} then
-        (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
-      else
-        obj.getD "packages" #[]
-    return {name, lakeDir, packagesDir?, packages}
+    return ver
+
+def getPackages (ver : StdVer) (obj : JsonObject) : Except String (Array PackageEntry) := do
+  if ver < {minor := 7} then
+    (·.map PackageEntry.ofV6) <$> obj.getD "packages" #[]
+  else
+    obj.getD "packages" #[]
+
+protected def fromJson? (json : Json) : Except String Manifest := do
+  let obj ← JsonObject.fromJson? json
+  let ver ← getVersion obj
+  let name ← obj.getD "name" Name.anonymous
+  let lakeDir ← obj.getD "lakeDir" defaultLakeDir
+  let packagesDir? ← obj.get? "packagesDir"
+  let packages ← getPackages ver obj
+  return {name, lakeDir, packagesDir?, packages}
 
 instance : FromJson Manifest := ⟨Manifest.fromJson?⟩
 
 /-- Parse a `Manifest` from a string. -/
-def parse (s : String) : Except String Manifest := do
-  match Json.parse s with
+def parse (data : String) : Except String Manifest := do
+  match Json.parse data with
   | .ok json => fromJson? json
-  | .error e => throw s!"manifest is not valid JSON: {e}"
+  | .error e => throw s!"invalid JSON: {e}"
 
 /-- Parse a manifest file. -/
 def load (file : FilePath) : IO Manifest := do
@@ -240,7 +246,45 @@ def load? (file : FilePath) : IO (Option Manifest) := do
   | .error (.noFileOrDirectory ..) => return none
   | .error e => throw e
 
-/-- 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'
+/-- Serialize the manifest to a JSON file. -/
+def save (self : Manifest) (manifestFile : FilePath) : IO PUnit := do
+  let contents := Json.pretty self.toJson
+  IO.FS.writeFile manifestFile <| contents.push '\n'
+
+@[deprecated save (since := "2024-12-17")] abbrev saveToFile := @save
+
+/-- Deserialize package entries from a (partial) JSON manifest. -/
+def decodeEntries (data : Json)  : Except String (Array PackageEntry) := do
+  let obj ← JsonObject.fromJson? data
+  getPackages (← getVersion obj) obj
+
+/-- Deserialize manifest package entries from a JSON string. -/
+def parseEntries (data : String) : Except String (Array PackageEntry) := do
+  match Json.parse data with
+  | .ok json => decodeEntries json
+  | .error e => throw s!"invalid JSON: {e}"
+
+/-- Deserialize manifest package entries from a JSON file. -/
+def loadEntries (file : FilePath) : IO (Array PackageEntry) := do
+  let contents ← IO.FS.readFile file
+  match inline <| parseEntries contents with
+  | .ok a => return a
+  | .error e => error s!"{file}: {e}"
+
+/--
+Deserialize manifest package entries from a JSON file.
+Returns an empty array if the file does not exist.
+-/
+def tryLoadEntries (file : FilePath) : IO (Array PackageEntry) := do
+  match  (← inline (loadEntries file) |>.toBaseIO) with
+  | .ok a => return a
+  | .error (.noFileOrDirectory ..) => return #[]
+  | .error e => error s!"{file}: {e}"
+
+/-- Serialize manifest package entries to a JSON file. -/
+def saveEntries (file : FilePath) (entries : Array PackageEntry)  : IO PUnit := do
+  let contents := Json.pretty <| Json.mkObj [
+    ("schemaVersion", toJson version),
+    ("packages", toJson entries)
+  ]
+  IO.FS.writeFile file <| contents.push '\n'

src/lake/Lake/Load/Resolve.lean

@@ -373,7 +373,7 @@ def Workspace.writeManifest
     packagesDir? := ws.relPkgsDir
     packages := manifestEntries
   }
-  manifest.saveToFile ws.manifestFile
+  manifest.save ws.manifestFile
 
 /-- Run a package's `post_update` hooks. -/
 def Package.runPostUpdateHooks (pkg : Package) : LakeT LoggerIO PUnit := do
@@ -399,15 +399,12 @@ def Workspace.updateAndMaterialize
   return ws
 
 /--
-Check whether the manifest exists and
-whether entries in the manifest are up-to-date,
+Check whether entries in the manifest are up-to-date,
 reporting warnings and/or errors as appropriate.
 -/
 def validateManifest
   (pkgEntries : NameMap PackageEntry) (deps : Array Dependency)
 : LoggerIO PUnit := do
-  if pkgEntries.isEmpty && !deps.isEmpty then
-    error "missing manifest; use `lake update` to generate one"
   deps.forM fun dep => do
     let warnOutOfDate (what : String) :=
       logWarning <|
@@ -429,16 +426,27 @@ downloading and/or updating them as necessary.
 def Workspace.materializeDeps
   (ws : Workspace) (manifest : Manifest)
   (leanOpts : Options := {}) (reconfigure := false)
+  (overrides : Array PackageEntry := #[])
 : LoggerIO Workspace := do
+  -- Load locked dependencies
   if !manifest.packages.isEmpty && manifest.packagesDir? != some (mkRelPathString ws.relPkgsDir) then
     logWarning <|
       "manifest out of date: packages directory changed; \
       use `lake update` to rebuild the manifest \
       (warning: this will update ALL workspace dependencies)"
   let relPkgsDir := manifest.packagesDir?.getD ws.relPkgsDir
-  let pkgEntries : NameMap PackageEntry := manifest.packages.foldl (init := {})
-    fun map entry => map.insert entry.name entry
+  let mut pkgEntries := mkNameMap PackageEntry
+  pkgEntries := manifest.packages.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
   validateManifest pkgEntries ws.root.depConfigs
+  let wsOverrides ← Manifest.tryLoadEntries ws.packageOverridesFile
+  pkgEntries := wsOverrides.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
+  pkgEntries := overrides.foldl (init := pkgEntries) fun map entry =>
+    map.insert entry.name entry
+  if pkgEntries.isEmpty && !ws.root.depConfigs.isEmpty then
+    error "missing manifest; use `lake update` to generate one"
+  -- Materialize all dependencies
   let ws := ws.addPackage ws.root
   ws.resolveDepsCore fun pkg dep => do
     let ws ← getWorkspace

src/lake/Lake/Load/Workspace.lean

@@ -44,12 +44,12 @@ elaborating its configuration file and resolving its dependencies.
 If `updateDeps` is true, updates the manifest before resolving dependencies.
 -/
 def loadWorkspace (config : LoadConfig) : LoggerIO Workspace := do
-  let {reconfigure, leanOpts, updateDeps, updateToolchain, ..} := config
+  let {reconfigure, leanOpts, updateDeps, updateToolchain, packageOverrides, ..} := config
   let ws ← loadWorkspaceRoot config
   if updateDeps then
     ws.updateAndMaterialize {} leanOpts updateToolchain
   else if let some manifest ← Manifest.load? ws.manifestFile then
-    ws.materializeDeps manifest leanOpts reconfigure
+    ws.materializeDeps manifest leanOpts reconfigure packageOverrides
   else
     ws.updateAndMaterialize {} leanOpts updateToolchain
 

src/lake/Lake/Util/Version.lean

@@ -101,7 +101,7 @@ def StdVer.parse (ver : String) : Except String StdVer := do
     let core ← SemVerCore.parse <| ver.extract 0 sepPos
     let specialDescr := ver.extract (ver.next' sepPos h) ver.endPos
     if specialDescr.isEmpty then
-      throw "invalid Lean version: '-' suffix cannot be empty"
+      throw "invalid version: '-' suffix cannot be empty"
     return {toSemVerCore := core, specialDescr}
 
 protected def StdVer.toString (ver : StdVer) : String :=

src/lake/tests/packageOverrides/bar1/Bar.lean

@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println "Hello from bar1"

src/lake/tests/packageOverrides/bar1/lakefile.toml

@@ -0,0 +1,4 @@
+name = "bar"
+
+[[lean_exe]]
+name = "bar"

src/lake/tests/packageOverrides/bar2/Bar.lean

@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println "Hello from bar2"

src/lake/tests/packageOverrides/bar2/lakefile.toml

@@ -0,0 +1,4 @@
+name = "bar"
+
+[[lean_exe]]
+name = "bar"

src/lake/tests/packageOverrides/clean.sh

@@ -0,0 +1,2 @@
+rm -rf bar1/.git bar2/.lake .lake
+rm -f lake-manifest.json

src/lake/tests/packageOverrides/foo/Foo.lean

@@ -0,0 +1,2 @@
+def main : IO Unit :=
+  IO.println "Hello from foo"

src/lake/tests/packageOverrides/foo/lakefile.toml

@@ -0,0 +1,4 @@
+name = "foo"
+
+[[lean_exe]]
+name = "foo"

src/lake/tests/packageOverrides/lakefile.lean

@@ -0,0 +1,9 @@
+import Lake
+open System Lake DSL
+
+package test
+
+meta if get_config? foo |>.isSome then
+require "leanprover" / "foo"
+
+require bar from git "bar1"

src/lake/tests/packageOverrides/packages.json

@@ -0,0 +1,15 @@
+{"schemaVersion": "1.1.0",
+ "packages":
+ [{"type": "path",
+   "dir": "bar2",
+   "name": "bar",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+   {"type": "path",
+   "dir": "foo",
+   "scope": "leanprover",
+   "name": "foo",
+   "manifestFile": "lake-manifest.json",
+   "inherited": false,
+   "configFile": "lakefile.toml"}]}

src/lake/tests/packageOverrides/test.sh

@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+set -exo pipefail
+
+LAKE=${LAKE:-../../.lake/build/bin/lake}
+
+./clean.sh
+
+# Since committing a Git repository to a Git repository is not well-supported,
+# We reinitialize the `bar1` repository on each test.
+pushd bar1
+git init
+git checkout -b master
+git config user.name test
+git config user.email test@example.com
+git add --all
+git commit -m "initial commit"
+popd
+
+$LAKE resolve-deps -R
+$LAKE exe bar | grep --color "bar1"
+
+$LAKE resolve-deps -R -Kfoo --packages=packages.json
+$LAKE --packages=packages.json exe bar  | grep --color "bar2"
+$LAKE --packages=packages.json exe foo  | grep --color "foo"
+
+$LAKE resolve-deps -R
+$LAKE exe bar | grep --color "bar1"
+
+cp packages.json .lake/package-overrides.json
+$LAKE resolve-deps -R -Kfoo
+$LAKE exe bar | grep --color "bar2"
+$LAKE exe foo | grep --color "foo"