Email Gateway (Aug 22 2022 at 13:25): Email Gateway (Aug 22 2022 at 13:25):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Hi,
I have a problem with sledgehammer in Isabelle 2016 with a recent vampire:
./vampire --version
Vampire 4.0 (commit 910b0ff on 2016-04-14 14:40:26 +0200)
I added the vampire binary to Isabelle by setting these environment
variables, as documented in sledgehammer.pdf:
export VAMPIRE_HOME=$HOME/local/bin
export VAMPIRE_VERSION=4.0
Very often (I guess in >50% of the cases), vampire fails like this:
Sledgehammering...
"e": Try this: using Cons.prems(2) by auto (20 ms).
"spass": Try this: using Cons.prems(2) by auto (4 ms).
"vampire": A prover error occurred. (Pass the "verbose" option for
details.)
When I look at the output of vampire, it says:
User error: Vampire only supports a single conjecuture in a problem
And it's true, the vampire input file generated by sledgehammer
sometimes ends with more than one conjecture, for example:
% Conjectures (2)
tff(conj_0, conjecture,
($false)).
tff(conj_1, conjecture,
((?[N4 : nat]: (pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat,
N4), aa_list_a_nat(size_size_list_a, cons_a(x, xsa)))) &
(pp(aa_nat_bool(aa_nat_fun_nat_bool(ord_less_nat, N4),
aa_list_a_nat(size_size_list_a, ysa))) & (~
aa_nat_a(aa_list_a_fun_nat_a(nth_a, cons_a(x, xsa)), N4) =
aa_nat_a(aa_list_a_fun_nat_a(nth_a, ysa), N4))))))).
I attached a minimal theory file that shows the problem.
Is this a known problem? Is there anything I can do?
Thanks,
Christoph
Foo.thy
Email Gateway (Aug 22 2022 at 13:25):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Dear Christoph,
Thank you for your report. This wasn't a known problem; I guess most of us are using an older Vampire.
This will be fixed in the next Isabelle release. If you want to repair your Isabelle locally, change line 535 of
src/HOL/Tools/ATP/atp_systems.ML
from
prem_role = Conjecture,
to
prem_role = Hypothesis,
and rebuild the HOL image:
./bin/isabelle build -b HOL
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 13:25):From: Christoph Dittmann <f-isabellelist@yozora.eu>
Dear Jasmin,
Thanks, this seems to fix it.
Christoph
Email Gateway (Aug 22 2022 at 17:54):From: Lawrence Paulson <lp15@cam.ac.uk>
I’m getting this problem too. Only it’s two years later and your fix is already in the sources. Could something else be going on?
Larry
Email Gateway (Aug 22 2022 at 17:55):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Larry,
I need a more detailed bug report. Notably, which platform? And do you really get the output
User error: Vampire only supports a single conjecuture in a problem
like Christoph did in 2016? I doubt so; hence your issue has likely nothing to do with his.
Jasmin
Last updated: Nov 21 2024 at 12:39 UTC