[isabelle-dev] Is the distribution broken?

[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] ()

by

     sledgehammer [expect = some_preplayed, debug] ()

and send me the output?

Cheers,
Martin


Le 2023-10-03 à 16 h 11, Lawrence Paulson a écrit :
> 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 at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev