Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Is the distribution broken?


view this post on Zulip 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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC