[isabelle-dev] Failure of AFP/Proof_Strategy_Language

[Jasmin Blanchette]

Hi Makarius,

Yes, my (actually: Lukas Bartl's, under my supervision) change to Sledgehammer (d3c0734059ee) is probably the issue.

Sledgehammer is an end user tool. It should be possible to change its output without breaking things. So I'm not a big fan of the "Proof_Strategy_Language" entry's existence in the AFP. But since it's there, maybe we could ask its developer to fix it?

Best,
Jasmin

--
Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 26. Oct 2024, at 22:03, Makarius <makarius at sketis.net> wrote:
> 
> In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of AFP/Proof_Strategy_Language:
> 
> Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error Proof_Strategy_Language")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 88 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 34 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 101 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 16 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 29 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> *** empty sequence. no proof found.
> *** At command "find_proof" (line 22 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")
> 
> 
> The parent Isabelle/0c9075bdff38 appears to be fine, so it is probably due to the changes in Sledgehammer in d3c0734059ee.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241028/351ba18c/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4674 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20241028/351ba18c/attachment.bin>