<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Makarius,<div><br></div><div>Yes, my (actually: Lukas Bartl's, under my supervision) change to Sledgehammer (d3c0734059ee) is probably the issue.</div><div><br></div><div>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?</div><div><br></div><div>Best,</div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div>--<br>Prof. Dr. Jasmin Blanchette<br>Chair of Theoretical Computer Science and Theorem Proving<br>Ludwig-Maximilians-Universität München<br>Oettingenstr. 67, 80538 München, Germany<br>Tel.: +49 (0)89 2180 9341<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 26. Oct 2024, at 22:03, Makarius <makarius@sketis.net> wrote:</div><br class="Apple-interchange-newline"><div><div>In Isabelle/d3c0734059ee + AFP/4082096ade5a we have a failure of AFP/Proof_Strategy_Language:<br><br>Proof_Strategy_Language FAILED (see also "isabelle build_log -H Error Proof_Strategy_Language")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 88 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 34 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 101 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 16 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 29 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br>*** empty sequence. no proof found.<br>*** At command "find_proof" (line 22 of "~~/dirs/AFP/thys/Proof_Strategy_Language/Example.thy")<br><br><br>The parent Isabelle/0c9075bdff38 appears to be fine, so it is probably due to the changes in Sledgehammer in d3c0734059ee.<br><br><br><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></div></div></blockquote></div><br></div></body></html>