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 <>
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.


isabelle-dev mailing list

view this post on Zulip Email Gateway (Oct 04 2023 at 06:42):

From: Martin Desharnais <>
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] ()


sledgehammer [expect = some_preplayed, debug] ()

and send me the output?


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC