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.

Author: tydeu

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.