feat: LAKE_PKG_URL_MAP

src/lake/Lake/CLI/Error.lean

@@ -37,6 +37,7 @@ inductive CliError
 | unknownLeanInstall
 | unknownLakeInstall
 | leanRevMismatch (expected actual : String)
+| invalidEnv (msg : String)
 deriving Inhabited, Repr
 
 namespace CliError
@@ -66,5 +67,6 @@ def toString : CliError → String
 | unknownLeanInstall      => "could not detect a Lean installation"
 | unknownLakeInstall      => "could not detect the configuration of the Lake installation"
 | leanRevMismatch e a     => s!"expected Lean commit {e}, but got {if a.isEmpty then "nothing" else a}"
+| invalidEnv msg          => msg
 
 instance : ToString CliError := ⟨toString⟩

src/lake/Lake/CLI/Main.lean

@@ -59,6 +59,7 @@ def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall
 /-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
 def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
   Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall?
+    |>.adaptExcept fun msg => .invalidEnv msg
 
 /-- Make a `LoadConfig` from a `LakeOptions`. -/
 def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig :=

src/lake/Lake/CLI/Serve.lean

@@ -58,7 +58,7 @@ def serve (config : LoadConfig) (args : Array String) : IO UInt32 := do
       pure (← LakeT.run ctx getAugmentedEnv, ws.root.moreServerArgs)
     else
       IO.eprintln "warning: package configuration has errors, falling back to plain `lean --server`"
