feat: lake: rename dependencies (#10452)

This PR refactors Lake's package naming procedure to allow packages to
be renamed by the consumer. With this, users can now require a package
using a different name than the one it was defined with.

This is support will be used in the future to enable seamlessly
including the same package at multiple different versions within the
same workspace.

In a Lake package configuration file written in Lean, the current
package's assigned name is now accessed through `__name__` instead of
the previous `_package.name`. A deprecation warning has been added to
`_package.name` to assist in migration.

src/lake/Lake/CLI/Translate/Lean.lean

@@ -279,11 +279,13 @@ def Dependency.mkRequire (cfg : Dependency) : RequireDecl := Unhygienic.run do
 
 private meta def genMkDeclFields
   (cmds : Array Command)
-  (tyName : Name) [info : ConfigInfo tyName] (takesName : Bool)
+  (tyName : Name) [info : ConfigInfo tyName]
   (exclude : Array Name := #[])
 : MacroM (Array Command) := do
   let val ← `(fs)
-  let ty := if takesName then Syntax.mkCApp tyName #[mkIdent `n] else mkCIdent tyName
+  let tyArgs := info.arity.fold (init := Array.emptyWithCapacity info.arity) fun i _ as =>
+    as.push (mkIdent <| .mkSimple s!"x_{i+1}")
+  let ty := Syntax.mkCApp tyName tyArgs
   let val ← info.fields.foldlM (init := val) fun val {name, canonical, ..} => do
     if !canonical || exclude.contains name then
       return val
@@ -298,21 +300,21 @@ private meta def genMkDeclFields
 local macro "gen_lean_encoders%" : command => do
   let cmds := #[]
   -- Targets
-  let cmds ← genMkDeclFields cmds ``LeanConfig false
-  let cmds ← genMkDeclFields cmds ``LeanLibConfig true
+  let cmds ← genMkDeclFields cmds ``LeanConfig
+  let cmds ← genMkDeclFields cmds ``LeanLibConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genMkDeclFields cmds ``LeanExeConfig true
+  let cmds ← genMkDeclFields cmds ``LeanExeConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genMkDeclFields cmds ``InputFileConfig true
-  let cmds ← genMkDeclFields cmds ``InputDirConfig true
+  let cmds ← genMkDeclFields cmds ``InputFileConfig
+  let cmds ← genMkDeclFields cmds ``InputDirConfig
   -- Package
-  let cmds ← genMkDeclFields cmds ``WorkspaceConfig false
-  let cmds ← genMkDeclFields cmds ``PackageConfig true
+  let cmds ← genMkDeclFields cmds ``WorkspaceConfig
+  let cmds ← genMkDeclFields cmds ``PackageConfig
   return ⟨mkNullNode cmds⟩
 
 gen_lean_encoders%
 
-def PackageConfig.mkCommand (cfg : PackageConfig n) : PackageCommand := Unhygienic.run do
+def PackageConfig.mkCommand (cfg : PackageConfig p n) : PackageCommand := Unhygienic.run do
   let declVal? := mkDeclValWhere? (mkDeclFields cfg)
   `(packageCommand|package $(mkIdent n):ident $[$declVal?]?)
 
@@ -355,7 +357,7 @@ protected def InputDirConfig.mkCommand
 
 /-- Create a Lean module that encodes the declarative configuration of the package. -/
 public def Package.mkLeanConfig (pkg : Package) : TSyntax ``module := Unhygienic.run do
-  let pkgConfig : PackageConfig pkg.name :=
+  let pkgConfig : PackageConfig pkg.name pkg.origName :=
     {pkg.config with testDriver := pkg.testDriver, lintDriver := pkg.lintDriver}
   let defaultTargets := pkg.defaultTargets.foldl NameSet.insert NameSet.empty
   `(module|

src/lake/Lake/CLI/Translate/Toml.lean

@@ -151,11 +151,14 @@ public instance : ToToml Dependency := ⟨(toToml ·.toToml)⟩
 
 private meta def genToToml
   (cmds : Array Command)
-  (tyName : Name) [info : ConfigInfo tyName] (takesName : Bool)
+  (tyName : Name) [info : ConfigInfo tyName]
   (exclude : Array Name := #[])
 : MacroM (Array Command) := do
-  let val ← if takesName then `(t.insert `name $(mkIdent `n)) else `(t)
-  let ty := if takesName then Syntax.mkCApp tyName #[mkIdent `n] else mkCIdent tyName
+  let val ← if info.arity == 0 then `(t) else
+    `(t.insert `name $(mkIdent <| .mkSimple s!"x_{info.arity}"))
+  let tyArgs := info.arity.fold (init := Array.emptyWithCapacity info.arity) fun i _ as =>
+    as.push (mkIdent <| .mkSimple s!"x_{i+1}")
+  let ty := Syntax.mkCApp tyName tyArgs
   let val ← info.fields.foldlM (init := val) fun val {name, canonical, ..} => do
     if !canonical || exclude.contains name then
       return val
@@ -170,16 +173,16 @@ private meta def genToToml
 local macro "gen_toml_encoders%" : command => do
   let cmds := #[]
   -- Targets
-  let cmds ← genToToml cmds ``LeanConfig false
-  let cmds ← genToToml cmds ``LeanLibConfig true
+  let cmds ← genToToml cmds ``LeanConfig
+  let cmds ← genToToml cmds ``LeanLibConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genToToml cmds ``LeanExeConfig true
+  let cmds ← genToToml cmds ``LeanExeConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genToToml cmds ``InputFileConfig true
-  let cmds ← genToToml cmds ``InputDirConfig true
+  let cmds ← genToToml cmds ``InputFileConfig
+  let cmds ← genToToml cmds ``InputDirConfig
   -- Package
-  let cmds ← genToToml cmds ``WorkspaceConfig false
-  let cmds ← genToToml cmds ``PackageConfig true
+  let cmds ← genToToml cmds ``WorkspaceConfig
+  let cmds ← genToToml cmds ``PackageConfig
   return ⟨mkNullNode cmds⟩
 
 gen_toml_encoders%
@@ -194,7 +197,7 @@ gen_toml_encoders%
 
 /-- Create a TOML table that encodes the declarative configuration of the package. -/
 public def Package.mkTomlConfig (pkg : Package) (t : Table := {}) : Table :=
-  let cfg : PackageConfig pkg.name :=
+  let cfg : PackageConfig pkg.name pkg.origName :=
     {pkg.config with testDriver := pkg.testDriver, lintDriver := pkg.lintDriver}
   cfg.toToml t
   |>.smartInsert `defaultTargets pkg.defaultTargets

src/lake/Lake/Config/Meta.lean

@@ -57,7 +57,7 @@ set_option internal.parseQuotWithCurrentStage false
 
 private meta def mkConfigAuxDecls
   (vis? : Option (TSyntax ``visibility))
-  (structId : Ident) (structTy : Term) (views : Array FieldView)
+  (structId : Ident) (structArity : Nat) (structTy : Term) (views : Array FieldView)
 : MacroM (Array Command) := do
   let data : FieldMetadata := {}
   -- `..` is used to avoid missing pattern error from an incomplete match.
@@ -113,7 +113,8 @@ private meta def mkConfigAuxDecls
   let fieldsInst ← `( $[$vis?:visibility]? instance $instId:ident : ConfigFields $structTy := ⟨$fieldsId⟩)
   let instId := mkIdentFrom structId <| structId.getId.modifyBase (·.str "instConfigInfo")
   let structNameLit : Term := ⟨mkNode ``Term.doubleQuotedName #[mkAtom "`", mkAtom "`", structId]⟩
-  let infoInst ← `( $[$vis?:visibility]? instance $instId:ident : ConfigInfo $structNameLit := {fields := $fieldsId})
+  let info ← `({fields := $fieldsId, arity := $(quote structArity)})
+  let infoInst ← `( $[$vis?:visibility]? instance $instId:ident : ConfigInfo $structNameLit := $info)
   let instId := mkIdentFrom structId <| structId.getId.modifyBase (·.str "instEmptyCollection")
   let emptyInst ← `( $[$vis?:visibility]? instance $instId:ident : EmptyCollection $structTy := ⟨{}⟩)
   return data.cmds.push fieldsDef |>.push fieldsInst |>.push infoInst |>.push emptyInst
@@ -166,6 +167,6 @@ public meta def expandConfigDecl : Macro := fun stx => do
     extends $ps,* $(xty?.join)? where $(ctor?.join)? $fields* $drv:optDeriving
   )
   let vis? := mods.raw[2].getOptional?.map (⟨·⟩)
-  let auxDecls ← mkConfigAuxDecls vis? structId structTy views
+  let auxDecls ← mkConfigAuxDecls vis? structId bs.size structTy views
   let cmds := #[struct] ++ auxDecls
   return mkNullNode cmds

src/lake/Lake/Config/MetaClasses.lean

@@ -42,6 +42,7 @@ public class ConfigInfo (name : Name) where
   fields : Array ConfigFieldInfo
   fieldMap : NameMap ConfigFieldInfo :=
     fields.foldl (init := ∅) fun m i => m.insert i.name i
+  arity : Nat
 
 public instance [parent : ConfigParent σ ρ] [field : ConfigField ρ name α] : ConfigField σ name α where
   mkDefault s := field.mkDefault (parent.get s)

src/lake/Lake/Config/Package.lean

@@ -26,12 +26,14 @@ public nonempty_type OpaquePostUpdateHook (pkg : Name)
 public structure Package where
   /-- The name of the package. -/
   name : Name
+  /-- The name specified by the package. -/
+  origName : Name
   /-- The absolute path to the package's directory. -/
   dir : FilePath
   /-- The path to the package's directory relative to the workspace. -/
   relDir : FilePath
   /-- The package's user-defined configuration. -/
-  config : PackageConfig name
+  config : PackageConfig name origName
   /-- The absolute path to the package's configuration file. -/
   configFile : FilePath
   /-- The path to the package's configuration file (relative to `dir`). -/

src/lake/Lake/Config/PackageConfig.lean

@@ -24,7 +24,7 @@ namespace Lake
 
 set_option linter.unusedVariables false in
 /-- A `Package`'s declarative configuration. -/
-public configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanConfig where
+public configuration PackageConfig (p : Name) (n : Name) extends WorkspaceConfig, LeanConfig where
   /-- **For internal use.** Whether this package is Lean itself. -/
   bootstrap : Bool := false
 
@@ -306,11 +306,12 @@ public configuration PackageConfig (name : Name) extends WorkspaceConfig, LeanCo
   libPrefixOnWindows : Bool := false
 deriving Inhabited
 
-/-- The package's name. -/
-public abbrev PackageConfig.name (_ : PackageConfig n) := n
+/-- The package's name as specified by the author. -/
+public abbrev PackageConfig.origName (_ : PackageConfig p n) := n
 
 /-- A package declaration from a configuration written in Lean. -/
 public structure PackageDecl where
   name : Name
-  config : PackageConfig name
+  origName : Name
+  config : PackageConfig name origName
   deriving TypeName

src/lake/Lake/DSL/Config.lean

@@ -9,22 +9,28 @@ prelude
 public import Lean.Elab.Term
 import Lake.DSL.Extensions
 import Lake.DSL.Syntax
+import Lake.Util.Name
 
 namespace Lake.DSL
 open Lean Elab Term
 
+@[builtin_term_elab nameConst]
+def elabNameConst : TermElab := fun stx expectedType? => do
+  let env ← getEnv
+  unless env.contains packageDeclName do
+    throwError "`__name__` can only be used after the `package` declaration"
+  let exp :=
+    match nameExt.getState env with
+    | .anonymous => mkIdent <| packageDeclName.str "origName"
+    | name => Name.quoteFrom stx name
+  withMacroExpansion stx exp <| elabTerm exp expectedType?
+
 /--
 A dummy default constant for `__dir__` to make it type check
 outside Lakefile elaboration (e.g., when editing).
 -/
 public opaque dummyDir : System.FilePath
 
-/--
-A dummy default constant for `get_config` to make it type check
-outside Lakefile elaboration (e.g., when editing).
--/
-public opaque dummyGetConfig? : Name → Option String
-
 @[builtin_term_elab dirConst]
 def elabDirConst : TermElab := fun stx expectedType? => do
   let exp :=
@@ -36,6 +42,12 @@ def elabDirConst : TermElab := fun stx expectedType? => do
       Syntax.mkApp (mkCIdentFrom stx ``id) #[mkCIdentFrom stx ``dummyDir]
   withMacroExpansion stx exp <| elabTerm exp expectedType?
 
+/--
+A dummy default constant for `get_config` to make it type check
+outside Lakefile elaboration (e.g., when editing).
+-/
+public opaque dummyGetConfig? : Name → Option String
+
 @[builtin_term_elab getConfig]
 def elabGetConfig : TermElab := fun stx expectedType? => do
   tryPostponeIfNoneOrMVar expectedType?

src/lake/Lake/DSL/Extensions.lean

@@ -12,6 +12,9 @@ open Lean
 
 namespace Lake
 
+public builtin_initialize nameExt : EnvExtension Name ←
+  registerEnvExtension (pure .anonymous)
+
 public builtin_initialize dirExt : EnvExtension (Option System.FilePath) ←
   registerEnvExtension (pure none)
 

src/lake/Lake/DSL/Package.lean

@@ -9,6 +9,7 @@ prelude
 public import Lake.DSL.Syntax
 import Lake.Config.Package
 import Lake.DSL.Attributes
+import Lake.DSL.Extensions
 import Lake.DSL.DeclUtil
 
 open Lean Parser Elab Command
@@ -26,15 +27,24 @@ def elabPackageCommand : CommandElab := fun stx => do
   withRef kw do
   let configId : Ident ← `(pkgConfig)
   let id ← mkConfigDeclIdent nameStx?
-  let name := Name.quoteFrom id id.getId
-  let ty := Syntax.mkCApp ``PackageConfig #[name]
+  let origName := Name.quoteFrom id id.getId
+  let name :=
+    match nameExt.getState (← getEnv) with
+    | .anonymous => origName
+    | name => Name.quoteFrom id name
+  let ty := Syntax.mkCApp ``PackageConfig #[name, origName]
   elabConfig ``PackageConfig configId ty cfg
   let attr ← `(Term.attrInstance| «package»)
   let attrs := #[attr] ++ expandAttrs attrs?
   let id := mkIdentFrom id packageDeclName
-  let decl ← `({name := $name, config := $configId})
+  let decl ← `({name := $name, origName := $origName, config := $configId})
   let cmd ← `($[$doc?]? @[$attrs,*] abbrev $id : PackageDecl := $decl)
   withMacroExpansion stx cmd <| elabCommand cmd
+  let nameId := mkIdentFrom id <| packageDeclName.str "name"
+  elabCommand <| ← `(
+    @[deprecated "Use `__name__` instead." (since := "2025-09-18")]
+    abbrev $nameId := __name__
+  )
 
 @[builtin_macro postUpdateDecl]
 def expandPostUpdateDecl : Macro := fun stx => do
@@ -43,9 +53,8 @@ def expandPostUpdateDecl : Macro := fun stx => do
     `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := do $seq $[$wds?:whereDecls]?)
   | `($[$doc?]? $[$attrs?]? post_update%$kw $[$pkg?]? := $defn $[$wds?:whereDecls]?) => withRef kw do
     let pkg ← expandOptSimpleBinder pkg?
-    let pkgName := mkIdentFrom pkg `_package.name
     let attr ← `(Term.attrInstance| «post_update»)
     let attrs := #[attr] ++ expandAttrs attrs?
     `($[$doc?]? @[$attrs,*] def postUpdateHook : PostUpdateHookDecl :=
-      {pkg := $pkgName, fn := fun $pkg => $defn} $[$wds?:whereDecls]?)
+      {pkg := __name__, fn := fun $pkg => $defn} $[$wds?:whereDecls]?)
   | stx => Macro.throwErrorAt stx "ill-formed post_update declaration"

src/lake/Lake/DSL/Syntax.lean

@@ -18,6 +18,12 @@ allows the reference manual to document the DSL syntax.
 
 namespace Lake.DSL
 
+/--
+A macro that expands to the assigned name of package
+during the Lakefile's elaboration.
+-/
+scoped syntax (name := nameConst) "__name__" : term
+
 /--
 A macro that expands to the path of package's directory
 during the Lakefile's elaboration.

src/lake/Lake/DSL/Targets.lean

@@ -130,11 +130,10 @@ def expandTargetCommand : Macro := fun stx => do
   let attr ← `(Term.attrInstance| «target»)
   let attrs := #[attr] ++ expandAttrs attrs?
   let name := Name.quoteFrom id id.getId
-  let pkgName := mkIdentFrom id (packageDeclName.str "name")
   let pkg ← expandOptSimpleBinder pkg?
-  `(family_def $id : CustomOut ($pkgName, $name) := $ty
+  `(family_def $id : CustomOut (__name__, $name) := $ty
     $[$doc?]? abbrev $id :=
-      Lake.DSL.mkTargetDecl $ty $pkgName $name (fun $pkg => $defn)
+      Lake.DSL.mkTargetDecl $ty __name__ $name (fun $pkg => $defn)
     $[$wds?:whereDecls]?
     @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl)
 
@@ -165,12 +164,11 @@ def mkConfigDeclDef
   let targetAttr ← `(Term.attrInstance| «target»)
   let kindAttr ← `(Term.attrInstance| $attrId:ident)
   let attrs := #[targetAttr, kindAttr] ++ expandAttrs attrs?
-  let pkg ← mkIdentFromRef (packageDeclName.str "name")
   let declTy ← mkIdentFromRef delTyName.typeName
   let kind := Name.quoteFrom (← getRef) kind
-  `(family_def $id : CustomOut ($pkg, $name) := ConfigTarget $kind
+  `(family_def $id : CustomOut (__name__, $name) := ConfigTarget $kind
     $[$doc?]? abbrev $id : $declTy :=
-      Lake.DSL.mkConfigDecl $pkg $name $kind $configId
+      Lake.DSL.mkConfigDecl __name__ $name $kind $configId
     @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl
   )
 
@@ -228,12 +226,11 @@ def expandExternLibCommand : Macro := fun stx => do
   let attr2 ← `(Term.attrInstance| «extern_lib»)
   let attrs := #[attr1, attr2] ++ expandAttrs attrs?
   let id := expandIdentOrStrAsIdent nameStx
-  let pkgName := mkIdentFrom kw (packageDeclName.str "name")
   let targetId := mkIdentFrom id <| id.getId.modifyBase (· ++ `static)
   let name := Name.quoteFrom id id.getId
   let kind := Name.quoteFrom kw ExternLib.configKind
   `(target $targetId:ident $[$pkg?]? : FilePath := $defn $[$wds?:whereDecls]?
-    family_def $id : CustomOut ($pkgName, $name) := ConfigTarget $kind
+    family_def $id : CustomOut (__name__, $name) := ConfigTarget $kind
     $[$doc?:docComment]? def $id : ExternLibDecl :=
-      Lake.DSL.mkExternLibDecl $pkgName $name
+      Lake.DSL.mkExternLibDecl __name__ $name
     @[$attrs,*] def configDecl : ConfigDecl := $(id).toConfigDecl)

src/lake/Lake/Load/Config.lean

@@ -26,6 +26,8 @@ public structure LoadConfig where
   lakeArgs? : Option (Array String) := none
   /-- The absolute path to the root directory of the Lake workspace. -/
   wsDir : FilePath
+  /-- The assigned name of the package. If `Name.anonymous`, the package's own name will be used. -/
+  pkgName : Name := .anonymous
   /-- The loaded package's directory (relative to the workspace directory). -/
   relPkgDir : FilePath := "."
   /-- The absolute path to the loaded package's directory. -/

src/lake/Lake/Load/Lean.lean

@@ -28,9 +28,9 @@ The resulting package does not yet include any dependencies.
 -/
 public def loadLeanConfig (cfg : LoadConfig) : LogIO (Package × Environment) := do
   let configEnv ← importConfigFile cfg
-  let {name, config} ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
+  let ⟨name, origName, config⟩ ← IO.ofExcept <| PackageDecl.loadFromEnv configEnv cfg.leanOpts
   let pkg : Package := {
-    name, config
+    name, origName, config
     dir := cfg.pkgDir
     relDir := cfg.relPkgDir
     configFile := cfg.configFile

src/lake/Lake/Load/Lean/Elab.lean

@@ -15,7 +15,7 @@ import Lake.DSL.Extensions
 import Lake.DSL.Attributes
 import Lake.Load.Config
 import Lake.Build.Trace
-import Lake.Util.Log
+import Lake.Util.JsonObject
 
 /-! # Lean Configuration Elaborator
 
@@ -60,7 +60,7 @@ public def configModuleName : Name := `lakefile
 
 /-- Elaborate `configFile` with the given package directory and options. -/
 def elabConfigFile
-  (pkgDir : FilePath) (lakeOpts : NameMap String)
+  (pkgName : Name) (pkgDir : FilePath) (lakeOpts : NameMap String)
   (leanOpts := Options.empty) (configFile := pkgDir / defaultLeanConfigFile)
 : LogIO Environment := do
 
@@ -72,6 +72,7 @@ def elabConfigFile
   let env := env.setMainModule configModuleName
 
   -- Configure extensions
+  let env := nameExt.setState env pkgName
   let env := dirExt.setState env pkgDir
   let env := optsExt.setState env lakeOpts
 
@@ -163,6 +164,7 @@ where
     |>.insert ``IR.declMapExt
 
 structure ConfigTrace where
+  name : Name
   platform : String
   leanHash : String
   configHash : Hash
@@ -177,9 +179,12 @@ toolchain). Otherwise, elaborate the configuration and save it to the `.olean`.
 public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do
   let some configName := FilePath.mk <$> cfg.configFile.fileName
     | error "invalid configuration file name"
-  let olean := cfg.lakeDir / configName.withExtension "olean"
-  let traceFile := cfg.lakeDir / configName.withExtension "olean.trace"
-  let lockFile := cfg.lakeDir / configName.withExtension "olean.lock"
+  let pkgName := cfg.pkgName.toString (escape := false)
+  let configDir := cfg.lakeDir / "config" / pkgName
+  IO.FS.createDirAll configDir
+  let olean := configDir / configName.withExtension "olean"
+  let traceFile := configDir / configName.withExtension "olean.trace"
+  let lockFile := configDir / configName.withExtension "olean.lock"
   /-
   Remark:
   To prevent race conditions between the `.olean` and its trace file
@@ -240,9 +245,9 @@ public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do
     | .ok _ | .error (.noFileOrDirectory ..) =>
       h.putStrLn <| Json.pretty <| toJson
         {platform := System.Platform.target, leanHash := cfg.lakeEnv.leanGithash,
-          configHash, options := lakeOpts : ConfigTrace}
+          configHash, name := cfg.pkgName, options := lakeOpts : ConfigTrace}
       h.truncate
-      let env ← elabConfigFile cfg.pkgDir lakeOpts cfg.leanOpts cfg.configFile
+      let env ← elabConfigFile cfg.pkgName cfg.pkgDir lakeOpts cfg.leanOpts cfg.configFile
       Lean.writeModule env olean
       h.unlock
       return env
@@ -256,17 +261,28 @@ public def importConfigFile (cfg : LoadConfig) : LogIO Environment := do
     else
       h.lock (exclusive := false)
       let contents ← h.readToEnd
-      let .ok (trace : ConfigTrace) := Json.parse contents >>= fromJson?
-        | error "compiled configuration is invalid; run with '-R' to reconfigure"
-      let upToDate :=
-        (← olean.pathExists) ∧ trace.platform = System.Platform.target ∧
-        trace.leanHash = cfg.lakeEnv.leanGithash ∧ trace.configHash = configHash
-      if upToDate then
-        let env ← importConfigFileCore olean cfg.leanOpts
-        h.unlock
-        return env
-      else
-        elabConfig (← acquireTrace h) trace.options
+      let errMsg := "compiled configuration is invalid; run with '-R' to reconfigure"
+      match Json.parse contents with
+      | .ok json =>
+        match fromJson? json with
+        | .ok (trace : ConfigTrace) =>
+          let upToDate :=
+            (← olean.pathExists) ∧ trace.name = cfg.pkgName ∧ trace.configHash = configHash ∧
+            trace.platform = System.Platform.target ∧ trace.leanHash = cfg.lakeEnv.leanGithash
+          if upToDate then
+            let env ← importConfigFileCore olean cfg.leanOpts
+            h.unlock
+            return env
+          else
+            elabConfig (← acquireTrace h) trace.options
+        | .error _ => -- trace has unexpected format, try to just read the one necessary field
+          match JsonObject.fromJson? json >>= (·.get "options") with
+          | .ok (opts : NameMap String) =>
+            elabConfig (← acquireTrace h) opts
+          | .error _ =>
+            error errMsg
+      | .error _ =>
+        error errMsg
   if (← traceFile.pathExists) then
     validateTrace <| ← IO.FS.Handle.mk traceFile .read
   else

src/lake/Lake/Load/Resolve.lean

@@ -25,20 +25,6 @@ This module contains definitions for resolving the dependencies of a package.
 
 namespace Lake
 
-def stdMismatchError (newName : String) (rev : String) :=
-s!"the 'std' package has been renamed to '{newName}' and moved to the
-'leanprover-community' organization; downstream packages which wish to
-update to the new std should replace
-
-  require std from
-    git \"https://github.com/leanprover/std4\"{rev}
-
-in their Lake configuration file with
-
-  require {newName} from
-    git \"https://github.com/leanprover-community/{newName}\"{rev}
-"
-
 /--
 Loads the package configuration of a materialized dependency.
 Adds the facets defined in the package to the `Workspace`.
@@ -55,6 +41,7 @@ def loadDepPackage
   let (pkg, env?) ← loadPackageCore name {
     lakeEnv := ws.lakeEnv
     wsDir := ws.dir
+    pkgName := dep.name
     pkgDir
     relPkgDir := dep.relPkgDir
     relConfigFile := dep.configFile
@@ -218,24 +205,6 @@ private def updateAndMaterializeDep
     store matDep.name matDep.manifestEntry
     return matDep
 
-/-- Verify that a dependency was loaded with the correct name. -/
-private def validateDep
-  (pkg : Package) (dep : Dependency) (matDep : MaterializedDep) (depPkg : Package)
-: LoggerIO PUnit := do
-  if depPkg.name ≠ dep.name then
-    if dep.name = .mkSimple "std" then
-      let rev :=
-        match matDep.manifestEntry.src with
-        | .git (inputRev? := some rev) .. => s!" @ {repr rev}"
-        | _ => ""
-      logError (stdMismatchError depPkg.name.toString rev)
-    if matDep.manifestEntry.src matches .git .. then
-      if let .error e ← IO.FS.removeDirAll depPkg.dir |>.toBaseIO then -- cleanup
-        -- Deleting git repositories via IO.FS.removeDirAll does not work reliably on Windows
-        logError s!"'{dep.name}' was downloaded incorrectly; \
-          you will need to manually delete '{depPkg.dir}': {e}"
-    error s!"{pkg.name}: package '{depPkg.name}' was required as '{dep.name}'"
-
 /--
 Exit code returned if Lake needs a manual restart.
 Used, for instance, if the toolchain is updated and no Elan is detected.
@@ -352,7 +321,7 @@ def Workspace.updateAndMaterializeCore
     ws.updateToolchain matDeps
     let start := ws.packages.size
     let ws ← (deps.zip matDeps).foldlM (init := ws) fun ws (dep, matDep) => do
-      let (depPkg, ws) ← loadUpdatedDep ws.root dep matDep ws
+      let (depPkg, ws) ← loadUpdatedDep dep matDep ws
       let ws := ws.addPackage depPkg
       return ws
     ws.packages.foldlM (init := ws) (start := start) fun ws pkg =>
@@ -362,10 +331,9 @@ def Workspace.updateAndMaterializeCore
 where
   @[inline] updateAndLoadDep pkg dep := do
     let matDep ← updateAndMaterializeDep (← getWorkspace) pkg dep
-    loadUpdatedDep pkg dep matDep
-  @[inline] loadUpdatedDep pkg dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
+    loadUpdatedDep dep matDep
+  @[inline] loadUpdatedDep dep matDep : StateT Workspace (UpdateT LoggerIO) Package  := do
     let depPkg ← loadDepPackage matDep dep.opts leanOpts true
-    validateDep pkg dep matDep depPkg
     addDependencyEntries depPkg
     return depPkg
 

src/lake/Lake/Load/Toml.lean

@@ -245,7 +245,7 @@ public instance : DecodeToml PathPatDescr := ⟨PathPatDescr.decodeToml⟩
 public def decodeVersionTags (v : Value) : EDecodeM StrPat :=
   inline <| Pattern.decodeToml (presets := versionTagPresets) v
 
-public instance : DecodeField (PackageConfig n) `versionTags where
+public instance : DecodeField (PackageConfig p n) `versionTags where
   decodeField := decodeFieldCore `versionTags decodeVersionTags
 
 -- for `platformIndependent`, `releaseRepo`, `buildArchive`, etc.
@@ -360,11 +360,13 @@ section
 set_option internal.parseQuotWithCurrentStage false
 private meta def genDecodeToml
   (cmds : Array Command)
-  (tyName : Name) [info : ConfigInfo tyName]  (takesName : Bool)
+  (tyName : Name) [info : ConfigInfo tyName]
   (exclude : Array Name := {})
 : MacroM (Array Command) := do
   let init ← `(TomlFieldInfos.empty)
-  let ty := if takesName then Syntax.mkCApp tyName #[mkIdent `n] else mkCIdent tyName
+  let tyArgs := info.arity.fold (init := Array.emptyWithCapacity info.arity) fun i _ as =>
+    as.push (mkIdent <| .mkSimple s!"x_{i+1}")
+  let ty := Syntax.mkCApp tyName tyArgs
   let infos ← info.fields.foldlM (init := init) fun infos {name, parent, ..} =>
     if parent || exclude.contains name then
       return infos
@@ -382,16 +384,16 @@ end
 local macro "gen_toml_decoders%" : command => do
   let cmds := #[]
   -- Targets
-  let cmds ← genDecodeToml cmds ``LeanConfig false
-  let cmds ← genDecodeToml cmds ``LeanLibConfig true
+  let cmds ← genDecodeToml cmds ``LeanConfig
+  let cmds ← genDecodeToml cmds ``LeanLibConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genDecodeToml cmds ``LeanExeConfig true
+  let cmds ← genDecodeToml cmds ``LeanExeConfig
     (exclude := #[`nativeFacets])
-  let cmds ← genDecodeToml cmds ``InputFileConfig true
-  let cmds ← genDecodeToml cmds ``InputDirConfig true
+  let cmds ← genDecodeToml cmds ``InputFileConfig
+  let cmds ← genDecodeToml cmds ``InputDirConfig
   -- Package
-  let cmds ← genDecodeToml cmds ``WorkspaceConfig false
-  let cmds ← genDecodeToml cmds ``PackageConfig true
+  let cmds ← genDecodeToml cmds ``WorkspaceConfig
+  let cmds ← genDecodeToml cmds ``PackageConfig
   return ⟨mkNullNode cmds⟩
 
 gen_toml_decoders%
@@ -435,14 +437,15 @@ public def loadTomlConfig (cfg: LoadConfig) : LogIO Package := do
   match (← loadToml ictx |>.toBaseIO) with
   | .ok table =>
     let .ok pkg errs := EStateM.run (s := #[]) do
-      let name ← stringToLegalOrSimpleName <$> table.tryDecode `name
-      let config ← @PackageConfig.decodeToml name table
+      let origName ← stringToLegalOrSimpleName <$> table.tryDecode `name
+      let name := if cfg.pkgName.isAnonymous then origName else cfg.pkgName
+      let config ← @PackageConfig.decodeToml name origName table
       let (targetDecls, targetDeclMap) ← decodeTargetDecls name table
       let defaultTargets ← table.tryDecodeD `defaultTargets #[]
       let defaultTargets := defaultTargets.map stringToLegalOrSimpleName
       let depConfigs ← table.tryDecodeD `require #[]
       return {
-        name := name
+        name, origName
         dir := cfg.pkgDir
         relDir := cfg.relPkgDir
         configFile := cfg.configFile

src/lake/tests/depRenaming/clean.sh

@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json dep/.lake produced.out

src/lake/tests/depRenaming/dep/lakefile.lean

@@ -0,0 +1,7 @@
+import Lake
+open System Lake DSL
+
+package dep
+
+target name : String := do
+  return .pure <| (__name__).toString

src/lake/tests/depRenaming/lakefile.toml

@@ -0,0 +1,9 @@
+name = "test"
+
+[[require]]
+name = "a"
+path = "dep"
+
+[[require]]
+name = "b"
+path = "dep"

src/lake/tests/depRenaming/test.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Test loading the same dependency with different names
+test_run update
+test_eq 'a' query @a/name
+test_eq 'b' query @b/name
+
+# cleanup
+rm -f produced.out

src/shell/CMakeLists.txt

@@ -197,7 +197,7 @@ ENDFOREACH(T)
 # toolchain: requires elan to download toolchain
 # online: downloads remote repositories
 file(GLOB_RECURSE LEANLAKETESTS
-  #"${LEAN_SOURCE_DIR}/lake/tests/test.sh"
+  "${LEAN_SOURCE_DIR}/lake/tests/test.sh"
   "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
 FOREACH(T ${LEANLAKETESTS})
   if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")