Naso (Aug 26 2023 at 04:56): Naso (Aug 26 2023 at 04:56):I'm getting timing out proofs of False in an empty Scratch.thy file with RC3 from vampire. Is this expected behaviour? I can't reproduce in 2022.
Mathias Fleury (Aug 27 2023 at 12:05):This indicates that vampire has a bug
Mathias Fleury (Aug 27 2023 at 12:06):@Martin Desharnais I don't remember, was there a vampire update between Isabelle2022 and Isabelle2023-RC3?
Mathias Fleury (Aug 27 2023 at 12:07):As we do not follow vampire releases regularly, it might a bug in an old version
Mathias Fleury (Aug 27 2023 at 12:08):As a work around, you can remove vampire from the list of provers
Mathias Fleury (Aug 29 2023 at 09:07):Not sure if relevant but Makarius mentions a "Last-minute improvement of Sledgehammer for vampire.", so maybe that :shrug:
Naso (Aug 31 2023 at 10:39):Mathias Fleury said:
Not sure if relevant but Makarius mentions a "Last-minute improvement of Sledgehammer for vampire.", so maybe that :shrug:
Yes, I started using RC4 and the problem has not recurred :)
Last updated: Dec 21 2024 at 16:20 UTC