fix: symbol clashes between packages (#11082)

This PR prevents symbol clashes between (non-`@[export]`) definitions
from different Lean packages.

Previously, if two modules define a function with the same name and were
transitively imported (even privately) by some downstream module,
linking would fail due to a symbol clash. Similarly, if a user defined a
symbol with the same name as one in the `Lean` library, Lean would use
the core symbol even if one did not import `Lean`.

This is solved by changing Lean's name mangling algorithm to include an
optional package identifier. This identifier is provided by Lake via
`--setup` when building a module. This information is weaved through the
elaborator, interpreter, and compiler via a persistent environment
extension that associates modules with their package identifier.

With a package identifier, standard symbols have the form
`lp_<pkg-id>_<mangled-def>`. Without one, the old scheme is used (i.e.,
`l_<mangled-def>`). Module initializers are also prefixed with package
identifier (if any). For example, the initializer for a module `Foo` in
a package `test` is now `initialize_test_Foo` (instead of
`initialize_Foo`). Lake's default for native library names has also been
adjusted accordingly, so that libraries can still, by default, be used
as plugins. Thus, the default library name of the `lean_lib Foo` in
`package test` will now be `libtest_Foo`.

When using Lake to build the Lean core (i.e., `bootstrap = true`), no
package identifier will be used. Thus, definitions in user packages can
never have symbol clashes with core.

Closes #222.

doc/dev/ffi.md

@@ -129,8 +129,7 @@ For all other modules imported by `lean`, the initializer is run without `builti
 Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtin_init]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
 `lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
 
-The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
-Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
+The initializer for module `A.B` in a package `foo` is called `initialize_foo_A_B`. For modules in the Lean core (e.g., `Init.Prelude`), the initializer is called `initialize_Init_Prelude`. Module initializers will automatically initialize any imported modules. They are also idempotent (when run with the same `builtin` flag), but not thread-safe.
 
 **Important for process-related functionality**: If your application needs to use process-related functions from libuv, such as `Std.Internal.IO.Process.getProcessTitle` and `Std.Internal.IO.Process.setProcessTitle`, you must call `lean_setup_args(argc, argv)` (which returns a potentially modified `argv` that must be used in place of the original) **before** calling `lean_initialize()` or `lean_initialize_runtime_module()`. This sets up process handling capabilities correctly, which is essential for certain system-level operations that Lean's runtime may depend on.
 

src/Lean/Compiler/IR/EmitC.lean

@@ -11,6 +11,7 @@ public import Lean.Compiler.IR.EmitUtil
 public import Lean.Compiler.IR.NormIds
 public import Lean.Compiler.IR.SimpCase
 public import Lean.Compiler.IR.Boxing
+public import Lean.Compiler.ModPkgExt
 
 public section
 
@@ -28,8 +29,14 @@ structure Context where
 
 abbrev M := ReaderT Context (EStateM String String)
 
-def getEnv : M Environment := Context.env <$> read
-def getModName : M Name := Context.modName <$> read
+@[inline] def getEnv : M Environment := Context.env <$> read
+
+@[inline] def getModName : M Name := Context.modName <$> read
+
+@[inline] def getModInitFn : M String := do
+  let pkg? := (← getEnv).getModulePackage?
+  return mkModuleInitializationFunctionName (← getModName) pkg?
+
 def getDecl (n : Name) : M Decl := do
   let env ← getEnv
   match findEnvDecl env n with
@@ -76,9 +83,9 @@ def toCName (n : Name) : M String := do
   let env ← getEnv;
   -- TODO: we should support simple export names only
   match getExportNameFor? env n with
-  | some (.str .anonymous s) => pure s
+  | some (.str .anonymous s) => return s
   | some _                   => throwInvalidExportName n
-  | none                     => if n == `main then pure leanMainFn else pure n.mangle
+  | none                     => return if n == `main then leanMainFn else getSymbolStem env n
 
 def emitCName (n : Name) : M Unit :=
   toCName n >>= emit
@@ -89,7 +96,7 @@ def toCInitName (n : Name) : M String := do
   match getExportNameFor? env n with
   | some (.str .anonymous s) => return "_init_" ++ s
   | some _                   => throwInvalidExportName n
-  | none                     => pure ("_init_" ++ n.mangle)
+  | none                     => return "_init_" ++ getSymbolStem env n
 
 def emitCInitName (n : Name) : M Unit :=
   toCInitName n >>= emit
@@ -168,11 +175,10 @@ def emitMainFn : M Unit := do
       emitLn "lean_initialize();"
     else
       emitLn "lean_initialize_runtime_module();"
-    let modName ← getModName
     /- We disable panic messages because they do not mesh well with extracted closed terms.
        See issue #534. We can remove this workaround after we implement issue #467. -/
     emitLn "lean_set_panic_messages(false);"
-    emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */);")
+    emitLn s!"res = {← getModInitFn}(1 /* builtin */);"
     emitLn "lean_set_panic_messages(true);"
     emitLns ["lean_io_mark_end_initialization();",
              "if (lean_io_result_is_ok(res)) {",
@@ -747,17 +753,22 @@ def emitDeclInit (d : Decl) : M Unit := do
 
 def emitInitFn : M Unit := do
   let env ← getEnv
-  let modName ← getModName
-  env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin);")
+  let impInitFns ← env.imports.mapM fun imp => do
+    let some idx := env.getModuleIdx? imp.module
+      | throw "(internal) import without module index" -- should be unreachable
+    let pkg? := env.getModulePackageByIdx? idx
+    let fn := mkModuleInitializationFunctionName imp.module pkg?
+    emitLn s!"lean_object* {fn}(uint8_t builtin);"
+    return fn
   emitLns [
     "static bool _G_initialized = false;",
-    "LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin) {",
+    s!"LEAN_EXPORT lean_object* {← getModInitFn}(uint8_t builtin) \{",
     "lean_object * res;",
     "if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
     "_G_initialized = true;"
   ]
