Skip to content

Commit 1559cd4

Browse files
datokratdatokrat
committed
revert more tracing
1 parent ae4cae2 commit 1559cd4

3 files changed

Lines changed: 28 additions & 74 deletions

File tree

‎src/Lean/Elab/Tactic/Omega/Frontend.lean‎

Lines changed: 4 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -425,11 +425,7 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
425425
return (p, 0)
426426
else
427427
let t ← instantiateMVars (← whnfR (← inferType h))
428-
trace[omega] "adding fact: {h}({Hashable.hash h}) : {t}({Hashable.hash t}); {reprStr h}"
429-
if let .const n lvls := h then
430-
trace[omega] "h = .const {n} {lvls}"
431-
if let .const n lvls := t then
432-
trace[omega] "t = .const {n} {lvls}"
428+
trace[omega] "adding fact: {t}"
433429
match t with
434430
| .forallE _ x y _ =>
435431
if ← pure t.isArrow <&&> isProp x <&&> isProp y then
@@ -509,15 +505,13 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
509505
| _ => pure (p, 0)
510506
| _ => pure (p, 0)
511507

512-
initialize Lean.registerTraceClass `processFacts
513-
514508
/--
515509
Process all the facts in a `MetaProblem`, returning the new problem, and the number of new facts.
516510
517511
This is partial because new facts may be generated along the way.
518512
-/
519513
partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
520-
let ret ← do match p.facts with
514+
match p.facts with
521515
| [] => pure (p, 0)
522516
| h :: t =>
523517
if p.processedFacts.contains h then
@@ -528,7 +522,6 @@ partial def processFacts (p : MetaProblem) : OmegaM (MetaProblem × Nat) := do
528522
processedFacts := p.processedFacts.insert h } h
529523
let (p₂, n₂) ← p₁.processFacts
530524
return (p₂, n₁ + n₂)
531-
return ret
532525

533526
end MetaProblem
534527

@@ -616,13 +609,6 @@ where
616609
|>.map (fun ((n, a),_) => m!" {n} := {a}")
617610
|> m!"\n".joinSep
618611

619-
initialize Lean.registerTraceClass `omegaImpl
620-
621-
initialize Lean.registerTraceClass `contradictionHandling
622-
initialize Lean.registerTraceClass `splitting
623-
initialize Lean.registerTraceClass `preparation
624-
initialize Lean.registerTraceClass `proof
625-
626612
mutual
627613

