diff --git a/src/lake/Lake/CLI/Translate/Lean.lean b/src/lake/Lake/CLI/Translate/Lean.lean
index 7dcf0def12..e305fabe9c 100644
--- a/src/lake/Lake/CLI/Translate/Lean.lean
+++ b/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|
diff --git a/src/lake/Lake/CLI/Translate/Toml.lean b/src/lake/Lake/CLI/Translate/Toml.lean
index 7fff975ced..ad5e3dad2d 100644
--- a/src/lake/Lake/CLI/Translate/Toml.lean
+++ b/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
diff --git a/src/lake/Lake/Config/Meta.lean b/src/lake/Lake/Config/Meta.lean
index 5997d3a94f..71180ee838 100644
--- a/src/lake/Lake/Config/Meta.lean
+++ b/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
diff --git a/src/lake/Lake/Config/MetaClasses.lean b/src/lake/Lake/Config/MetaClasses.lean
index de3a4c1263..bd6a839246 100644
--- a/src/lake/Lake/Config/MetaClasses.lean
+++ b/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)
diff --git a/src/lake/Lake/Config/Package.lean b/src/lake/Lake/Config/Package.lean
index 70a1bfee7a..6f4fdbc5ef 100644
--- a/src/lake/Lake/Config/Package.lean
+++ b/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`). -/
diff --git a/src/lake/Lake/Config/PackageConfig.lean b/src/lake/Lake/Config/PackageConfig.lean
index 8a40ab526e..3aa5dc5a50 100644
--- a/src/lake/Lake/Config/PackageConfig.lean
+++ b/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
diff --git a/src/lake/Lake/DSL/Config.lean b/src/lake/Lake/DSL/Config.lean
index 0ef703c6c3..b688c834a9 100644
--- a/src/lake/Lake/DSL/Config.lean
+++ b/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?
diff --git a/src/lake/Lake/DSL/Extensions.lean b/src/lake/Lake/DSL/Extensions.lean
index 5168f9336c..fc8a1c0292 100644
--- a/src/lake/Lake/DSL/Extensions.lean
+++ b/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)
 
diff --git a/src/lake/Lake/DSL/Package.lean b/src/lake/Lake/DSL/Package.lean
index 6040ef32ed..27c58c73a6 100644
--- a/src/lake/Lake/DSL/Package.lean
+++ b/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"
diff --git a/src/lake/Lake/DSL/Syntax.lean b/src/lake/Lake/DSL/Syntax.lean
index 3e95f47a4b..c5411749f1 100644
--- a/src/lake/Lake/DSL/Syntax.lean
+++ b/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.
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
index f0a13b9bed..c41facee67 100644
--- a/src/lake/Lake/DSL/Targets.lean
+++ b/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)
diff --git a/src/lake/Lake/Load/Config.lean b/src/lake/Lake/Load/Config.lean
index aeb911d290..48d3032f18 100644
--- a/src/lake/Lake/Load/Config.lean
+++ b/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. -/
diff --git a/src/lake/Lake/Load/Lean.lean b/src/lake/Lake/Load/Lean.lean
index 1a1bd17d05..06d348377c 100644
--- a/src/lake/Lake/Load/Lean.lean
+++ b/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
diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean
index 46a54f29b1..4896afc739 100644
--- a/src/lake/Lake/Load/Lean/Elab.lean
+++ b/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
diff --git a/src/lake/Lake/Load/Resolve.lean b/src/lake/Lake/Load/Resolve.lean
index 3e537ed256..0fa010a14b 100644
--- a/src/lake/Lake/Load/Resolve.lean
+++ b/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
 
diff --git a/src/lake/Lake/Load/Toml.lean b/src/lake/Lake/Load/Toml.lean
index 6d892461a0..da83634206 100644
--- a/src/lake/Lake/Load/Toml.lean
+++ b/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
diff --git a/src/lake/tests/depRenaming/clean.sh b/src/lake/tests/depRenaming/clean.sh
new file mode 100755
index 0000000000..61c77ffd42
--- /dev/null
+++ b/src/lake/tests/depRenaming/clean.sh
@@ -0,0 +1 @@
+rm -rf .lake lake-manifest.json dep/.lake produced.out
diff --git a/src/lake/tests/depRenaming/dep/lakefile.lean b/src/lake/tests/depRenaming/dep/lakefile.lean
new file mode 100644
index 0000000000..c53f7b02b3
--- /dev/null
+++ b/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
diff --git a/src/lake/tests/depRenaming/lakefile.toml b/src/lake/tests/depRenaming/lakefile.toml
new file mode 100644
index 0000000000..0f58677dad
--- /dev/null
+++ b/src/lake/tests/depRenaming/lakefile.toml
@@ -0,0 +1,9 @@
+name = "test"
+
+[[require]]
+name = "a"
+path = "dep"
+
+[[require]]
+name = "b"
+path = "dep"
diff --git a/src/lake/tests/depRenaming/test.sh b/src/lake/tests/depRenaming/test.sh
new file mode 100755
index 0000000000..132849f2e1
--- /dev/null
+++ b/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
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 63b2444734..bec8e2bc67 100644
--- a/src/shell/CMakeLists.txt
+++ b/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).*")