feat: omega uses Lean.HashMap instead of Std.Data.HashMap (#588)

* remove Std.HashMap from omega dependencies

* fix import

* chore: retain history of omega benchmarks

* #588

Std/Tactic/Omega/Coeffs/IntList.lean

@@ -1,4 +1,5 @@
 import Std.Tactic.Omega.IntList
+import Std.Data.List.Basic
 
 /-!
 # `Coeffs` as a wrapper for `IntList`
@@ -59,6 +60,11 @@ abbrev length (xs : Coeffs) := List.length xs
 abbrev leading (xs : Coeffs) : Int := IntList.leading xs
 /-- Shim for `List.map`. -/
 abbrev map (f : Int → Int) (xs : Coeffs) : Coeffs := List.map f xs
+/-- Shim for `.enum.find?`. -/
+abbrev findIdx? (f : Int → Bool) (xs : Coeffs) : Option Nat :=
+  List.findIdx? f xs
+  -- We could avoid `Std.Data.List.Basic` by using the less efficient:
+  -- xs.enum.find? (f ·.2) |>.map (·.1)
 /-- Shim for `IntList.bmod`. -/
 abbrev bmod (x : Coeffs) (m : Nat) : Coeffs := IntList.bmod x m
 /-- Shim for `IntList.bmod_dot_sub_dot_bmod`. -/

Std/Tactic/Omega/Core.lean

@@ -6,9 +6,8 @@ Authors: Scott Morrison
 import Std.Tactic.Omega.OmegaM
 import Std.Tactic.Omega.Constraint
 import Std.Tactic.Omega.MinNatAbs
-import Std.Data.HashMap.Basic
 
-open Lean (HashSet)
+open Lean (HashMap HashSet)
 
 namespace Std.Tactic.Omega
 

test/omega/benchmark.lean

@@ -14,6 +14,12 @@ with one test removed (in which a test-for-failure succeeds with today's `omega`
 The benchmark consists of `lake build && hyperfine "lake env lean test/omega/benchmark.lean"`
 run on a freshly rebooted machine!
 
+2024-02-06 feat: omega uses Lean.HashMap instead of Std.Data.HashMap (#588)
+kim@carica std4 % lake build && hyperfine "lake env lean test/omega/benchmark.lean"
+Benchmark 1: lake env lean test/omega/benchmark.lean
+  Time (mean ± σ):      2.530 s ±  0.008 s    [User: 2.249 s, System: 0.276 s]
+  Range (min … max):    2.513 s …  2.542 s    10 runs
+
 2024-02-03 feat: omega handles min, max, if (#575)
 kim@carica std4 % lake build && hyperfine "lake env lean test/omega/benchmark.lean"
 Benchmark 1: lake env lean test/omega/benchmark.lean