Email Gateway (Aug 22 2022 at 18:09): Email Gateway (Aug 22 2022 at 18:09):From: Michal Wallace <michal.wallace@gmail.com>
Running sledgehammer on windows on a fresh copy of Isabelle2018 RC3 gives me
the following error message:
"verit": A prover error occurred:
Abnormal termination with exit code 127
Oddly, "verit" is not configured as one of the sledgehammer provers in
jedit:
cvc4 z3 spass e remote_vampire
(I think the problem first appeared in RC2, but not sure...)
Email Gateway (Aug 22 2022 at 18:09):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Wallace,
On 3. Aug 2018, at 08:46, Michal Wallace <michal.wallace@gmail.com> wrote:
Running sledgehammer on windows on a fresh copy of Isabelle2018 RC3 gives me
the following error message:
We've independently noted the problem yesterday. The decision has been to take out veriT (whose support is experimental and undocumented) from the release, and reintroduce it afterwards once we have sorted out the issues.
Oddly, "verit" is not configured as one of the sledgehammer provers in
jedit:cvc4 z3 spass e remote_vampire
If this configuration was done in the Sledgehammer panel, it affects only the Sledgehammer panel, not the "sledgehammer" command. (See also "sledgehammer_params".)
Cheers,
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC