[isabelle-dev] Is the distribution broken?

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

Larry