From be197cd43196c97b52083cc0250a9e73ae901683 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 9 Jul 2024 16:14:39 +0200 Subject: [PATCH] fix: prefer original module in const2ModIdx (#4652) When a definition is redeclared, the original code would clobber the value of `const2ModIdx` every time, meaning that a constant would be attributed to a module which occurs later than the modules for constants referencing this one. Preferring the original module ensures that these module indexes are dependency-ordered. This originally came up as a bug in `shake`, which assumes this property, see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/check.20for.20unused.20imports.20doesn't.20stop/near/449139309). --- src/Lean/Environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 22be24fff5..4055bc296f 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -868,9 +868,9 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) ( -- Recall that the map has not been modified when `cinfoPrev? = some _`. unless equivInfo cinfoPrev cinfo do throwAlreadyImported s const2ModIdx modIdx cname - const2ModIdx := const2ModIdx.insert cname modIdx + const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1 for cname in mod.extraConstNames do - const2ModIdx := const2ModIdx.insert cname modIdx + const2ModIdx := const2ModIdx.insertIfNew cname modIdx |>.1 let constants : ConstMap := SMap.fromHashMap constantMap false let exts ← mkInitialExtensionStates let mut env : Environment := {