628614
/--
@@ -637,6 +623,7 @@ partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
637623
trace[omega] "Case splitting on {hType}"
638624
let_expr Or hType₁ hType₂ := hType | throwError "Unexpected disjunction {hType}"
639625
let p?₁ ← withoutModifyingState do withLocalDeclD `h₁ hType₁ fun h₁ => do
626+
withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₁}") do
640627
let m₁ := { m with facts := [h₁], disjunctions := t }
641628
let (m₁, n) ← m₁.processFacts
642629
if 0 < n then
@@ -647,6 +634,7 @@ partial def splitDisjunction (m : MetaProblem) : OmegaM Expr := do
647634
return none
648635
if let some p₁ := p?₁ then
649636
withLocalDeclD `h₂ hType₂ fun h₂ => do
637+
withTraceNode `omega (msg := fun _ => do pure m!"Assuming fact:{indentExpr hType₂}") do
650638
let m₂ := { m with facts := [h₂], disjunctions := t }
651639
let p₂ ← omegaImpl m₂
652640
let p₂ ← mkLambdaFVars #[h₂] p₂

‎src/Lean/Elab/Tactic/Omega/OmegaM.lean‎

Lines changed: 14 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -89,12 +89,9 @@ def atoms : OmegaM (Array Expr) := do
8989
/-- Return the `Expr` representing the list of atoms. -/
9090
def atomsList : OmegaM Expr := do mkListLit (.const ``Int []) (← atoms).toList
9191

92-
initialize Lean.registerTraceClass `linearComboPrf
93-
9492
/-- Return the `Expr` representing the list of atoms as a `Coeffs`. -/
9593
def atomsCoeffs : OmegaM Expr := do
96-
withTraceNode `linearComboPrf (fun _ => return "atomsCoeffs") do
97-
return .app (.const ``Coeffs.ofList []) (← atomsList)
94+
return .app (.const ``Coeffs.ofList []) (← atomsList)
9895

9996
/-- Run an `OmegaM` computation, restoring the state afterwards depending on the result. -/
10097
def commitWhen (t : OmegaM (α × Bool)) : OmegaM α := do
@@ -175,7 +172,7 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
175172
match e.getAppFnArgs with
176173
| (``Nat.cast, #[.const ``Int [], _, e']) =>
177174
-- Casts of natural numbers are non-negative.
178-
let mut r := [(Expr.app (.const ``Int.ofNat_nonneg []) e')]
175+
let mut r := [Expr.app (.const ``Int.ofNat_nonneg []) e']
179176
match (← cfg).splitNatSub, e'.getAppFnArgs with
180177
| true, (``HSub.hSub, #[_, _, _, _, a, b]) =>
181178
-- `((a - b : Nat) : Int)` gives a dichotomy
@@ -197,8 +194,8 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
197194
let ne_zero := mkApp3 (.const ``Ne [1]) (.const ``Int []) k (toExpr (0 : Int))
198195
let pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
199196
(toExpr (0 : Int)) k
200-
pure [(mkApp3 (.const ``Int.mul_ediv_self_le []) x k (← mkDecideProof ne_zero)),
201-
(mkApp3 (.const ``Int.lt_mul_ediv_self_add []) x k (← mkDecideProof pos))]
197+
pure [mkApp3 (.const ``Int.mul_ediv_self_le []) x k (← mkDecideProof ne_zero),
198+
mkApp3 (.const ``Int.lt_mul_ediv_self_add []) x k (← mkDecideProof pos)]
202199
| (``HMod.hMod, #[_, _, _, _, x, k]) =>
203200
match k.getAppFnArgs with
204201
| (``HPow.hPow, #[_, _, _, _, b, exp]) => match natCast? b with
@@ -208,9 +205,9 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
208205
let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
209206
(toExpr (0 : Int)) b
210207
let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
211-
pure [(mkApp3 (.const ``Int.emod_nonneg []) x k
212-
(mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)),
213-
(mkApp3 (.const ``Int.emod_lt_of_pos []) x k pow_pos)]
208+
pure [mkApp3 (.const ``Int.emod_nonneg []) x k
209+
(mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos),
210+
mkApp3 (.const ``Int.emod_lt_of_pos []) x k pow_pos]
214211
| (``Nat.cast, #[.const ``Int [], _, k']) =>
215212
match k'.getAppFnArgs with
216213
| (``HPow.hPow, #[_, _, _, _, b, exp]) => match natCast? b with
@@ -221,20 +218,20 @@ def analyzeAtom (e : Expr) : OmegaM (List Expr) := do
221218
(toExpr (0 : Nat)) b
222219
let pow_pos := mkApp3 (.const ``Nat.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
223220
let cast_pos := mkApp2 (.const ``Int.ofNat_pos_of_pos []) k' pow_pos
224-
pure [(mkApp3 (.const ``Int.emod_nonneg []) x k
225-
(mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)),
226-
(mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos)]
221+
pure [mkApp3 (.const ``Int.emod_nonneg []) x k
222+
(mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos),
223+
mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos]
227224
| _ => match x.getAppFnArgs with
228225
| (``Nat.cast, #[.const ``Int [], _, x']) =>
229226
-- Since we push coercions inside `%`, we need to record here that
230227
-- `(x : Int) % (y : Int)` is non-negative.
231-
pure [(mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)]
228+
pure [mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k]
232229
| _ => pure ∅
233230
| _ => pure ∅
234231
| (``Min.min, #[_, _, x, y]) =>
235-
pure [(mkApp2 (.const ``Int.min_le_left []) x y), (mkApp2 (.const ``Int.min_le_right []) x y)]
232+
pure [mkApp2 (.const ``Int.min_le_left []) x y, mkApp2 (.const ``Int.min_le_right []) x y]
236233
| (``Max.max, #[_, _, x, y]) =>
237-
pure [(mkApp2 (.const ``Int.le_max_left []) x y), (mkApp2 (.const ``Int.le_max_right []) x y)]
234+
pure [mkApp2 (.const ``Int.le_max_left []) x y, mkApp2 (.const ``Int.le_max_right []) x y]
238235
| (``ite, #[α, i, dec, t, e]) =>
239236
if α == (.const ``Int []) then
240237
pure [mkApp5 (.const ``ite_disjunction [0]) α i dec t e]
@@ -258,7 +255,7 @@ def lookup (e : Expr) : OmegaM (Nat × Option (List Expr)) := do
258255
match c.atoms[e]? with
259256
| some i => return (i, none)
260257
| none =>
261-
trace[omega] "New atom: {e} with hash {Hashable.hash e}"
258+
trace[omega] "New atom: {e}"
262259
let facts ← analyzeAtom e
263260
if ← isTracingEnabledFor `omega then
264261
unless facts.isEmpty do

