Last maze triggers simp heartbeat error
Opened this issue · 2 comments
Hello! I was playing around a bit after today's talk and tried to bored-ly solve the long maze just to pass some time.
I'm not sure if there's anything to fix really, but just to note, if you do:
example : can_escape maze3 :=
by west
west
west
south
south
south
south
east
east
north
north
east
east
south
south
south
south
south
south
south
south
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
west
north
north
north
north
north
north
north
north
east
east
south
south
south
south
south
south
east
east
east
east
north
north
north
north
east
east
east
north
north
east
east
east
east
east
east
the last east says cannot move east, even though clearly you can from the picture.
The issue seems to be simp failing -- if I apply step_east and then simp, the infoview says:
▶ 473:5-473:9: error:
tactic 'simp' failed, nested error:
(deterministic) timeout at 'simp', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)
and indeed set_option maxHeartbeats 999999999 fixes the issue (lets me east).
Not sure as I say that there's anything that needs tweaking, I take it changing the default globally is silly, but yeah just sharing :)
Thanks for the fun.
⊙ lean --version julian@Airm
Lean (version 4.0.0, commit cb32681978e8, Release)
FWIW
Wow, interesting. I wonder if we can make east (and the other tactics) more efficient so that we don't hit such an error.