From 343328b7dfe7bc2bb31a66e2894508e3f8a0a3d2 Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 25 Sep 2025 18:10:39 -0400 Subject: [PATCH] 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 | 24 ++++----- src/lake/Lake/CLI/Translate/Toml.lean | 25 +++++----- src/lake/Lake/Config/Meta.lean | 7 +-- src/lake/Lake/Config/MetaClasses.lean | 1 + src/lake/Lake/Config/Package.lean | 4 +- src/lake/Lake/Config/PackageConfig.lean | 9 ++-- src/lake/Lake/DSL/Config.lean | 24 ++++++--- src/lake/Lake/DSL/Extensions.lean | 3 ++ src/lake/Lake/DSL/Package.lean | 19 +++++-- src/lake/Lake/DSL/Syntax.lean | 6 +++ src/lake/Lake/DSL/Targets.lean | 15 +++--- src/lake/Lake/Load/Config.lean | 2 + src/lake/Lake/Load/Lean.lean | 4 +- src/lake/Lake/Load/Lean/Elab.lean | 52 +++++++++++++------- src/lake/Lake/Load/Resolve.lean | 40 ++------------- src/lake/Lake/Load/Toml.lean | 29 ++++++----- src/lake/tests/depRenaming/clean.sh | 1 + src/lake/tests/depRenaming/dep/lakefile.lean | 7 +++ src/lake/tests/depRenaming/lakefile.toml | 9 ++++ src/lake/tests/depRenaming/test.sh | 12 +++++ src/shell/CMakeLists.txt | 2 +- 21 files changed, 175 insertions(+), 120 deletions(-) create mode 100755 src/lake/tests/depRenaming/clean.sh create mode 100644 src/lake/tests/depRenaming/dep/lakefile.lean create mode 100644 src/lake/tests/depRenaming/lakefile.toml create mode 100755 src/lake/tests/depRenaming/test.sh 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).*")