[isabelle-dev] Is the distribution broken?

Lawrence Paulson lp15 at cam.ac.uk
Tue Oct 3 16:11:32 CEST 2023

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.


More information about the isabelle-dev mailing list