Disable timeout

Stream: general

[Markus Himmel]

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]

@Mario Carneiro @Gabriel Ebner ??

[Mario Carneiro]

You could set it to something absurd

[Markus Himmel]

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]

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

[Markus Himmel]

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

[Patrick Massot]

How did that end in the new members stream?

[Markus Himmel]

Sorry, I am sometimes unsure where to put these advanced-but-probably-trivial questions. Feel free to move the topic to a more fitting stream.

[Johan Commelin]

@Markus Himmel #general is for everything you are unsure about (-;

[Patrick Massot]

There is another rule that applies here: Markus, you are not a new member.

[Notification Bot]

This topic was moved here from #new members > Disable timeout by Mario Carneiro

[Mario Carneiro]

FWIW the test has the expected behavior when you run it from console mode (where the default timeout is infinity)

[Markus Himmel]

Can you reproduce the timeout from VS Code?

[Kenny Lau]

sometimes I post in #new members sarcastically

[Mario Carneiro]

although I think it causes a memory leak so you might also be seeing a memory abort

[Mario Carneiro]

I can

[Mario Carneiro]

Lean doesn't have tail recursion (!) so long loops are basically memory leaks

[Markus Himmel]

Okay, but can the memory leak cause the (deterministic) timeout message?

[Mario Carneiro]

It can definitely contribute to pushing the "time" along, but it shouldn't matter if the timeout is unlimited

[Mario Carneiro]

"time" is actually memory allocations

[Mario Carneiro]

On review it looks like that option is read on thread initialization time and on main() but not otherwise

[Mario Carneiro]

meaning that you are stuck with whatever timeout is set at the command line

[Mario Carneiro]

I believe you can modify the lean server invocation in vscode to include a timeout setting if you want to go that route

[Markus Himmel]

I turns out that there is a "Lean timeout" setting in the VS Code settings, and setting this to 0 indeed does the trick.

[Markus Himmel]

So can set_option timeout be fixed or should we add a remark to the docstring of the timeout option that says that it doesn't work?

[Gabriel Ebner]

This is theoretically fixable. Please file an issue if it is very important to you.