-      pure (config.env.installVars.push (invalidConfigEnvVar, log), #[])
+      pure (config.env.baseVars.push (invalidConfigEnvVar, log), #[])
   (← IO.Process.spawn {
     cmd := config.env.lean.lean.toString
     args := #["--server"] ++ moreServerArgs ++ args

src/lake/Lake/Config/Env.lean

@@ -3,10 +3,11 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
+import Lake.Util.Name
 import Lake.Util.NativeLib
 import Lake.Config.InstallPath
 
-open System
+open System Lean
 
 /-! # Lake's Environment
 Definitions related to a Lake environment.
@@ -24,6 +25,8 @@ structure Env where
   lean : LeanInstall
   /-- The Elan installation (if any) of the environment. -/
   elan? : Option ElanInstall
+  /-- A name-to-URL mapping of URL overwrites for the named packages. -/
+  pkgUrlMap : NameMap String
   /-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/
   initToolchain : String
   /-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/
@@ -34,20 +37,27 @@ structure Env where
   initSharedLibPath : SearchPath
   /-- The initial binary search path of the environment (i.e., `PATH`). -/
   initPath : SearchPath
-  deriving Inhabited, Repr
+  deriving Inhabited
 
 namespace Env
 
 /-- Compute an `Lake.Env` object from the given installs and set environment variables. -/
-def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : BaseIO Env :=
+def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : EIO String Env :=
   return {
     lake, lean, elan?,
+    pkgUrlMap := ← computePkgUrlMap
     initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD ""
     initLeanPath := ← getSearchPath "LEAN_PATH",
     initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH",
     initSharedLibPath := ← getSearchPath sharedLibPathEnvVar,
     initPath := ← getSearchPath "PATH"
   }
+where
+  computePkgUrlMap := do
+    let some urlMapStr ← IO.getEnv "LAKE_PKG_URL_MAP" | return {}
+    match Json.parse urlMapStr |>.bind fromJson? with
+    | .ok urlMap => return urlMap
+    | .error e => throw s!"'LAKE_PKG_URL_MAP' has invalid JSON: {e}"
 
 /--
 The preferred toolchain of the environment. May be empty.
@@ -95,13 +105,14 @@ Combines the initial path of the environment with that of the Lean installation.
 def sharedLibPath (env : Env) : SearchPath :=
   env.lean.sharedLibPath ++ env.initSharedLibPath
 
-/-- Environment variable settings based only on the Elan/Lean/Lake installations. -/
-def installVars (env : Env) : Array (String × Option String)  :=
+/-- Environment variable settings that are not augmented by a Lake workspace. -/
+def baseVars (env : Env) : Array (String × Option String)  :=
   #[
     ("ELAN_HOME", env.elan?.map (·.home.toString)),
     ("ELAN_TOOLCHAIN", if env.toolchain.isEmpty then none else env.toolchain),
     ("LAKE", env.lake.lake.toString),
     ("LAKE_HOME", env.lake.home.toString),
+    ("LAKE_PKG_URL_MAP", toJson env.pkgUrlMap |>.compress),
     ("LEAN_SYSROOT", env.lean.sysroot.toString),
     ("LEAN_AR", env.lean.ar.toString),
     ("LEAN_CC", env.lean.leanCc?)
@@ -109,7 +120,7 @@ def installVars (env : Env) : Array (String × Option String)  :=
 
 /-- Environment variable settings for the `Lake.Env`. -/
 def vars (env : Env) : Array (String × Option String)  :=
-  let vars := env.installVars ++ #[
+  let vars := env.baseVars ++ #[
     ("LEAN_PATH", some env.leanPath.toString),
     ("LEAN_SRC_PATH", some env.leanSrcPath.toString),
     ("PATH", some env.path.toString)

src/lake/Lake/Config/Monad.lean

@@ -19,16 +19,22 @@ namespace Lake
 abbrev MonadLakeEnv (m : Type → Type u) :=
   MonadReaderOf Lake.Env m
 
+/-- A transformer to equip a monad with a `Lake.Env`. -/
+abbrev LakeEnvT := ReaderT Lake.Env
+
+@[inline] def LakeEnvT.run (env : Lake.Env) (self : LakeEnvT m α) : m α :=
+  ReaderT.run self env
+
 /-- A monad equipped with a (read-only) Lake `Workspace`. -/
 abbrev MonadWorkspace (m : Type → Type u) :=
   MonadReaderOf Workspace m
 
 /-- A monad equipped with a (read-only) Lake context. -/
 abbrev MonadLake (m : Type → Type u) :=
-  MonadReaderOf Context m
+  MonadReaderOf Lake.Context m
 
 /-- Make a `Lake.Context` from a `Workspace`. -/
-@[inline] def mkLakeContext (ws : Workspace) : Context where
+@[inline] def mkLakeContext (ws : Workspace) : Lake.Context where
   opaqueWs := ws
 
 instance [MonadWorkspace m] [Functor m] : MonadLake m where
@@ -109,13 +115,19 @@ def findExternLib? (name : Name) : m (Option ExternLib) :=
 end
 
 section
-variable [MonadLakeEnv m] [Functor m]
+variable [MonadLakeEnv m]
 
 /-! ## Environment Helpers -/
 
 @[inline] def getLakeEnv : m Lake.Env :=
   read
 
+variable [Functor m]
+
+/-- Get the `LAKE_PACKAGE_URL_MAP` for the Lake environment. Empty if none. -/
+@[inline] def getPkgUrlMap : m (NameMap String) :=
+  (·.pkgUrlMap) <$> getLakeEnv
+
 /-- Get the name of Elan toolchain for the Lake environment. Empty if none. -/
 @[inline] def getElanToolchain : m String :=
   (·.toolchain) <$> getLakeEnv

src/lake/Lake/Config/Workspace.lean

@@ -176,7 +176,7 @@ The detected environment augmented with Lake's and the workspace's paths.
 These are the settings use by `lake env` / `Lake.env` to run executables.
 -/
 def augmentedEnvVars (self : Workspace) : Array (String × Option String) :=
-  let vars := self.lakeEnv.installVars ++ #[
+  let vars := self.lakeEnv.baseVars ++ #[
     ("LEAN_PATH", some self.augmentedLeanPath.toString),
     ("LEAN_SRC_PATH", some self.augmentedLeanSrcPath.toString),
     ("PATH", some self.augmentedPath.toString)

src/lake/Lake/Load/Main.lean

@@ -101,14 +101,14 @@ def Workspace.updateAndMaterialize (ws : Workspace)
     unless toUpdate.isEmpty do
       for entry in (← Manifest.loadOrEmpty ws.manifestFile) do
         unless entry.inherited || toUpdate.contains entry.name do
-          let dep ← entry.materialize ws.dir ws.relPkgsDir
+          let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
           modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
     buildAcyclic (·.1.name) (ws.root, FilePath.mk ".") fun (pkg, relPkgDir) resolve => do
       let inherited := pkg.name != ws.root.name
       let deps ← IO.ofExcept <| loadDepsFromEnv pkg.configEnv pkg.leanOpts
       -- Materialize this package's dependencies first
       let deps ← deps.mapM fun dep => fetchOrCreate dep.name do
-        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir
+        dep.materialize inherited ws.dir ws.relPkgsDir relPkgDir ws.lakeEnv.pkgUrlMap
       -- Load dependency packages and materialize their locked dependencies
       let deps ← deps.mapM fun dep => do
         if let .some pkg := (← getThe (NameMap Package)).find? dep.name then
@@ -122,7 +122,7 @@ def Workspace.updateAndMaterialize (ws : Workspace)
           for entry in (← Manifest.loadOrEmpty depPkg.manifestFile) do
             unless (← getThe (OrdNameMap MaterializedDep)).contains entry.name do
               let entry := entry.setInherited.inDirectory dep.relPkgDir
-              let dep ← entry.materialize ws.dir ws.relPkgsDir
+              let dep ← entry.materialize ws.dir ws.relPkgsDir ws.lakeEnv.pkgUrlMap
               modifyThe (OrdNameMap MaterializedDep) (·.insert entry.name dep)
           modifyThe (NameMap Package) (·.insert dep.name depPkg)
           return (depPkg, dep.relPkgDir)
@@ -176,7 +176,7 @@ def Workspace.materializeDeps (ws : Workspace) (manifest : Manifest) (reconfigur
           | _, _ => warnOutOfDate "source kind (git/path)"
       let depPkgs ← deps.mapM fun dep => fetchOrCreate dep.name do
         if let some entry := pkgEntries.find? dep.name then
-          let result ← entry.materialize ws.dir relPkgsDir
+          let result ← entry.materialize ws.dir relPkgsDir ws.lakeEnv.pkgUrlMap
           -- Union manifest and configuration options (preferring manifest)
           let opts := entry.opts.mergeBy (fun _ e _ => e) dep.opts
           loadDepPackage ws.dir result pkg.leanOpts opts reconfigure

src/lake/Lake/Load/Manifest.lean

@@ -3,8 +3,8 @@ Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone, Gabriel Ebner
 -/
-import Lean.Data.Json
 import Lake.Util.Log
+import Lake.Util.Name
 
 open System Lean
 
@@ -15,18 +15,6 @@ to create, modify, serialize, and deserialize it.
 
 namespace Lake
 
-instance [ToJson α] : ToJson (NameMap α) where
-  toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf
-
-instance [FromJson α] : FromJson (NameMap α) where
-  fromJson? j := do
-    (← j.getObj?).foldM (init := {}) fun m k v =>
-      let k := k.toName
-      if k.isAnonymous then
-        throw "expected name"
-      else
-        return m.insert k (← fromJson? v)
-
 /-- Current version of the manifest format. -/
 def Manifest.version : Nat := 6
 

src/lake/Lake/Load/Materialize.lean

@@ -19,7 +19,7 @@ or resolve a local path dependency.
 namespace Lake
 
 /-- Update the Git package in `repo` to `rev` if not already at it. -/
-def updateGitPkg (repo : GitRepo) (rev? : Option String) (name : String) : LogIO PUnit := do
+def updateGitPkg (name : String) (repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
   let rev ← repo.findRemoteRevision rev?
   if (← repo.getHeadRevision) = rev then
     if (← repo.hasDiff) then
@@ -29,8 +29,9 @@ def updateGitPkg (repo : GitRepo) (rev? : Option String) (name : String) : LogIO
     repo.checkoutDetach rev
 
 /-- Clone the Git package as `repo`. -/
-def cloneGitPkg (repo : GitRepo) (url : String) (rev? : Option String) : LogIO PUnit := do
-  logInfo s!"cloning {url} to {repo}"
+def cloneGitPkg (name : Name) (repo : GitRepo)
+(url : String) (rev? : Option String) : LogIO PUnit := do
+  logInfo s!"{name}: cloning {url} to '{repo.dir}'"
   repo.clone url
   if let some rev := rev? then
     let hash ← repo.resolveRemoteRevision rev
@@ -41,34 +42,34 @@ Update the Git repository from `url` in `repo` to `rev?`.
 If `repo` is already from `url`, just checkout the new revision.
 Otherwise, delete the local repository and clone a fresh copy from `url`.
 -/
-def updateGitRepo (repo : GitRepo) (url : String)
-(rev? : Option String) (name : String) : LogIO Unit := do
+def updateGitRepo (name : String) (repo : GitRepo)
+(url : String) (rev? : Option String) : LogIO Unit := do
   let sameUrl ← EIO.catchExceptions (h := fun _ => pure false) <| show IO Bool from do
     let some remoteUrl ← repo.getRemoteUrl? | return false
     if remoteUrl = url then return true
     return (← IO.FS.realPath remoteUrl) = (← IO.FS.realPath url)
   if sameUrl then
-    updateGitPkg repo rev? name
+    updateGitPkg name repo rev?
   else
     if System.Platform.isWindows then
       -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on windows
       logInfo s!"{name}: URL has changed; you might need to delete '{repo.dir}' manually"
-      updateGitPkg repo rev? name
+      updateGitPkg name repo rev?
     else
       logInfo s!"{name}: URL has changed; deleting '{repo.dir}' and cloning again"
       IO.FS.removeDirAll repo.dir
-      cloneGitPkg repo url rev?
+      cloneGitPkg name repo url rev?
 
 /--
 Materialize the Git repository from `url` into `repo` at `rev?`.
 Clone it if no local copy exists, otherwise update it.
 -/
-def materializeGitRepo (repo : GitRepo) (url : String)
-(rev? : Option String) (name : String) : LogIO Unit := do
+def materializeGitRepo (name : String) (repo : GitRepo)
+(url : String) (rev? : Option String) : LogIO Unit := do
   if (← repo.dirExists) then
-    updateGitRepo repo url rev? name
+    updateGitRepo name repo url rev?
   else
-    cloneGitPkg repo url rev?
+    cloneGitPkg name repo url rev?
 
 structure MaterializedDep where
   /-- Path to the materialized package relative to the workspace's root directory. -/
@@ -88,7 +89,8 @@ Materializes a configuration dependency.
 For Git dependencies, updates it to the latest input revision.
 -/
 def Dependency.materialize (dep : Dependency) (inherited : Bool)
-(wsDir relPkgsDir relParentDir : FilePath) : LogIO MaterializedDep :=
+(wsDir relPkgsDir relParentDir : FilePath) (pkgUrlMap : NameMap String)
+: LogIO MaterializedDep :=
   match dep.src with
   | .path dir =>
     let relPkgDir := relParentDir / dir
@@ -98,10 +100,11 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
       manifestEntry := .path dep.name dep.opts inherited relPkgDir
     }
   | .git url inputRev? subDir? => do
-    let name := dep.name.toString (escape := false)
-    let relGitDir := relPkgsDir / name
+    let sname := dep.name.toString (escape := false)
+    let relGitDir := relPkgsDir / sname
     let repo := GitRepo.mk (wsDir / relGitDir)
-    materializeGitRepo repo url inputRev? name
+    let materializeUrl := pkgUrlMap.find? dep.name |>.getD url
+    materializeGitRepo sname repo materializeUrl inputRev?
     let rev ← repo.getHeadRevision
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
@@ -111,8 +114,10 @@ def Dependency.materialize (dep : Dependency) (inherited : Bool)
     }
 
 /--
-Materializes a manifest package entry, cloning and/or checking it out as necessary. -/
-def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : PackageEntry) : LogIO MaterializedDep :=
+Materializes a manifest package entry, cloning and/or checking it out as necessary.
+-/
+def PackageEntry.materialize (manifestEntry : PackageEntry)
+(wsDir relPkgsDir : FilePath) (pkgUrlMap : NameMap String) : LogIO MaterializedDep :=
   match manifestEntry with
   | .path _name _opts _inherited relPkgDir =>
     return {
@@ -121,8 +126,8 @@ def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : Pack
       manifestEntry
     }
   | .git name _opts _inherited url rev _inputRev? subDir? => do
-    let name := name.toString (escape := false)
-    let relGitDir := relPkgsDir / name
+    let sname := name.toString (escape := false)
+    let relGitDir := relPkgsDir / sname
     let gitDir := wsDir / relGitDir
     let repo := GitRepo.mk gitDir
     /-
@@ -134,11 +139,13 @@ def PackageEntry.materialize (wsDir relPkgsDir : FilePath) (manifestEntry : Pack
     if (← repo.dirExists) then
       if (← repo.getHeadRevision?) = rev then
         if (← repo.hasDiff) then
-          logWarning s!"{name}: repository '{repo.dir}' has local changes"
+          logWarning s!"{sname}: repository '{repo.dir}' has local changes"
       else
-        updateGitRepo repo url rev name
+        let url := pkgUrlMap.find? name |>.getD url
+        updateGitRepo sname repo url rev
     else
-      cloneGitPkg repo url rev
+      let url := pkgUrlMap.find? name |>.getD url
+      cloneGitPkg sname repo url rev
     let relPkgDir := match subDir? with | .some subDir => relGitDir / subDir | .none => relGitDir
     return {
       relPkgDir

src/lake/Lake/Util/Name.lean

@@ -3,6 +3,7 @@ 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
 import Lean.Data.NameMap
 import Lake.Util.DRBMap
 import Lake.Util.RBArray
@@ -28,6 +29,18 @@ abbrev OrdNameMap α := RBArray Name α Name.quickCmp
 abbrev DNameMap α := DRBMap Name α Name.quickCmp
 @[inline] def DNameMap.empty : DNameMap α := DRBMap.empty
 
+instance [ToJson α] : ToJson (NameMap α) where
+  toJson m := Json.obj <| m.fold (fun n k v => n.insert compare k.toString (toJson v)) .leaf
+
+instance [FromJson α] : FromJson (NameMap α) where
+  fromJson? j := do
+    (← j.getObj?).foldM (init := {}) fun m k v =>
+      let k := k.toName
+      if k.isAnonymous then
+        throw "expected name"
+      else
+        return m.insert k (← fromJson? v)
+
 /-! # Name Helpers -/
 
 namespace Name

src/lake/tests/clone/test.sh

@@ -23,22 +23,23 @@ git add --all
 git commit -m "initial commit"
 popd
 
-HELLO_URL="file://$(pwd)/hello"
+HELLO_MAP="{\"hello\" : \"file://$(pwd)/hello\"}"
 
 cd test
 
-$LAKE -R -Kurl="$HELLO_URL" update
+# test that `LAKE_PKG_URL_MAP` properly overwrites the config-specified Git URL
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | grep "file://"
 # test that a second `lake update` is a no-op (with URLs)
 # see https://github.com/leanprover/lean4/commit/6176fdba9e5a888225a23e5d558a005e0d1eb2f6#r125905901
-$LAKE -R -Kurl="$HELLO_URL" update | diff - /dev/null
+LAKE_PKG_URL_MAP=$HELLO_MAP $LAKE update | diff - /dev/null
 rm -rf lake-packages
 
 # Test that Lake produces no warnings on a `lake build` after a `lake update`
 # See https://github.com/leanprover/lean4/issues/2427
 
-$LAKE -R update
+$LAKE update
 # test that a second `lake update` is a no-op (with file paths)
-$LAKE -R update | diff - /dev/null
+$LAKE update | diff - /dev/null
 test -d lake-packages/hello
 # test that Lake produces no warnings
 $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
@@ -58,13 +59,10 @@ $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null
 # See https://github.com/leanprover/lake/issues/104
 
 TEST_URL=https://example.com/hello.git
-MANIFEST=lake-manifest.json
+TEST_MAP="{\"hello\" : \"$TEST_URL\"}"
 
-cat $MANIFEST
-sed_i "s,\\.\\.[^\"]*,$TEST_URL," $MANIFEST
-cat $MANIFEST
 # set invalid remote
 git -C lake-packages/hello remote set-url origin $TEST_URL
 # build should succeed (do nothing) despite the invalid remote because
 # the remote should not be fetched; Lake should also not produce any warnings
-$LAKE build -R -Kurl=$TEST_URL 3>&1 1>&2 2>&3 | diff - /dev/null
+LAKE_PKG_URL_MAP=$TEST_MAP $LAKE build 3>&1 1>&2 2>&3 | diff - /dev/null

src/lake/tests/clone/test/lakefile.lean

@@ -4,12 +4,7 @@ open System Lake DSL
 
 package test
 
-def url : String :=
-  match get_config? url with
-  | some url => url
-  | none => (FilePath.mk ".." / "hello").toString
-
-require hello from git url
+require hello from git "../hello"
 
 @[default_target]
 lean_exe test {

src/lake/tests/env/test.sh

@@ -26,6 +26,11 @@ test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = fo
 test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo
 test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo
 
+# Test `LAKE_PKG_URL_MAP` setting and errors
+test "`LAKE_PKG_URL_MAP='{"a":"a"}' $LAKE env printenv LAKE_PKG_URL_MAP`" = '{"a":"a"}'
+(LAKE_PKG_URL_MAP=foo $LAKE env 2>&1 || true) | grep invalid
+(LAKE_PKG_URL_MAP=0 $LAKE env 2>&1 || true) | grep invalid
+
 # Test that the platform-specific shared library search path is set
 if [ "$OS" = Windows_NT ]; then
 $LAKE env which libleanshared.dll # DLL in `bin` directory is in `PATH`