Zulip Chat Archive

Is there a set_option that disables the (deterministic) timeout message completely and just lets tactics run as long as they want? I tried set_option timeout 0 but that doesn't seem to do the trick.

Johan Commelin (Jul 14 2020 at 09:12):

@Mario Carneiro @Gabriel Ebner ??

Mario Carneiro (Jul 14 2020 at 09:12):

You could set it to something absurd

Markus Himmel (Jul 14 2020 at 09:13):

Mario Carneiro said:

You could set it to something absurd

Actually, I always get the (deterministic) timeout message in the same place, regardless of whether I set set_option timeout 100000000 or set_option timeout 1

Mario Carneiro (Jul 14 2020 at 09:14):

from reading the code it appears that set_option timeout 0 should indeed act as unbounded

Markus Himmel (Jul 14 2020 at 09:15):

That's interesting. The following times out for me:

set_option timeout 0

meta def stupid_tac : tactic unit :=
tactic.trace "Hi" >> stupid_tac

example : true :=
by stupid_tac

Notification Bot (Jul 14 2020 at 09:21):

This topic was moved by Mario Carneiro to #general > Disable timeout

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib