Sage Binder (Feb 28 2024 at 00:19): Sage Binder (Feb 28 2024 at 00:19):Hello,
I am aware that sledgehammer sometimes produces proofs which time out. However, I have noticed that sometimes proofs which sledgehammer indicates as timing out actually do appear terminate when they are used (I say "appears" to mean that the syntax highlighting which indicates the non-termination of a tactic goes away—is there another indication of termination besides syntax highlighting?). I am wondering if a sledgehammer proof is safe to use if it appears to terminate within the Isabelle theory, even if sledgehammer itself says that it timed out.
Thanks!
Mathias Fleury (Feb 28 2024 at 10:20):It is safe to use
Mathias Fleury (Feb 28 2024 at 10:22):The issue you are seeing boils down to Isabelle timings (on the tactic level) to vary vastly between two calls. Sledgehammer marks tactic calls as failed after a certain timeout (and Sledgehammer spawns many threads), but actually the call might go through
Last updated: Apr 27 2024 at 16:16 UTC