From 57132aebaaf70ad9b0d0d2b0b791c0977a9cf5da Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 14 Jul 2026 13:06:22 +0000 Subject: [PATCH 1/4] feat: add `@[trusted_axiom]` attribute and `linter.untrustedAxioms` linter This PR adds a `@[trusted_axiom]` attribute for marking axioms as trusted and a new (default-off) `linter.untrustedAxioms` linter that warns when a declaration added to the environment transitively depends on an axiom not tagged `@[trusted_axiom]`. Co-Authored-By: Claude --- src/Lean/Elab/MutualDef.lean | 9 ++ src/Lean/TrustedAxiomAttr.lean | 53 +++++++++ tests/elab/linterUntrustedAxioms.lean | 149 ++++++++++++++++++++++++++ 3 files changed, 211 insertions(+) create mode 100644 src/Lean/TrustedAxiomAttr.lean create mode 100644 tests/elab/linterUntrustedAxioms.lean diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 81f3d84a62a9..0907b79ac798 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -7,6 +7,7 @@ module prelude public import Lean.Elab.Deriving.Basic public import Lean.Elab.PreDefinition.Main +import Lean.TrustedAxiomAttr import all Lean.Elab.ErrorUtils public section namespace Lean.Elab @@ -1441,6 +1442,14 @@ this warning can be disabled with `set_option warn.classDefReducibility false`." addPreDefinitions docCtx preDefs for view in views, funFVar in funFVars do addLocalVarInfo view.declId funFVar + if Linter.getLinterValue linter.untrustedAxioms (← Linter.getLinterOptions) then + -- lint on the kernel-check chain so that `collectAxioms` does not block elaboration + let act ← Core.wrapAsyncAsSnapshot (cancelTk? := none) + (desc := s!"linting axioms of {headers.map (·.declName)}") fun _ => + for header in headers do + withRef header.declId <| warnIfUsesUntrustedAxioms header.declName + let task ← BaseIO.mapTask act (← getEnv).checked + Core.logSnapshotTask { stx? := none, reportingRange := .skip, cancelTk? := none, task } processDeriving (headers : Array DefViewElabHeader) := do for header in headers, view in views do diff --git a/src/Lean/TrustedAxiomAttr.lean b/src/Lean/TrustedAxiomAttr.lean new file mode 100644 index 000000000000..453274d1e0df --- /dev/null +++ b/src/Lean/TrustedAxiomAttr.lean @@ -0,0 +1,53 @@ +/- +Copyright (c) 2026 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sebastian Ullrich +-/ +module + +prelude +public import Lean.Attributes +import Lean.Util.CollectAxioms +import Lean.Util.Sorry +import Lean.Linter.Init +import Lean.AddDecl + +namespace Lean + +/-- +Marks an axiom as "trusted" so that the `linter.untrustedAxioms` linter does not warn about +declarations depending on axioms tagged with this attribute. +-/ +@[builtin_doc] +public builtin_initialize trustedAxiomAttr : TagAttribute ← + registerTagAttribute `trusted_axiom "mark an axiom as trusted so that `linter.untrustedAxioms` does not warn about declarations depending on it" fun declName => do + unless getOriginalConstKind? (← getEnv) declName matches some .axiom do + throwError "Cannot add attribute `@[trusted_axiom]` to non-axiom `{.ofConstName declName}`" + +public register_builtin_option linter.untrustedAxioms : Bool := { + defValue := false + descr := "Warn when a declaration added to the environment depends on an axiom that is not \ + tagged with `@[trusted_axiom]`. This should be considered a preliminary elaboration-side \ + check that does not replace the use of external checker tools such as `comparator` with \ + their own axiom checks." +} + +open Linter in +public def warnIfUsesUntrustedAxioms (declName : Name) : CoreM Unit := do + unless getLinterValue linter.untrustedAxioms (← getLinterOptions) do return + if (← MonadLog.hasErrors) then return + let env ← getEnv + let some info := env.find? declName | return + if info.isUnsafe then return + if warn.sorry.get (← getOptions) && + (info.type.hasSorry || (info.value? (allowOpaque := true)).any (·.hasSorry)) then + return + let axioms ← collectAxioms declName + let offending := axioms.filter (!trustedAxiomAttr.hasTag env ·) + unless offending.isEmpty do + let axMsgs := offending.toList.map fun ax => m!"`{MessageData.ofConstName ax}`" + logLint linter.untrustedAxioms (← getRef) + m!"declaration depends on axioms that are not tagged \ + `@[trusted_axiom]`: {MessageData.joinSep axMsgs ", "}" + +end Lean diff --git a/tests/elab/linterUntrustedAxioms.lean b/tests/elab/linterUntrustedAxioms.lean new file mode 100644 index 000000000000..7fa5d7976d96 --- /dev/null +++ b/tests/elab/linterUntrustedAxioms.lean @@ -0,0 +1,149 @@ +/-! +Tests the `@[trusted_axiom]` attribute and the `linter.untrustedAxioms` linter, which warns when a +declaration transitively depends on an axiom not tagged `@[trusted_axiom]`. +-/ + +axiom untrustedAx : 1 = 2 + +@[trusted_axiom] axiom trustedAx : 1 = 1 + +-- The linter is off by default. +#guard_msgs in +theorem offByDefault : 1 = 2 := untrustedAx + +set_option linter.untrustedAxioms true + +/-! Axiom declarations themselves are not linted, only their uses. -/ + +#guard_msgs in +axiom anotherUntrustedAx : 2 = 3 + +#guard_msgs in +@[trusted_axiom] axiom anotherTrustedAx : 2 = 2 + +/-! Direct use of an untrusted axiom warns; use of a trusted axiom does not. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesUntrusted : 1 = 2 := untrustedAx + +#guard_msgs in +theorem usesTrusted : 1 = 1 := trustedAx + +/-! Transitive dependencies are reported. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesTransitively : 2 = 1 := usesUntrusted.symm + +/-! All offending axioms are listed in a single warning. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `anotherUntrustedAx`, `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesBoth : 1 = 3 := untrustedAx.trans anotherUntrustedAx + +/-! Private declarations are linted as well. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +private theorem privateUses : 1 = 2 := untrustedAx + +/-! +Internal auxiliary declarations (e.g. `match` functions) are not linted separately; their axioms +are reported once via the surrounding declaration. +-/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesViaMatch : (n : Nat) → 1 = 2 + | 0 => untrustedAx + | _+1 => untrustedAx + +/-! +`sorryAx` is not reported for a declaration containing the `sorry` itself, which already produces +the `warn.sorry` warning. +-/ + +/-- +warning: declaration uses `sorry` +-/ +#guard_msgs in +theorem usesSorry : 1 = 2 := sorry + +/-! Transitive `sorry`s are not covered by `warn.sorry`, so `sorryAx` is reported for them. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `sorryAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +theorem usesSorryTransitively : 2 = 1 := usesSorry.symm + +/-! The synchronous elaboration path warns as well. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +set_option Elab.async false in +theorem usesUntrustedSync : 1 = 2 := untrustedAx + +/-! `example`s are linted. -/ + +/-- +warning: declaration depends on axioms that are not tagged `@[trusted_axiom]`: `untrustedAx` + +Note: This linter can be disabled with `set_option linter.untrustedAxioms false` +-/ +#guard_msgs in +example : 1 = 2 := untrustedAx + +/-! Explicitly disabling the linter wins over `linter.all`. -/ + +set_option linter.all true in +set_option linter.untrustedAxioms false in +#guard_msgs in +theorem explicitOff : 1 = 2 := untrustedAx + +/-! The attribute can only be applied to axioms in the current module. -/ + +def notAnAxiom : Nat := 1 + +/-- error: Cannot add attribute `@[trusted_axiom]` to non-axiom `notAnAxiom` -/ +#guard_msgs in +attribute [trusted_axiom] notAnAxiom + +/-- +error: Cannot add attribute `[trusted_axiom]` to declaration `propext` because it is in an imported module +-/ +#guard_msgs in +attribute [trusted_axiom] propext + +/-- +error: Invalid attribute scope: Attribute `[trusted_axiom]` must be global, not `local` +-/ +#guard_msgs in +attribute [local trusted_axiom] anotherUntrustedAx From 5cabad2bacdee7d691e7abd5cdd491c1db7ff71a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Jul 2026 09:39:06 +0000 Subject: [PATCH 2/4] perf: record axiom dependencies eagerly during kernel checking MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `linter.untrustedAxioms` called `collectAxioms` with a fresh cache per declaration, re-walking the module-local dependency subgraph each time (up to +20% instructions on proof-heavy stdlib modules, which enable the linter via `set_option linter.all true`). `exportedAxiomsExt` is now `sync` and filled eagerly by `recordAxioms` from `addDecl`, so entries accumulate along the `checked` environment chain and each constant is walked only once per module; olean serialization reuses the recorded entries instead of recomputing them, making the eager fill instruction-neutral when the linter is off (`Std.Data.DTreeMap.Internal.WF.Lemmas` with export: linter off 40.29G → 40.31G instructions, linter on 48.85G → 42.01G; the remaining enabled-mode delta is mostly warning emission, which core axiom tagging will remove). Also, the `hasSorry` suppression check now runs only when `sorryAx` appears in the collected axioms, skipping the term traversal for sorry-free declarations. Co-Authored-By: Claude --- src/Lean/AddDecl.lean | 1 + src/Lean/TrustedAxiomAttr.lean | 6 +++-- src/Lean/Util/CollectAxioms.lean | 43 ++++++++++++++++++++++++++------ 3 files changed, 40 insertions(+), 10 deletions(-) diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean index e302ee1d4e73..16416cf6b767 100644 --- a/src/Lean/AddDecl.lean +++ b/src/Lean/AddDecl.lean @@ -192,6 +192,7 @@ where -- avoid follow-up errors by (trying to) add broken decl as axiom addAsAxiom throw ex + recordAxioms decl addAsAxiom := do -- try to add as axiom with given type for def/theorem match decl with diff --git a/src/Lean/TrustedAxiomAttr.lean b/src/Lean/TrustedAxiomAttr.lean index 453274d1e0df..51e9a2b4e329 100644 --- a/src/Lean/TrustedAxiomAttr.lean +++ b/src/Lean/TrustedAxiomAttr.lean @@ -39,10 +39,12 @@ public def warnIfUsesUntrustedAxioms (declName : Name) : CoreM Unit := do let env ← getEnv let some info := env.find? declName | return if info.isUnsafe then return - if warn.sorry.get (← getOptions) && + let axioms ← collectAxioms declName + -- Check the axioms first: a syntactic `sorry` always shows up as `sorryAx` in them, so we can + -- avoid the `hasSorry` term traversal for sorry-free declarations. + if axioms.contains ``sorryAx && warn.sorry.get (← getOptions) && (info.type.hasSorry || (info.value? (allowOpaque := true)).any (·.hasSorry)) then return - let axioms ← collectAxioms declName let offending := axioms.filter (!trustedAxiomAttr.hasTag env ·) unless offending.isEmpty do let axMsgs := offending.toList.map fun ax => m!"`{MessageData.ofConstName ax}`" diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean index dc9897059a44..fea698c1ea08 100644 --- a/src/Lean/Util/CollectAxioms.lean +++ b/src/Lean/Util/CollectAxioms.lean @@ -95,10 +95,12 @@ binary search without requiring the extension object. -/ private structure ExportedAxiomsState where importedModuleEntries : Array (Array (Name × Array Name)) := #[] + /-- Axiom dependencies of current-module declarations, filled eagerly by `recordAxioms`. -/ + localEntries : NameMap (Array Name) := {} instance : Inhabited ExportedAxiomsState := ⟨{}⟩ -/-- Look up pre-computed axioms for an imported declaration. -/ +/-- Look up pre-computed axioms for an imported or already-recorded local declaration. -/ private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environment) (c : Name) : Option (Array Name) := match env.getModuleIdxFor? c with @@ -108,14 +110,17 @@ private def ExportedAxiomsState.find? (s : ExportedAxiomsState) (env : Environme | some entry => some entry.2 | none => none else none - | none => none + | none => s.localEntries.find? c /-- Environment extension that records axiom dependencies for all declarations in a module. -Entries are computed once by `beforeExportFn` when the olean is serialized, not during -elaboration. During elaboration, `collectAxioms` walks bodies directly. Downstream modules -look up pre-computed entries for imported declarations, so axiom collection never crosses -module boundaries. +Entries for the current module are filled eagerly by `recordAxioms` as declarations pass the +kernel; the `sync` mode makes these writes accumulate along the `checked` environment chain so +that recording a declaration reuses the entries of all prior declarations. When the olean is +serialized, `exportEntriesFnEx` exports the entries of all exported declarations, computing any +entry missing due to e.g. realizations or error recovery. Downstream modules look up +pre-computed entries for imported declarations, so axiom collection never crosses module +boundaries. -/ private builtin_initialize exportedAxiomsExt : PersistentEnvExtension (Name × Array Name) (Name × Array Name) ExportedAxiomsState ← @@ -142,14 +147,36 @@ private builtin_initialize exportedAxiomsExt : -- Sort by name for binary search at import time. let entries := entries.qsort fun a b => Name.quickLt a.1 b.1 .uniform entries - asyncMode := .mainOnly + asyncMode := .sync } +/-- +Computes and records the axiom dependencies of the given just-added declaration into +`exportedAxiomsExt`. Entries recorded for earlier declarations are reused, so each constant is +walked only once per module. Skipped in realization contexts, which would require extension +replay; declarations without an entry are walked on demand by `collectAxioms` instead. +-/ +public def recordAxioms [Monad m] [MonadEnv m] (decl : Declaration) : m Unit := do + let env ← getEnv + if env.isRealizing then return + let privateEnv := env.setExporting false + let s := exportedAxiomsExt.getState env + let (_, st) := decl.getTopLevelNames.mapM (CollectAxioms.collectAndGet s.find?) + |>.run privateEnv |>.run {} + let newEntries := st.seen.foldl (init := #[]) fun acc c axs => + if (env.getModuleIdxFor? c).isNone && !s.localEntries.contains c then + acc.push (c, axs) + else + acc + unless newEntries.isEmpty do + modifyEnv fun env => exportedAxiomsExt.modifyState env fun s => + { s with localEntries := newEntries.foldl (init := s.localEntries) fun m (c, axs) => m.insert c axs } + /-- Collect all axioms transitively used by a constant. -/ public def collectAxioms [Monad m] [MonadEnv m] (constName : Name) : m (Array Name) := do let env ← getEnv let privateEnv := env.setExporting false - let s := exportedAxiomsExt.getState (asyncMode := .mainOnly) env + let s := exportedAxiomsExt.getState env return CollectAxioms.runM privateEnv do CollectAxioms.collectAndGet s.find? constName From b978969c192185e8950f5aaa157627763b68ac51 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Jul 2026 09:50:20 +0000 Subject: [PATCH 3/4] fix: do not enable `linter.untrustedAxioms` via `linter.all` The linter now runs only when `linter.untrustedAxioms` is set explicitly, instead of also being enabled by `linter.all`. The check is useful only with a curated set of `@[trusted_axiom]` declarations and comes with per-declaration cost, so it should not be implied by a blanket linter enable; in particular, the stdlib sets `set_option linter.all true` in many files, which flooded stdlib builds with warnings about the not-yet-tagged core axioms (with `@[trusted_axiom]` tags for them still pending on a stage0 update). `Std.Data.DTreeMap.Internal.WF.Lemmas` now builds warning-free at 40.30G instructions, matching the linter-off baseline. Co-Authored-By: Claude --- src/Lean/Elab/MutualDef.lean | 2 +- src/Lean/TrustedAxiomAttr.lean | 6 ++++-- tests/elab/linterUntrustedAxioms.lean | 8 ++++++-- 3 files changed, 11 insertions(+), 5 deletions(-) diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 0907b79ac798..f500d9b013c0 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -1442,7 +1442,7 @@ this warning can be disabled with `set_option warn.classDefReducibility false`." addPreDefinitions docCtx preDefs for view in views, funFVar in funFVars do addLocalVarInfo view.declId funFVar - if Linter.getLinterValue linter.untrustedAxioms (← Linter.getLinterOptions) then + if linter.untrustedAxioms.get (← getOptions) then -- lint on the kernel-check chain so that `collectAxioms` does not block elaboration let act ← Core.wrapAsyncAsSnapshot (cancelTk? := none) (desc := s!"linting axioms of {headers.map (·.declName)}") fun _ => diff --git a/src/Lean/TrustedAxiomAttr.lean b/src/Lean/TrustedAxiomAttr.lean index 51e9a2b4e329..fbc44559408b 100644 --- a/src/Lean/TrustedAxiomAttr.lean +++ b/src/Lean/TrustedAxiomAttr.lean @@ -29,12 +29,14 @@ public register_builtin_option linter.untrustedAxioms : Bool := { descr := "Warn when a declaration added to the environment depends on an axiom that is not \ tagged with `@[trusted_axiom]`. This should be considered a preliminary elaboration-side \ check that does not replace the use of external checker tools such as `comparator` with \ - their own axiom checks." + their own axiom checks. Unlike other linters, this linter is not enabled by `linter.all` \ + but only by setting this option explicitly, as it is useful only with a curated set of \ + `@[trusted_axiom]` declarations." } open Linter in public def warnIfUsesUntrustedAxioms (declName : Name) : CoreM Unit := do - unless getLinterValue linter.untrustedAxioms (← getLinterOptions) do return + unless linter.untrustedAxioms.get (← getOptions) do return if (← MonadLog.hasErrors) then return let env ← getEnv let some info := env.find? declName | return diff --git a/tests/elab/linterUntrustedAxioms.lean b/tests/elab/linterUntrustedAxioms.lean index 7fa5d7976d96..a8a6632edc40 100644 --- a/tests/elab/linterUntrustedAxioms.lean +++ b/tests/elab/linterUntrustedAxioms.lean @@ -11,6 +11,11 @@ axiom untrustedAx : 1 = 2 #guard_msgs in theorem offByDefault : 1 = 2 := untrustedAx +-- `linter.all` does not enable this linter; it must be enabled explicitly. +set_option linter.all true in +#guard_msgs in +theorem allDoesNotEnable : 1 = 2 := untrustedAx + set_option linter.untrustedAxioms true /-! Axiom declarations themselves are not linted, only their uses. -/ @@ -121,9 +126,8 @@ Note: This linter can be disabled with `set_option linter.untrustedAxioms false` #guard_msgs in example : 1 = 2 := untrustedAx -/-! Explicitly disabling the linter wins over `linter.all`. -/ +/-! Explicitly disabling the linter. -/ -set_option linter.all true in set_option linter.untrustedAxioms false in #guard_msgs in theorem explicitOff : 1 = 2 := untrustedAx From 49216109a0953233e92f9fc0bc95caed066547ab Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 16 Jul 2026 11:58:58 +0000 Subject: [PATCH 4/4] refactor: make `CollectAxioms` per-run cache a second layer over recorded entries The per-run `seen` cache no longer copies entries answered by `exportedAxiomsExt`; it now contains exactly the constants walked by the run, forming a second layer over the recorded entries. `collectAndGet` answers imported and already-recorded constants directly, and `recordAxioms` inserts the walked constants wholesale instead of filtering every referenced constant. Measured neutral on elaboration benchmarks (the dominant eager-fill cost is the `getUsedConstants` term walk itself, which is accepted); reduces per-declaration allocation and map bookkeeping. Co-Authored-By: Claude --- src/Lean/Util/CollectAxioms.lean | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/Lean/Util/CollectAxioms.lean b/src/Lean/Util/CollectAxioms.lean index fea698c1ea08..df92b84ef296 100644 --- a/src/Lean/Util/CollectAxioms.lean +++ b/src/Lean/Util/CollectAxioms.lean @@ -13,7 +13,11 @@ namespace Lean namespace CollectAxioms structure State where - /-- Cache mapping constants to their (sorted) axiom dependencies. -/ + /-- + Cache mapping constants walked by this run to their (sorted) axiom dependencies. Constants + answered by `extFind?` are deliberately not copied into this layer, so it contains exactly the + constants whose dependencies were not already recorded elsewhere. + -/ seen : NameMap (Array Name) := {} /-- Axioms accumulated for the current constant being processed. -/ axioms : NameSet := {} @@ -28,7 +32,8 @@ private def insertArray (s : NameSet) (axs : Array Name) : NameSet := /-- Collect axioms reachable from constant `c`, using `extFind?` to look up pre-computed axioms -for imported declarations. Results are cached in `State.seen`. +for imported and already-recorded declarations. Results for walked constants are cached in +`State.seen`, the second layer of the cache on top of `extFind?`. When processing a constant not found in `extFind?` or the cache, the function temporarily clears the axiom accumulator, recurses into the constant's dependencies, caches the result @@ -38,9 +43,9 @@ private partial def collect (extFind? : Environment → Name → Option (Array Name)) (c : Name) : M Unit := do let env ← read - -- Check extension for pre-computed axioms (imported declarations) + -- Check extension for pre-computed axioms (imported and already-recorded declarations) if let some axs := extFind? env c then - modify fun s => { s with axioms := insertArray s.axioms axs, seen := s.seen.insert c axs } + modify fun s => { s with axioms := insertArray s.axioms axs } return -- Check local cache let s ← get @@ -77,6 +82,8 @@ private partial def collect private def collectAndGet (extFind? : Environment → Name → Option (Array Name)) (c : Name) : M (Array Name) := do + if let some axs := extFind? (← read) c then + return axs collect extFind? c let some axs := (← get).seen.find? c | panic! s!"collectAndGet: '{c}' not in seen after collect" return axs @@ -163,8 +170,10 @@ public def recordAxioms [Monad m] [MonadEnv m] (decl : Declaration) : m Unit := let s := exportedAxiomsExt.getState env let (_, st) := decl.getTopLevelNames.mapM (CollectAxioms.collectAndGet s.find?) |>.run privateEnv |>.run {} + -- `seen` contains exactly the walked constants; skip walked imported constants missing from + -- the export table, which `find?` could never answer from `localEntries`. let newEntries := st.seen.foldl (init := #[]) fun acc c axs => - if (env.getModuleIdxFor? c).isNone && !s.localEntries.contains c then + if (env.getModuleIdxFor? c).isNone then acc.push (c, axs) else acc