Gergely Buday (Jun 13 2024 at 13:59): Gergely Buday (Jun 13 2024 at 13:59):Sometimes, at a hard to prove lemma I get a hint:
vampire: Try this: by metis (> 1.0 s, timed out)
but when I try by metis, the system loops and by metis keeps to be purple.
Is there a general advice how can I write a proper proof for the statement?
What is being over 1 seconds? How can I make Sledgehammer try longer? sledgehammer [timeou= ...] is something different I fear.
Gergely Buday (Jun 13 2024 at 14:06):Self-answer: I guess the
sledgehammer [preplay_timeout = 5]
sets the metis timeout.
Hanna Lachnitt (Jul 25 2024 at 18:16):Okay so this is my knowledge on this topic, please someone correct me if I am wrong.
Isabelle does not trust external solvers (such as vampire) when they claim they have found a proof. This would compromise its high level of assurance (where everything is build up from a small kernel of inference rules) since external solvers might have bugs in them.
On top of that there could be a problem with the translation to the problem given to the external solver. Usually that would only go in the direction of making an unsat problem sat because the problem is overapproximated (e.g., by not including the definition of an operator and therefore abstracting it).
Therefore, Isabelle tries to find a proof on its own (here with metis). It still learns some information from the external solver (such as what facts were needed, and as an optimization for some solvers even an unsat core). For some SMT solvers the solver can also return a proof certificate that then is easier to replay. But maybe its internal method is not strong enough to find the proof or (more unlikely) the solver made a mistake/did got the wrong input.
I don't think the sledgehammer option you show has anything to do with the general metis timeout since metis is a tactic on its own. There is probably an option for metis doing that. However, in my experience this is not an issue of metis not having enough time usually. Instead I would split the goal up further to make it easier for the automation.
Mathias Fleury (Jul 26 2024 at 15:02):One example of translation issue are lets: the generated problems do not contain lets. So the external might be able to solve the problem but not metis (who has the lets). In that particular example the solution is easy (add Let_def / unfold them), but in general it is not really worth investigating
Mathias Fleury (Jul 26 2024 at 15:05):IIRC the preplay_timeoutis controlling the amount of time sledgehammer tries the tactic before marking it as timeout. So a side effect is that it sets the "metis" timeout (but also the timeout from all other tactics)
Mathias Fleury (Jul 26 2024 at 15:05):There is limited reward in increasing the timeout too much, because (usually) you do not want to insert tactics that take too long anyway
Mathias Fleury (Jul 26 2024 at 15:06):(in my experience, there is a factor ~2 between the real time and the time given by sledgehammer)
Mathias Fleury (Jul 26 2024 at 15:22):And to add to Hanna answer, if metis is called on a small goal and few theorems, then it will either be fast or fail (usually by timeout)
Mathias Fleury (Jul 26 2024 at 15:23):Remark that a timeout can also mean that vampire did something incorrect
Mathias Fleury (Jul 26 2024 at 15:30):Hanna Lachnitt said:
general metis timeout since metis is a tactic on its own. There is probably an option for metis doing that
A timeout for tactics is too dangerous (only smt had it and this has been disabled by setting it in infinity), mostly because isabelle build launches many many threads, starting the timeout, but they are all waiting and would fail with a timeout, especially on weak hardware (let's say a raspberry pi + isabelle build)
Mathias Fleury (Jul 26 2024 at 15:35):Activating the "isar proof" option (by ticking the box) might solve the problem
Last updated: Dec 21 2024 at 16:20 UTC