feat: add file that shows dramatic delta in instantiateMVars timings.

Shell: 1.59s versus VSCode: 18.5s for "instantiate metavars".

tactic execution of Lean.Parser.Tactic.omega took 4.3s
instantiate metavars took 1.97s
share common exprs took 1.59s
type checking took 1.35s
process pre-definitions took 1.85s
linting took 127ms
elaboration took 690ms
cumulative profiling times:
    attribute application 0.00283ms
    elaboration 690ms
    fix level params 46.1ms
    instantiate metavars 1.97s
    linting 127ms
    parsing 2.07ms
    process pre-definitions 1.85s
    share common exprs 1.59s
    simp 18.7ms
    tactic execution 4.3s
    type checking 1.35s
    typeclass inference 299ms

tactic execution of Lean.Parser.Tactic.omega took 4.08s
instantiate metavars took 18.5s
share common exprs took 5.04s
type checking took 1.09s
process pre-definitions took 1.14s
linting took 382ms
elaboration took 3.06s

Author: bollu

tests/bench/omega/omega1-instantiate-metavars-very-slow.lean

@@ -0,0 +1,42 @@
+-- from the shell:
+--   + tactic execution of Lean.Parser.Tactic.omega took 4.3s
+--   + instantiate metavars took 1.97s
+-- from VSCode:
+--   + tactic execution of Lean.Parser.Tactic.omega took 4.08s
+--   + instantiate metavars took 18.5s
+
+set_option maxHeartbeats 0 -- runs out of heartbeats. Maybe that's an indication that the problem cannot be solved?
+set_option profiler true 
+theorem t
+(six0 s0x0 : BitVec 64)
+(h_six0_nonzero : six0 ≠ 0)
+(h_s0x1 : s0x1 + 16#64 * (s0x0 - six0) + 16#64 = s0x1 + 16#64 * (s0x0 - (six0 - 1#64)))
+(h_s0x2 : s0x2 + 16#64 * (s0x0 - six0) + 16#64 = s0x2 + 16#64 * (s0x0 - (six0 - 1#64)))
+(h_assert_1 : six0 ≤ s0x0)
+(h_assert_3 : six1 = s0x1 + 16#64 * (s0x0 - six0))
+(h_assert_4 : six2 = s0x2 + 16#64 * (s0x0 - six0))
+(n : Nat)
+(addr : BitVec 64)
+(h_le : (s0x0 - (six0 - 1#64)).toNat ≤ s0x0.toNat)
+(h_upper_bound : addr.toNat + n ≤ 2 ^ 64)
+(h_upper_bound₂ : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
+(h_upper_bound₃ : s0x2.toNat + (16#64 * (s0x0 - (six0 - 1#64))).toNat ≤ 2 ^ 64)
+(h_width_lt : (16#64).toNat * (s0x0 - (six0 - 1#64)).toNat < 2 ^ 64)
+(hmemSeparate_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
+  s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
+    (s0x1.toNat + s0x0.toNat * 16 ≤ s0x2.toNat ∨ s0x1.toNat ≥ s0x2.toNat + s0x0.toNat * 16))
+(hmemLegal_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
+(hmemLegal_omega : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
+(hmemSeparate_omega : s0x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+    2 ^ 64 ∧
+  addr.toNat + n ≤ 2 ^ 64 ∧
+    (s0x2.toNat +
+          16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
+        addr.toNat ∨
+      s0x2.toNat ≥ addr.toNat + n))
+(hmemLegal_omega : addr.toNat + n ≤ 2 ^ 64) :
+ s0x2.toNat + (16#64 * (s0x0 - six0)).toNat ≤ 2 ^ 64 ∧
+  addr.toNat + n ≤ 2 ^ 64 ∧
+    (s0x2.toNat + (16#64 * (s0x0 - six0)).toNat ≤ addr.toNat ∨ s0x2.toNat ≥ addr.toNat + n) := by
+  bv_omega
+