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

chore: increase maxHeartbeats default values

Browse source 
We now increase the number of heartbeats at `expr_eq_fn`. Thus, the
old default values are too small.
This commit is contained in:
Leonardo de Moura 2022-02-28 15:40:14 -08:00
parent b5f28239af
commit adf3510e08
5 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/CoreM.lean
View file

@ -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"
}

2
src/Lean/Meta/SynthInstance.lean
View file

@ -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"
}

2
tests/lean/1007.lean.expected.out
View file

@ -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 <num>' to set the limit)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)

2
tests/lean/906.lean.expected.out
View file

@ -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 <num>' to set the limit)
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

2
tests/lean/tcloop.lean.expected.out
View file

@ -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 <num>' to set the limit)
(deterministic) timeout at 'typeclass', maximum number of heartbeats (20000) has been reached (use 'set_option synthInstance.maxHeartbeats <num>' to set the limit)