-  env.imports.forM fun imp => emitLns [
-    "res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin);",
+  impInitFns.forM fun fn => emitLns [
+    s!"res = {fn}(builtin);",
     "if (lean_io_result_is_error(res)) return res;",
     "lean_dec_ref(res);"]
   let decls := getDecls env
@@ -774,9 +785,8 @@ def main : M Unit := do
 
 end EmitC
 
-@[export lean_ir_emit_c]
 def emitC (env : Environment) (modName : Name) : Except String String :=
-  match (EmitC.main { env := env, modName := modName }).run "" with
+  match EmitC.main { env, modName } |>.run "" with
   | EStateM.Result.ok    _   s => Except.ok s
   | EStateM.Result.error err _ => Except.error err
 

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -13,6 +13,7 @@ public import Lean.Compiler.IR.SimpCase
 public import Lean.Compiler.IR.Boxing
 public import Lean.Compiler.IR.ResetReuse
 public import Lean.Compiler.IR.LLVMBindings
+import Lean.Compiler.ModPkgExt
 
 public section
 
@@ -345,16 +346,18 @@ def throwInvalidExportName {α : Type} (n : Name) : M llvmctx α := do
   throw s!"invalid export name {n.toString}"
 
 def toCName (n : Name) : M llvmctx String := do
-  match getExportNameFor? (← getEnv) n with
-  | some (.str .anonymous s) => pure s
+  let env ← getEnv
+  match getExportNameFor? env n with
+  | some (.str .anonymous s) => return s
   | some _                   => throwInvalidExportName n
-  | none                     => if n == `main then pure leanMainFn else pure n.mangle
+  | none                     => return if n == `main then leanMainFn else getSymbolStem env n
 
 def toCInitName (n : Name) : M llvmctx String := do
-  match getExportNameFor? (← getEnv) n with
+  let env ← getEnv
+  match getExportNameFor? env n with
   | some (.str .anonymous s) => return "_init_" ++ s
   | some _                   => throwInvalidExportName n
-  | none                     => pure ("_init_" ++ n.mangle)
+  | none                     => return "_init_" ++ getSymbolStem env n
 
 /--
 ## LLVM Control flow Utilities
@@ -1333,8 +1336,9 @@ def emitDeclInit (builder : LLVM.Builder llvmctx)
          callLeanMarkPersistentFn builder dval
 
 def callModInitFn (builder : LLVM.Builder llvmctx)
-    (modName : Name) (input world : LLVM.Value llvmctx) (retName : String): M llvmctx (LLVM.Value llvmctx) := do
-  let fnName := mkModuleInitializationFunctionName modName
+    (modName : Name) (pkg? : Option PkgId)
+    (input world : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx) := do
+  let fnName := mkModuleInitializationFunctionName modName pkg?
   let retty ← LLVM.voidPtrType llvmctx
   let argtys := #[ (← LLVM.i8Type llvmctx), (← LLVM.voidPtrType llvmctx)]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
@@ -1344,9 +1348,9 @@ def callModInitFn (builder : LLVM.Builder llvmctx)
 def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M llvmctx Unit := do
   let env ← getEnv
   let modName ← getModName
-
+  let pkg? := env.getModulePackage?
   let initFnTy ← LLVM.functionType (← LLVM.voidPtrType llvmctx) #[ (← LLVM.i8Type llvmctx), (← LLVM.voidPtrType llvmctx)] (isVarArg := false)
-  let initFn ← LLVM.getOrAddFunction mod (mkModuleInitializationFunctionName modName) initFnTy
+  let initFn ← LLVM.getOrAddFunction mod (mkModuleInitializationFunctionName modName pkg?) initFnTy
   LLVM.setDLLStorageClass initFn LLVM.DLLStorageClass.export  -- LEAN_EXPORT
   let entryBB ← LLVM.appendBasicBlockInContext llvmctx initFn "entry"
   LLVM.positionBuilderAtEnd builder entryBB
@@ -1366,7 +1370,10 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
   env.imports.forM fun import_ => do
     let builtin ← LLVM.getParam initFn 0
     let world ← callLeanIOMkWorld builder
-    let res ← callModInitFn builder import_.module builtin world ("res_" ++ import_.module.mangle)
+    let some idx := env.getModuleIdx? import_.module
+      | throw "(internal) import without module index" -- should be unreachable
+    let pkg? := env.getModulePackageByIdx? idx
+    let res ← callModInitFn builder import_.module pkg? builtin world ("res_" ++ import_.module.mangle)
     let err? ← callLeanIOResultIsError builder res ("res_is_error_"  ++ import_.module.mangle)
     buildIfThen_ builder ("IsError" ++ import_.module.mangle) err?
       (fun builder => do
@@ -1512,7 +1519,8 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M
         See issue #534. We can remove this workaround after we implement issue #467. -/
   callLeanSetPanicMessages builder (← LLVM.constFalse llvmctx)
   let world ← callLeanIOMkWorld builder
-  let resv ← callModInitFn builder (← getModName) (← constInt8 1) world ((← getModName).toString ++ "_init_out")
+  let resv ← callModInitFn builder (← getModName) env.getModulePackage?
+    (← constInt8 1) world ((← getModName).toString ++ "_init_out")
   let _ ← LLVM.buildStore builder resv res
 
   callLeanSetPanicMessages builder (← LLVM.constTrue llvmctx)

src/Lean/Compiler/InitAttr.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.AddDecl
 public import Lean.Elab.InfoTree.Main
 import Init.Data.Range.Polymorphic.Stream
+import Lean.Compiler.NameMangling
+import Lean.Compiler.ModPkgExt
 
 public section
 
@@ -27,12 +29,16 @@ private def isIOUnit (type : Expr) : Bool :=
   | some type => isUnitType type
   | _ => false
 
+@[extern "lean_run_mod_init_core"]
+private unsafe opaque runModInitCore (sym : @& String) : IO Bool
+
 /--
-  Run the initializer of the given module (without `builtin_initialize` commands).
-  Return `false` if the initializer is not available as native code.
-  Initializers do not have corresponding Lean definitions, so they cannot be interpreted in this case. -/
-@[extern "lean_run_mod_init"]
-unsafe opaque runModInit (mod : Name) : IO Bool
+Run the initializer of the given module (without `builtin_initialize` commands).
+Return `false` if the initializer is not available as native code.
+Initializers do not have corresponding Lean definitions, so they cannot be interpreted in this case.
+-/
+@[inline] private unsafe def runModInit (mod : Name) (pkg? : Option String) : IO Bool :=
+  runModInitCore (mkModuleInitializationFunctionName mod pkg?)
 
 /-- Run the initializer for `decl` and store its value for global access. Should only be used while importing. -/
 @[extern "lean_run_init"]
@@ -159,7 +165,8 @@ private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit :
       -- any native Lean code reachable by the interpreter (i.e. from shared
       -- libraries with their corresponding module in the Environment) must
       -- first be initialized
-      if (← runModInit mod) then
+      let pkg? := env.getModulePackageByIdx? modIdx
+      if (← runModInit mod pkg?) then
         continue
       -- As `[init]` decls can have global side effects, ensure we run them at most once,
       -- just like the compiled code does.

src/Lean/Compiler/ModPkgExt.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+module
+
+prelude
+public import Lean.Environment
+import Lean.Compiler.NameMangling
+
+set_option doc.verso true
+
+namespace Lean
+
+/-- Persistent environment extension for storing a single serializable value per module. -/
+@[expose] public def ModuleEnvExtension (σ : Type) := PersistentEnvExtension σ σ σ
+
+public def registerModuleEnvExtension
+  [Inhabited σ] (mkInitial : IO σ) (name : Name := by exact decl_name%)
+: IO (ModuleEnvExtension σ) :=
+  registerPersistentEnvExtension {
+    name            := name
+    mkInitial       := mkInitial
+    addImportedFn   := fun _ _ => mkInitial
+    addEntryFn      := fun s _ => s
+    exportEntriesFn := fun s => #[s]
+  }
+
+namespace ModuleEnvExtension
+
+public instance [Inhabited σ] : Inhabited (ModuleEnvExtension σ) :=
+  inferInstanceAs (Inhabited (PersistentEnvExtension ..))
+
+public def getStateByIdx? [Inhabited σ] (ext : ModuleEnvExtension σ) (env : Environment) (idx : ModuleIdx) : Option σ :=
+  (ext.getModuleEntries env idx)[0]?
+
+end ModuleEnvExtension
+
+private initialize modPkgExt : ModuleEnvExtension (Option PkgId) ←
+  registerModuleEnvExtension (pure none)
+
+/-- Returns the package (if any) of an imported module (by its index). -/
+public def Environment.getModulePackageByIdx? (env : Environment) (idx : ModuleIdx) : Option PkgId :=
+  modPkgExt.getStateByIdx? env idx |>.join
+
+/-- Returns the package (if any) of the current module. -/
+@[inline] public def Environment.getModulePackage? (env : Environment) : Option PkgId :=
+  modPkgExt.getState env
+
+/-- Sets the package of the current module. -/
+@[inline] public def Environment.setModulePackage (pkg? : Option PkgId) (env : Environment) : Environment :=
+  modPkgExt.setState env pkg?
+
+/--
+Returns the standard base of the native symbol for the compiled constant {lean}`declName`.
+
+For many constants, this is the full symbol. However, initializers have an additional prefix
+(i.e., {lit}`_init_`) and boxed functions have an additional suffix (i.e., {lit}`___boxed`).
+Furthermore, some constants do not use this stem at all (e.g., {lit}`main` and definitions
+with {lit}`@[export]`).
+-/
+@[export lean_get_symbol_stem]
+public def getSymbolStem (env : Environment) (declName : Name) : String :=
+  let pkg? :=
+    match env.getModuleIdxFor? declName with
+    | some idx => env.getModulePackageByIdx? idx
+    | none => env.getModulePackage?
+  declName.mangle (mkPackageSymbolPrefix pkg?)

src/Lean/Compiler/NameMangling.lean

@@ -6,7 +6,7 @@ Author: Leonardo de Moura, Robin Arnez
 module
 
 prelude
-public import Init.Prelude
+public import Lean.Setup
 import Init.Data.String.Termination
 
 namespace String
@@ -130,13 +130,23 @@ def Name.mangleAux : Name → String
     | p              =>
       mangleAux p ++ "_" ++ n.repr ++ "_"
 
-@[export lean_name_mangle]
 public def Name.mangle (n : Name) (pre : String := "l_") : String :=
   pre ++ Name.mangleAux n
 
-@[export lean_mk_module_initialization_function_name]
-public def mkModuleInitializationFunctionName (moduleName : Name) : String :=
-  "initialize_" ++ moduleName.mangle ""
+/--
+The mangled name of the name used to create the module initialization function.
+
+This also used for the library name of a module plugin.
+-/
+public def mkModuleInitializationStem (moduleName : Name) (pkg? : Option PkgId := none) : String :=
+  let pre := pkg?.elim "" (s!"{·.mangle}_")
+  moduleName.mangle pre
+
+public def mkModuleInitializationFunctionName (moduleName : Name) (pkg? : Option PkgId := none) : String :=
+  "initialize_" ++ mkModuleInitializationStem moduleName pkg?
+
+public def mkPackageSymbolPrefix (pkg? : Option PkgId) : String :=
+  pkg?.elim "l_" (s!"lp_{·.mangle}_")
 
 -- assumes `s` has been generated `Name.mangle n ""`
 def Name.demangleAux (s : String) (p₀ : s.ValidPos) (res : Name)

src/Lean/Elab/Frontend.lean

@@ -157,6 +157,7 @@ def runFrontend
       liftM <| setup.dynlibs.forM Lean.loadDynlib
       return .ok {
         trustLevel
+        package? := setup.package?
         mainModuleName := setup.name
         isModule := strictOr setup.isModule stx.isModule
         imports := setup.imports?.getD stx.imports

src/Lean/Elab/Import.lean

@@ -8,6 +8,7 @@ module
 prelude
 public import Lean.Parser.Module
 meta import Lean.Parser.Module
+import Lean.Compiler.ModPkgExt
 
 public section
 
@@ -45,7 +46,8 @@ def processHeaderCore
     (startPos : String.Pos.Raw) (imports : Array Import) (isModule : Bool)
     (opts : Options) (messages : MessageLog) (inputCtx : Parser.InputContext)
     (trustLevel : UInt32 := 0) (plugins : Array System.FilePath := #[]) (leakEnv := false)
-    (mainModule := Name.anonymous) (arts : NameMap ImportArtifacts := {})
+    (mainModule := Name.anonymous) (package? : Option PkgId := none)
+    (arts : NameMap ImportArtifacts := {})
     : IO (Environment × MessageLog) := do
   let level := if isModule then
     if Elab.inServer.get opts then
@@ -63,7 +65,8 @@ def processHeaderCore
     let env ← mkEmptyEnvironment
     let pos := inputCtx.fileMap.toPosition startPos
     pure (env, messages.add { fileName := inputCtx.fileName, data := toString e, pos := pos })
-  return (env.setMainModule mainModule, messages)
+  let env := env.setMainModule mainModule |>.setModulePackage package?
+  return (env, messages)
 
 /--
 Elaborates the given header syntax into an environment.

src/Lean/Language/Lean.lean

@@ -285,6 +285,8 @@ simple uses, these can be computed eagerly without looking at the imports.
 structure SetupImportsResult where
   /-- Module name of the file being processed. -/
   mainModuleName : Name
+  /-- Package name of the file being processed (if any). -/
+  package? : Option PkgId := none
   /-- Whether the file is participating in the module system. -/
   isModule : Bool
   /-- Direct imports of the file being processed. -/
@@ -493,7 +495,7 @@ where
       -- allows `headerEnv` to be leaked, which would live until the end of the process anyway
       let (headerEnv, msgLog) ← Elab.processHeaderCore (leakEnv := true)
         stx.startPos setup.imports setup.isModule setup.opts .empty ctx.toInputContext
-        setup.trustLevel setup.plugins setup.mainModuleName setup.importArts
+        setup.trustLevel setup.plugins setup.mainModuleName setup.package? setup.importArts
       let stopTime := (← IO.monoNanosNow).toFloat / 1000000000
       let diagnostics := (← Snapshot.Diagnostics.ofMessageLog msgLog)
       if msgLog.hasErrors then

src/Lean/Server/FileWorker.lean

@@ -438,6 +438,7 @@ def setupImports
 
   return .ok {
     mainModuleName := doc.mod
+    package? := setup.package?
     isModule := strictOr setup.isModule header.isModule
     imports := setup.imports?.getD header.imports
     opts

src/Lean/Setup.lean

@@ -9,6 +9,8 @@ prelude
 public import Lean.Data.Json.Parser
 public import Lean.Util.LeanOptions
 
+set_option doc.verso true
+
 public section
 
 /-!
@@ -46,7 +48,7 @@ structure ModuleHeader where
   deriving Repr, Inhabited, ToJson, FromJson
 
 /--
-Module data files used for an `import` statement.
+Module data files used for an {lit}`import` statement.
 This structure is designed for efficient JSON serialization.
 -/
 structure ImportArtifacts where
@@ -107,18 +109,29 @@ def ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath
         fnames := fnames.push pFile
   return fnames
 
+/--
+The type of module package identifiers.
+
+This is a {name}`String` that is used to disambiguate native symbol prefixes between
+different packages (and different versions of the same package).
+-/
+public abbrev PkgId := String
+
 /-- A module's setup information as described by a JSON file. -/
 structure ModuleSetup where
-  /-- Name of the module. -/
+  /-- The name of the module. -/
   name : Name
+  /-- The package to which the module belongs (if any). -/
+  package? : Option PkgId := none
   /--
   Whether the module, by default, participates in the module system.
-  Even if `false`, a module can still choose to participate by using `module` in its header.
+  Even if {lean}`false`, a module can still choose to participate by using
+  {lit}`module` in its header.
   -/
   isModule : Bool := false
   /--
   The module's direct imports.
-  If `none`, uses the imports from the module header.
+  If {lean}`none`, uses the imports from the module header.
   -/
   imports? : Option (Array Import) := none
   /-- Pre-resolved artifacts of transitively imported modules. -/
@@ -131,7 +144,7 @@ structure ModuleSetup where
   options : LeanOptions := {}
   deriving Repr, Inhabited, ToJson, FromJson
 
-/-- Load a `ModuleSetup` from a JSON file. -/
+/-- Load a {lean}`ModuleSetup` from a JSON file. -/
 def ModuleSetup.load (path : System.FilePath) : IO ModuleSetup := do
   let contents ← IO.FS.readFile path
   match Json.parse contents >>= fromJson? with

src/lake/Lake/Build/Module.lean

@@ -481,6 +481,7 @@ private def Module.recFetchSetup (mod : Module) : FetchM (Job ModuleSetup) := en
     return {
       name := mod.name
       isModule := header.isModule
+      package? := mod.pkg.id?
       imports? := none
       importArts := info.directArts
       dynlibs := dynlibs.map (·.path)
@@ -978,6 +979,7 @@ private def setupEditedModule
     let transImpArts ← fetchTransImportArts directImports info.directArts !header.isModule
     return {
       name := mod.name
+      package? := mod.pkg.id?
       isModule := header.isModule
       imports? := none
       importArts := transImpArts

src/lake/Lake/Config/LeanLib.lean

@@ -58,9 +58,13 @@ The names of the library's root modules
 
 /-- The name of the native library (e.g., what is passed to `-l`). -/
 public def libName (self : LeanLib) : String :=
+  let libName :=
+    if self.config.libName.isEmpty then
+      mkModuleInitializationStem self.name self.pkg.id?
+    else self.config.libName
   if self.libPrefixOnWindows && System.Platform.isWindows then
-    s!"lib{self.config.libName}"
-  else self.config.libName
+    s!"lib{libName}"
+  else libName
 
 /-- The file name of the library's static binary (i.e., its `.a`) -/
 @[inline] public def staticLibFileName (self : LeanLib) : FilePath :=
@@ -84,7 +88,9 @@ public def libName (self : LeanLib) : String :=
 
 /-- Whether the shared binary of this library is a valid plugin. -/
 public def isPlugin (self : LeanLib) : Bool :=
-  self.roots == #[self.name] && self.libName == self.name.mangle ""
+  if h : self.roots.size = 1 then
+    self.libName == mkModuleInitializationStem self.roots[0] self.pkg.id?
+  else false
 
 /-- The library's `extraDepTargets` configuration. -/
 @[inline] public def extraDepTargets (self : LeanLib) :=

src/lake/Lake/Config/LeanLibConfig.lean

@@ -49,7 +49,7 @@ public configuration LeanLibConfig (name : Name) extends LeanConfig where
   Used as a base for the file names of its static and dynamic binaries.
   Defaults to the mangled name of the target.
   -/
-  libName : String := name.mangle ""
+  libName : String := ""
 
   /--
   Whether static and shared binaries of this library should be prefixed with `lib` on Windows.

src/lake/Lake/Config/Module.lean

@@ -147,7 +147,7 @@ public def dynlibSuffix := "-1"
     name used for the module's initialization function, thus enabling it
     to be loaded as a plugin.
   -/
-  self.name.mangle ""
+  mkModuleInitializationStem self.name self.pkg.id?
 
 @[inline] public def dynlibFile (self : Module) : FilePath :=
   self.pkg.leanLibDir / s!"{self.dynlibName}.{sharedLibExt}"

src/lake/Lake/Config/Package.lean

@@ -129,6 +129,10 @@ namespace Package
 @[inline] public def bootstrap (self : Package) : Bool  :=
   self.config.bootstrap
 
+/-- The identifier passed to Lean to disambiguate the package's native symbols. -/
+public def id? (self : Package) : Option PkgId :=
+  if self.bootstrap then none else some <| self.name.toString (escape := false)
+
 /-- The package version. -/
 @[inline] public def version (self : Package) : LeanVer  :=
   self.config.version

src/library/ir_interpreter.cpp

@@ -200,7 +200,6 @@ option_ref<decl> find_ir_decl_boxed(elab_environment const & env, name const & n
 extern "C" double lean_float_of_nat(lean_obj_arg a);
 extern "C" float lean_float32_of_nat(lean_obj_arg a);
 
-static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_mangled_suffix = nullptr;
 static name * g_interpreter_prefer_native = nullptr;
 
@@ -209,9 +208,10 @@ static name * g_interpreter_prefer_native = nullptr;
 static name_hash_map<object *> * g_init_globals;
 
 // reuse the compiler's name mangling to compute native symbol names
-extern "C" object * lean_name_mangle(object * n, object * pre);
-string_ref name_mangle(name const & n, string_ref const & pre) {
-    return string_ref(lean_name_mangle(n.to_obj_arg(), pre.to_obj_arg()));
+/* getSymbolStem (env : Environment) (fn : Name) :  String */
+extern "C" obj_res lean_get_symbol_stem(obj_arg env, obj_arg fn);
+string_ref get_symbol_stem(elab_environment const & env, name const & fn) {
+    return string_ref(lean_get_symbol_stem(env.to_obj_arg(), fn.to_obj_arg()));
 }
 
 extern "C" object * lean_ir_format_fn_body_head(object * b);
@@ -839,7 +839,7 @@ private:
         }
         symbol_cache_entry e_new { get_decl(fn), {nullptr, false} };
         if (m_prefer_native || decl_tag(e_new.m_decl) == decl_kind::Extern || has_init_attribute(m_env, fn)) {
-            string_ref mangled = name_mangle(fn, *g_mangle_prefix);
+            string_ref mangled = get_symbol_stem(m_env, fn);
             string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
             // check for boxed version first
             if (void *p_boxed = lookup_symbol_in_cur_exe(boxed_mangled.data())) {
@@ -961,7 +961,7 @@ private:
             }
         } else {
             if (decl_tag(e.m_decl) == decl_kind::Extern) {
-                string_ref mangled = name_mangle(fn, *g_mangle_prefix);
+                string_ref mangled = get_symbol_stem(m_env, fn);
                 string_ref boxed_mangled(string_append(mangled.to_obj_arg(), g_boxed_mangled_suffix->raw()));
                 throw exception(sstream() << "Could not find native implementation of external declaration '" << fn
                                           << "' (symbols '" << boxed_mangled.data() << "' or '" << mangled.data() << "').\n"
@@ -1184,12 +1184,9 @@ extern "C" LEAN_EXPORT object * lean_eval_const(object * env, object * opts, obj
     }
 }
 
-/* mkModuleInitializationFunctionName (moduleName : Name) : String */
-extern "C" obj_res lean_mk_module_initialization_function_name(obj_arg);
-
-extern "C" LEAN_EXPORT object * lean_run_mod_init(object * mod, object *) {
-    string_ref mangled = string_ref(lean_mk_module_initialization_function_name(mod));
-    if (void * init = lookup_symbol_in_cur_exe(mangled.data())) {
+/* runModInitCore (sym : @& String) : IO Bool */
+extern "C" LEAN_EXPORT obj_res lean_run_mod_init_core(b_obj_arg  sym) {
+    if (void * init = lookup_symbol_in_cur_exe(string_cstr(sym))) {
         auto init_fn = reinterpret_cast<object *(*)(uint8_t)>(init);
         uint8_t builtin = 0;
         object * r = init_fn(builtin);
@@ -1212,8 +1209,6 @@ extern "C" LEAN_EXPORT object * lean_run_init(object * env, object * opts, objec
 }
 
 void initialize_ir_interpreter() {
-    ir::g_mangle_prefix = new string_ref("l_");
-    mark_persistent(ir::g_mangle_prefix->raw());
     ir::g_boxed_mangled_suffix = new string_ref("___boxed");
     mark_persistent(ir::g_boxed_mangled_suffix->raw());
     ir::g_interpreter_prefer_native = new name({"interpreter", "prefer_native"});
@@ -1234,6 +1229,5 @@ void finalize_ir_interpreter() {
     delete ir::g_init_globals;
     delete ir::g_interpreter_prefer_native;
     delete ir::g_boxed_mangled_suffix;
-    delete ir::g_mangle_prefix;
 }
 }

tests/lake/examples/reverse-ffi/Makefile

@@ -9,6 +9,8 @@ all: run run-local
 lake:
 	$(LAKE) --dir=lib build
 
+LIB_NAME=rffi_RFFI
+
 OUT_DIR = out
 LEAN_SYSROOT ?= $(shell lean --print-prefix)
 LEAN_LIBDIR := $(LEAN_SYSROOT)/lib/lean
@@ -23,7 +25,7 @@ endif
 
 $(OUT_DIR)/main: main.c lake | $(OUT_DIR)
 # Add library paths for Lake package and for Lean itself
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS)
+	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS)
 
 run: $(OUT_DIR)/main
 ifeq ($(OS),Windows_NT)
@@ -54,8 +56,8 @@ LEAN_SHLIB_ROOT := $(LEAN_LIBDIR)
 endif
 
 $(OUT_DIR)/main-local: main.c lake | $(OUT_DIR)
-	cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)RFFI.$(SHLIB_EXT) $(OUT_DIR)
-	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -lRFFI -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL)
+	cp -f $(LEAN_SHLIB_ROOT)/*.$(SHLIB_EXT) lib/.lake/build/lib/$(SHLIB_PREFIX)$(LIB_NAME).$(SHLIB_EXT) $(OUT_DIR)
+	cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(OUT_DIR) -l$(LIB_NAME) -lInit_shared -lleanshared_2 -lleanshared_1 -lleanshared $(LINK_FLAGS_LOCAL)
 
 run-local: $(OUT_DIR)/main-local
 	$(OUT_DIR)/main-local

tests/lake/examples/reverse-ffi/main.c

@@ -7,14 +7,14 @@ extern uint64_t my_length(lean_obj_arg);
 extern void lean_initialize_runtime_module();
 extern void lean_initialize();
 extern void lean_io_mark_end_initialization();
-extern lean_object * initialize_RFFI(uint8_t builtin);
+extern lean_object * initialize_rffi_RFFI(uint8_t builtin);
 
 int main() {
   lean_initialize_runtime_module();
   lean_object * res;
   // use same default as for Lean executables
   uint8_t builtin = 1;
-  res = initialize_RFFI(builtin);
+  res = initialize_rffi_RFFI(builtin);
   if (lean_io_result_is_ok(res)) {
       lean_dec_ref(res);
   } else {

tests/lake/examples/targets/lakefile.lean

@@ -11,6 +11,7 @@ lean_lib Foo where
 lean_lib Bar where
   defaultFacets := #[LeanLib.sharedFacet]
   libPrefixOnWindows := true
+  libName := "Bar"
 
 lean_lib Baz where
   extraDepTargets := #[`caw]

tests/lake/examples/targets/test.sh

@@ -17,6 +17,8 @@ LIB_PREFIX=lib
 SHARED_LIB_EXT=so
 fi
 
+PKG=targets
+
 ./clean.sh
 
 # Test error on nonexistent facet
@@ -69,19 +71,19 @@ test -f ./.lake/build/ir/Bar.c.o.export
 # Test default targets
 test ! -f ./.lake/build/bin/c
 test ! -f ./.lake/build/lib/lean/Foo.olean
-test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.a
+test ! -f ./.lake/build/lib/${LIB_PREFIX}${PKG}_Foo.a
 test ! -f ./.lake/build/meow.txt
 $LAKE build targets/
 ./.lake/build/bin/c
 test -f ./.lake/build/lib/lean/Foo.olean
-test -f ./.lake/build/lib/${LIB_PREFIX}Foo.a
+test -f ./.lake/build/lib/${LIB_PREFIX}${PKG}_Foo.a
 cat ./.lake/build/meow.txt | grep Meow!
 
 # Test shared lib facets
-test ! -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
+test ! -f ./.lake/build/lib/${LIB_PREFIX}${PKG}_Foo.$SHARED_LIB_EXT
 test ! -f ./.lake/build/lib/libBar.$SHARED_LIB_EXT
 $LAKE build Foo:shared Bar
-test -f ./.lake/build/lib/${LIB_PREFIX}Foo.$SHARED_LIB_EXT
+test -f ./.lake/build/lib/${LIB_PREFIX}${PKG}_Foo.$SHARED_LIB_EXT
 test -f ./.lake/build/lib/libBar.$SHARED_LIB_EXT
 
 # Test static lib facet
@@ -90,9 +92,9 @@ $LAKE build Foo:shared Bar:static
 test -f ./.lake/build/lib/libBar.a
 
 # Test dynlib facet
-test ! -f ./.lake/build/lib/lean/Foo.$SHARED_LIB_EXT
+test ! -f ./.lake/build/lib/lean/${PKG}_Foo.$SHARED_LIB_EXT
 $LAKE build +Foo:dynlib
-test -f ./.lake/build/lib/lean/Foo.$SHARED_LIB_EXT
+test -f ./.lake/build/lib/lean/${PKG}_Foo.$SHARED_LIB_EXT
 
 # Test library `extraDepTargets`
 test ! -f ./.lake/build/caw.txt

tests/lake/tests/precompileLink/test.sh

@@ -3,6 +3,7 @@ source ../common.sh
 
 ./clean.sh
 
+
 # Test that precompilation works with a Lake import
 # https://github.com/leanprover/lean4/issues/7388
 test_run -v build LakeTest
@@ -22,12 +23,13 @@ test_maybe_err "-lBogus" build -KlinkArgs=-lBogus
 ./clean.sh
 
 # Test that dynlibs are part of the module trace unless `platformIndependent` is set
+PKG=precompileArgs
 test_run build -R
-echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+echo foo > .lake/build/lib/lean/${PKG}_Foo_Bar.$SHARED_LIB_EXT
 test_err "Building Foo" build --rehash
-test_cmd rm .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+test_cmd rm .lake/build/lib/lean/${PKG}_Foo_Bar.$SHARED_LIB_EXT
 test_run build -R -KplatformIndependent=true
-echo foo > .lake/build/lib/lean/Foo_Bar.$SHARED_LIB_EXT
+echo foo > .lake/build/lib/lean/${PKG}_Foo_Bar.$SHARED_LIB_EXT
 test_run build --rehash --no-build
 
 # cleanup

tests/pkg/def_clash/Test/BarA.lean

@@ -0,0 +1,3 @@
+module
+
+public def bar : String := "barA"

tests/pkg/def_clash/Test/BarB.lean

@@ -0,0 +1,3 @@
+module
+
+public def bar : String := "barB"

tests/pkg/def_clash/Test/UseBarA.lean

@@ -0,0 +1,4 @@
+module
+import Test.BarA
+
+public def useBarA : String := bar

tests/pkg/def_clash/Test/UseBarB.lean

@@ -0,0 +1,4 @@
+module
+import Test.BarB
+
+public def useBarB : String := bar

tests/pkg/def_clash/TestLocalUse.lean

@@ -0,0 +1,9 @@
+module
+import Test.UseBarA
+import Test.UseBarB
+
+public def main : IO Unit := do
+  IO.print useBarA
+  IO.print "; "
+  IO.print useBarB
+  IO.print "\n"

tests/pkg/def_clash/TestUse.lean

@@ -2,6 +2,8 @@ module
 import UseA
 import UseB
 
-def main : IO Unit := do
-  IO.println useA
-  IO.println useB
+public def main : IO Unit := do
+  IO.print useA
+  IO.print "; "
+  IO.print useB
+  IO.print "\n"

tests/pkg/def_clash/lakefile.toml

@@ -1,5 +1,9 @@
 name = "test"
 
+[[lean_lib]]
+name = "Test"
+leanOptions.experimental.module = true
+
 [[lean_lib]]
 name = "TestFoo"
 leanOptions.experimental.module = true
@@ -8,6 +12,10 @@ leanOptions.experimental.module = true
 name = "TestUse"
 leanOptions.experimental.module = true
 
+[[lean_exe]]
+name = "TestLocalUse"
+leanOptions.experimental.module = true
+
 [[require]]
 name = "useA"
 path = "deps/useA"

tests/pkg/def_clash/test.sh

@@ -1,18 +1,22 @@
 #!/usr/bin/env bash
 
-# Tests the behavior of transitively importing multiple modules
-# that define the same symbol.
+# The test covers the behavior of transitively importing multiple modules
+# that have a definition with the same name.
 
-# Currently, if two packages define the same Lean symbol (e.g., `foo`)
-# they cannot be in the same transitive import graph, even if the no module
-# can see both instances of the symbol.
+# The native symbols Lean emits are prefixed with a package identifier
+# received from Lake. Thus, symbol clashes should not occur between packages.
+# However, they can still occur within them.
 
-# In the example in this directory, `fooA` and `fooB` both define `foo`.
+# Related Issues:
+# https://github.com/leanprover/lean4/issues/222
+
+# In the example in this directory, packages `fooA` and `fooB` both define `foo`.
 # `useA` privately imports and uses `fooA`, and `useB` private imports and uses
-# `fooB`. When `TestUse` imports `useA` and `useB`, the linker will complain
-# even though the Lean file does not see both `foo` definitions.
+# `fooB`. The executable `TestUse` then imports and uses `useA` and `useB`.
 
-# See also https://github.com/leanprover/lean4/issues/222
+# Similarly, modules `Test.BarA` and `Test.BarB` both define `bar`.
+# Modules `UseBarA` and `UseBarB` use them (privately), and `TestLocalUse`
+# imports both.
 
 source ../../lake/tests/common.sh
 
@@ -23,5 +27,9 @@ source ../../lake/tests/common.sh
 test_err "environment already contains 'foo'" build TestFoo
 
 # Test the behavior when multiple copies of the same definition (`foo`) exist
-# but are not visible to any one module: a symbol clash between the two `foo`s.
-test_err "l_foo" build TestUse
+# in different packages but are not visible to any one module.
+test_out "fooA; fooB" exe TestUse
+
+# Test the behavior when multiple copies of the same definition (`foo`) exist
+# in the same package but are not visible to any one module.
+test_err "lp_test_bar" build TestLocalUse

tests/pkg/user_plugin/test.sh

@@ -19,10 +19,11 @@ lake update -q
 
 # Build plugins
 lake build
+PKG=user__plugin # mangled
 LIB_DIR=.lake/build/lib
 check_plugin () {
   plugin=$1
-  shlib=$LIB_DIR/${LIB_PREFIX}$plugin.$SHLIB_EXT
+  shlib=$LIB_DIR/${LIB_PREFIX}${PKG}_$plugin.$SHLIB_EXT
   test -f $shlib || {
     echo "$plugin library not found; $LIB_DIR contains:"
     ls $LIB_DIR
@@ -31,8 +32,8 @@ check_plugin () {
 }
 check_plugin UserPlugin
 check_plugin UserEnvPlugin
-PLUGIN=$LIB_DIR/${LIB_PREFIX}UserPlugin.$SHLIB_EXT
-ENV_PLUGIN=$LIB_DIR/${LIB_PREFIX}UserEnvPlugin.$SHLIB_EXT
+PLUGIN=$LIB_DIR/${LIB_PREFIX}${PKG}_UserPlugin.$SHLIB_EXT
+ENV_PLUGIN=$LIB_DIR/${LIB_PREFIX}${PKG}_UserEnvPlugin.$SHLIB_EXT
 
 # Expected test output
 EXPECTED_OUT="Ran builtin initializer"