From 666fb5c571baa93ec7edf1a7f66d622837632ccb Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Sat, 7 Jun 2025 16:27:16 -0700 Subject: [PATCH] fix: update maxHeartbeats in tests/lean/run/match_expr_perf.lean (#8676) 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. --- tests/lean/run/match_expr_perf.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/run/match_expr_perf.lean b/tests/lean/run/match_expr_perf.lean index 08c2379e66..b1a43fef53 100644 --- a/tests/lean/run/match_expr_perf.lean +++ b/tests/lean/run/match_expr_perf.lean @@ -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}"