‎tests/bench/big_omega.lean‎

Lines changed: 10 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -1,47 +1,16 @@
1-
import Lean
2-
3-
open Lean Elab Tactic
4-
5-
-- Without any of these: fast
6-
run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- still fast
7-
run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- still fast
8-
run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- slow
9-
-- run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- fast again
10-
-- run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- still fast
11-
-- run_meta do logInfo m!"indicator fvar ID: {(← Lean.mkFreshFVarId).name}" -- slow again
12-
13-
-- #check Lean.Elab.Tactic.getFVarId
14-
-- elab "showFVarId" id:ident : tactic => do
15-
-- -- Resolve the identifier `id` to its FVarId
16-
-- let fvarId ← getFVarId id
17-
18-
-- -- FVarId has a `.name` field which is its unique internal name.
19-
-- -- We can log it to the infoview.
20-
-- logInfo m!"The identifier '{id}' corresponds to the FVarId: {fvarId.name}"
21-
22-
-- set_option trace.profiler true
23-
-- set_option trace.omegaImpl true
24-
-- set_option trace.contradictionHandling true
25-
-- set_option trace.splitting true
26-
-- set_option trace.preparation true
27-
-- set_option trace.proof true
28-
-- set_option trace.proveFalse true
29-
-- set_option trace.proveAssumption true
30-
-- set_option trace.linearComboPrf true
31-
32-
-- set_option trace.Meta.instantiateMVars true
33-
--set_option trace.Meta.isDefEq true
34-
-- set_option trace.Meta.synthInstance true
35-
36-
--set_option trace.omega true
1+
/-!
2+
This benchmark exercises `omega` in a way that creates a big proof, exercising `instantiateMVars`
3+
and `shareCommonPreDefs` as well. In particular, running it with `internal.cmdlineSnapshots=false`,
4+
like the language server does, uncovered a significant slowdown in `instantiateMVars` (#5614).
5+
-/
376

387
set_option maxHeartbeats 0
398
theorem memcpy_extracted_2 (six0 s0x0 : BitVec 64)
409
(h_six0_nonzero : six0 ≠ 0)
4110
(h_s0x1 : s0x1 + 16#64 * (s0x0 - six0) + 16#64 = s0x1 + 16#64 * (s0x0 - (six0 - 1#64)))
4211
(h_s0x2 : s0x2 + 16#64 * (s0x0 - six0) + 16#64 = s0x2 + 16#64 * (s0x0 - (six0 - 1#64)))
4312
(h_assert_1 : six0 ≤ s0x0)
44-
(_h_assert_3 : six1 = s0x1 + 16#64 * (s0x0 - six0))
13+
(h_assert_3 : six1 = s0x1 + 16#64 * (s0x0 - six0))
4514
(h_assert_4 : six2 = s0x2 + 16#64 * (s0x0 - six0))
4615
(n : Nat)
4716
(addr : BitVec 64)
@@ -50,12 +19,12 @@ theorem memcpy_extracted_2 (six0 s0x0 : BitVec 64)
5019
(h_upper_bound₂ : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
5120
(h_upper_bound₃ : s0x2.toNat + (16#64 * (s0x0 - (six0 - 1#64))).toNat ≤ 2 ^ 64)
5221
(h_width_lt : (16#64).toNat * (s0x0 - (six0 - 1#64)).toNat < 2 ^ 64)
53-
(_hmemSeparate_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
22+
(hmemSeparate_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
5423
s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64 ∧
5524
(s0x1.toNat + s0x0.toNat * 16 ≤ s0x2.toNat ∨ s0x1.toNat ≥ s0x2.toNat + s0x0.toNat * 16))
56-
(_hmemLegal_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
57-
(_hmemLegal_omega : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
58-
(_hmemSeparate_omega : s0x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
25+
(hmemLegal_omega : s0x1.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
26+
(hmemLegal_omega : s0x2.toNat + s0x0.toNat * 16 ≤ 2 ^ 64)
27+
(hmemSeparate_omega : s0x2.toNat + 16 % 2 ^ 64 * ((2 ^ 64 - (2 ^ 64 - 1 % 2 ^ 64 + six0.toNat) % 2 ^ 64 + s0x0.toNat) % 2 ^ 64) % 2 ^ 64 ≤
5928
2 ^ 64 ∧
6029
addr.toNat + n ≤ 2 ^ 64 ∧
6130
(s0x2.toNat +

0 commit comments

Comments
 (0)