From adf3510e0893775a6ce8286a1cdc1f2980dc2bc9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Feb 2022 15:40:14 -0800 Subject: [PATCH] chore: increase `maxHeartbeats` default values We now increase the number of heartbeats at `expr_eq_fn`. Thus, the old default values are too small. --- src/Lean/CoreM.lean | 2 +- src/Lean/Meta/SynthInstance.lean | 2 +- tests/lean/1007.lean.expected.out | 2 +- tests/lean/906.lean.expected.out | 2 +- tests/lean/tcloop.lean.expected.out | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 53ae7c8a49..cdfc9d4bb6 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -17,7 +17,7 @@ namespace Lean namespace Core register_builtin_option maxHeartbeats : Nat := { - defValue := 50000 + defValue := 200000 descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit" } diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index ed00034585..6181ea1a1b 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -15,7 +15,7 @@ import Lean.Util.Profile namespace Lean.Meta register_builtin_option synthInstance.maxHeartbeats : Nat := { - defValue := 500 + defValue := 20000 descr := "maximum amount of heartbeats per typeclass resolution problem. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit" } diff --git a/tests/lean/1007.lean.expected.out b/tests/lean/1007.lean.expected.out index 8878d33935..5a0afc591b 100644 --- a/tests/lean/1007.lean.expected.out +++ b/tests/lean/1007.lean.expected.out @@ -8,4 +8,4 @@ 1007.lean:40:35-40:40: warning: declaration uses 'sorry' 1007.lean:57:64-57:78: error: failed to synthesize IsLin fun x => sum fun i => norm x -(deterministic) timeout at 'typeclass', maximum number of heartbeats (500) has been reached (use 'set_option synthInstance.maxHeartbeats ' to set the limit) +(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats ' to set the limit) diff --git a/tests/lean/906.lean.expected.out b/tests/lean/906.lean.expected.out index 10ea7227c2..c475a2d51b 100644 --- a/tests/lean/906.lean.expected.out +++ b/tests/lean/906.lean.expected.out @@ -1,3 +1,3 @@ 906.lean:7:14-7:19: warning: declaration uses 'sorry' 906.lean:12:2-12:28: error: tactic 'simp' failed, nested error: -(deterministic) timeout at 'whnf', maximum number of heartbeats (50000) has been reached (use 'set_option maxHeartbeats ' to set the limit) +(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats ' to set the limit) diff --git a/tests/lean/tcloop.lean.expected.out b/tests/lean/tcloop.lean.expected.out index e7a6993653..7349958a60 100644 --- a/tests/lean/tcloop.lean.expected.out +++ b/tests/lean/tcloop.lean.expected.out @@ -1,3 +1,3 @@ tcloop.lean:14:2-14:15: error: failed to synthesize B Nat -(deterministic) timeout at 'typeclass', maximum number of heartbeats (500) has been reached (use 'set_option synthInstance.maxHeartbeats ' to set the limit) +(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats ' to set the limit)