Email Gateway (Oct 03 2023 at 14:12): Email Gateway (Oct 03 2023 at 14:12):From: Lawrence Paulson <lp15@cam.ac.uk>
I added some material and ran the HOL distribution locally. This is what I got:
Running HOL-Metis_Examples ...
HOL-Metis_Examples FAILED (see also "isabelle build_log -H Error HOL-Metis_Examples")
*** Unexpected outcome: "none"
*** At command "sledgehammer" (line 19 of "~~/src/HOL/Metis_Examples/Sledgehammer_Isar_Proofs.thy")
Unfinished session(s): HOL-Metis_Examples
If we run this in an interactive session, it fails in the same way. This can’t be connected with the material that I added.
Larry
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Oct 04 2023 at 06:42):From: Martin Desharnais <martin.desharnais@posteo.de>
Hi Larry,
I added this Sledgehammer proof-reconstruction test in
Isabelle/a98e0a816d28 (on 20 September 2023). I cannot reproduce the
failure on my machine or the Jenkins server.
I would also be surprised if your changed broke the test, as I wrote it
to not depend on any explicit lemma. It tests a lemma about integer
arithmetic thought; could your changes have an impact on that?
Could you please add the "debug" option to the Sledgehammer call in an
interactive session? i.e., replace the line
sledgehammer [expect = some_preplayed] ()
by
sledgehammer [expect = some_preplayed, debug] ()
and send me the output?
Cheers,
Martin
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Apr 27 2024 at 12:25 UTC