From 26fdc1e19afdc0e75937ed6f06166ff52e73d73a Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 21 Aug 2025 03:53:30 -0400 Subject: [PATCH] feat: `deriving BEq, Hashable` for `Lean.Import` (#10018) This PR derives `BEq` and `Hashable` for `Lean.Import`. Lake already did this later, but it now done when defining `Import`. Doing this in Lake became problematic when porting it to the module system (#9749). --- src/Lean/Setup.lean | 3 ++- src/lake/Lake/Load/Lean/Elab.lean | 2 -- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/Lean/Setup.lean b/src/Lean/Setup.lean index b5b25b5d0d..2a987ffc6e 100644 --- a/src/Lean/Setup.lean +++ b/src/Lean/Setup.lean @@ -29,7 +29,8 @@ structure Import where isExported : Bool := true /-- Whether all definitions (transitively) reachable through the -/ isMeta : Bool := false - deriving Repr, Inhabited, ToJson, FromJson + deriving Repr, Inhabited, ToJson, FromJson, + BEq, Hashable -- needed by Lake (in `Lake.Load.Elab.Lean`) instance : Coe Name Import := ⟨({module := ·})⟩ diff --git a/src/lake/Lake/Load/Lean/Elab.lean b/src/lake/Lake/Load/Lean/Elab.lean index e65fa08450..b1f275409d 100644 --- a/src/lake/Lake/Load/Lean/Elab.lean +++ b/src/lake/Lake/Load/Lean/Elab.lean @@ -21,8 +21,6 @@ open System Lean namespace Lake -deriving instance BEq, Hashable for Import - /- Cache for the imported header environment of Lake configuration files. -/ builtin_initialize importEnvCache : IO.Ref (Std.HashMap (Array Import) Environment) ← IO.mkRef {}