Zulip Chat Archive

Stream: new members

Topic: Disable timeout


view this post on Zulip Markus Himmel (Jul 14 2020 at 09:11):

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.

view this post on Zulip Johan Commelin (Jul 14 2020 at 09:12):

@Mario Carneiro @Gabriel Ebner ??

view this post on Zulip Mario Carneiro (Jul 14 2020 at 09:12):

You could set it to something absurd

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jul 14 2020 at 09:14):

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

view this post on Zulip 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

view this post on Zulip Notification Bot (Jul 14 2020 at 09:21):

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


Last updated: May 10 2021 at 00:31 UTC