max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: update maxHeartbeats in tests/lean/run/match_expr_perf.lean (#8676)

Browse source 
This PR updates `maxHeartbeats` in the match_expr_perf.lean test, since
with the new compiler this also includes the allocations made by the
compiler.
This commit is contained in:
Cameron Zwarich 2025-06-07 16:27:16 -07:00 • committed by GitHub
parent 8d8fd0715f
commit 666fb5c571
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/run/match_expr_perf.lean
View file

@ -11,7 +11,7 @@ import Lean.Elab.Tactic.Config
open Lean Meta Omega
set_option maxHeartbeats 5000
set_option maxHeartbeats 6000
def pushNot (h P : Expr) : MetaM (Option Expr) := do
let P ← whnfR P
trace[omega] "pushing negation: {P}"