From 8e6f2750dad101296a43a4d463bc8dfc29b03452 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 20 Mar 2026 14:27:26 +0100 Subject: [PATCH] fix: namespace used in private import and current module vanishes dowstream (#12840) This PR fixes an issue where the use of private imports led to unknown namespaces in downstream modules. Fixes #12833 --- src/Lean/Data/SMap.lean | 6 +++ src/Lean/Environment.lean | 3 +- src/Lean/Namespace.lean | 54 ++++++++++++------- .../Completion/CompletionCollectors.lean | 2 +- stage0/src/stdlib_flags.h | 4 +- tests/pkg/module/Module/Basic.lean | 3 ++ .../Module/ImportedPrivateImported.lean | 3 ++ tests/pkg/module/Module/PrivateImported.lean | 3 ++ 8 files changed, 56 insertions(+), 22 deletions(-) diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean index 0cb3f5ff0f..ccdfb90147 100644 --- a/src/Lean/Data/SMap.lean +++ b/src/Lean/Data/SMap.lean @@ -8,6 +8,9 @@ module prelude public import Std.Data.HashMap.Basic public import Lean.Data.PersistentHashMap +public import Std.Data.HashMap.Iterator +public import Lean.Data.Iterators.Producers.PersistentHashMap +public import Init.Data.Iterators.Combinators.Append public section universe u v w w' @@ -86,6 +89,9 @@ instance [Monad m] : ForM m (SMap α β) (α × β) where instance [Monad m] : ForIn m (SMap α β) (α × β) where forIn := ForM.forIn +def iter (s : SMap α β) := + s.map₁.iter.append s.map₂.iter + /-- Move from stage 1 into stage 2. -/ def switch (m : SMap α β) : SMap α β := if m.stage₁ then { m with stage₁ := false } else m diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 38343bbf77..6087fcb74a 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -525,11 +525,12 @@ where go parent? aconsts := do go (some c) c.aconsts.get /-- Accessibility levels of declarations in `Lean.Environment`. -/ -private inductive Visibility where +inductive Environment.Visibility where /-- Information private to the module. -/ | «private» /-- Information to be exported to other modules. -/ | «public» +deriving Inhabited, BEq /-- Maps `Visibility` to `α`. -/ private structure VisibilityMap (α : Type) where diff --git a/src/Lean/Namespace.lean b/src/Lean/Namespace.lean index a4e09cf284..9a08e11f41 100644 --- a/src/Lean/Namespace.lean +++ b/src/Lean/Namespace.lean @@ -8,41 +8,59 @@ module prelude public import Lean.EnvExtension -public section - namespace Lean +/-- +Map from namespace name to (max) visibility of (any) defining module. Namespaces do not have +visibility of their own. We use this information to avoid redeclaring namespaces that would always +be provided by an import anyway. +-/ +abbrev State := SMap Name Environment.Visibility + /-- Environment extension for tracking all `namespace` declared by users. -/ -builtin_initialize namespacesExt : SimplePersistentEnvExtension Name NameSSet ← - registerSimplePersistentEnvExtension { - addImportedFn := fun as => +private builtin_initialize namespacesExt : PersistentEnvExtension Name Name State ← + registerPersistentEnvExtension { + mkInitial := pure {} + addImportedFn := fun as => do + let env := (← read).env /- - We compute a `HashMap Name Unit` and then convert to `NameSSet` to improve Lean startup time. + We compute a `HashMap` and then convert to `SMap` to improve Lean startup time. Note: we have used `perf` to profile Lean startup cost when processing a file containing just `import Lean`. 6.18% of the runtime is here. It was 9.31% before the `HashMap` optimization. -/ let capacity := as.foldl (init := 0) fun r e => r + e.size - let map : Std.HashMap Name Unit := Std.HashMap.emptyWithCapacity capacity - let map := mkStateFromImportedEntries (fun map name => map.insert name ()) map as - SMap.fromHashMap map |>.switch - addEntryFn := fun s n => s.insert n + let mut map : Std.HashMap Name Environment.Visibility := Std.HashMap.emptyWithCapacity capacity + for mod in env.header.modules, modEntries in as do + let vis := if mod.isExported then .public else .private + for e in modEntries do + map := map.alter e fun + | some .public => some .public + | _ => some vis + return SMap.fromHashMap map |>.switch + -- local entries are not from private imports, so mark public + addEntryFn := fun s n => s.insert n .public + exportEntriesFn s := + let entries := s.map₂.toArray.map (·.1) + entries.qsort (·.quickLt) -- Namespaces from local helper constants can be disregarded in other environment branches. We - -- do *not* want `getNamespaceSet` to have to wait on all prior branches. + -- do *not* want `getNamespaces` to have to wait on all prior branches. asyncMode := .local } namespace Environment /-- Register a new namespace in the environment. -/ -def registerNamespace (env : Environment) (n : Name) : Environment := - if (namespacesExt.getState env).contains n then env else namespacesExt.addEntry env n +public def registerNamespace (env : Environment) (n : Name) : Environment := + -- Can only skip registering imported namespaces for public imports + if namespacesExt.getState env |>.find? n |>.any (· == .public) then env else + namespacesExt.addEntry env n /-- Return `true` if `n` is the name of a namespace in `env`. -/ -def isNamespace (env : Environment) (n : Name) : Bool := - (namespacesExt.getState env).contains n +public def isNamespace (env : Environment) (n : Name) : Bool := + namespacesExt.getState env |>.contains n -/-- Return a set containing all namespaces in `env`. -/ -def getNamespaceSet (env : Environment) : NameSSet := - namespacesExt.getState env +/-- Returns an iterator over all namespaces in `env`. -/ +public def getNamespaces (env : Environment) := + namespacesExt.getState env |>.iter.map (·.1) diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 2382a8f286..db21662deb 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -220,7 +220,7 @@ section IdCompletionUtils private def completeNamespaces (ctx : ContextInfo) (id : Name) (danglingDot : Bool) : M Unit := do let env ← getEnv - env.getNamespaceSet |>.forM fun ns => do + for ns in env.getNamespaces do unless ns.isInternal || env.contains ns do -- Ignore internal and namespaces that are also declaration names let label? ← bestLabelForDecl? ctx ns id danglingDot if let some bestLabel := label? then diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e444447049..6863f1e9f6 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -11,12 +11,12 @@ options get_default_options() { opts = opts.update({"debug", "terminalTacticsAsSorry"}, false); // switch to `true` for ABI-breaking changes affecting meta code; // see also next option! - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `false` when enabling `prefer_native` should also affect use // of built-in parsers in quotations; this is usually the case, but setting // both to `true` may be necessary for handling non-builtin parsers with // builtin elaborators - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // changes to builtin parsers may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true); diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 75405e7e6a..7edd9972b6 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -558,3 +558,6 @@ public def func (ctx : Nat) (operand : OpOperand2) : Nat := match operand.nextUse with | none => ctx | some _nextPtr => ctx + +/-- Setup for #12833. -/ +public def Namespaced.def := 0 diff --git a/tests/pkg/module/Module/ImportedPrivateImported.lean b/tests/pkg/module/Module/ImportedPrivateImported.lean index 0247380866..d907685ce6 100644 --- a/tests/pkg/module/Module/ImportedPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedPrivateImported.lean @@ -12,3 +12,6 @@ public import Module.PrivateImported /-- info: 5 -/ #guard_msgs in #eval publicDefOfPrivatelyInitialized + +/-! #12833: namespaces privately imported but publicly used must be re-exported. -/ +open Namespaced diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean index f838123fac..555f3d49a2 100644 --- a/tests/pkg/module/Module/PrivateImported.lean +++ b/tests/pkg/module/Module/PrivateImported.lean @@ -29,3 +29,6 @@ public def publicDefOfPrivatelyInitialized := initialized /-! #12198: `local simp` should be accepted on privately imported theorem -/ attribute [local simp] t + +/-- Setup for #12833. -/ +public def Namespaced.def2 := 0