<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p><br>
</p>
<div class="moz-cite-prefix">On 28/10/2024 09:39, Jasmin Blanchette
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:16ED96B2-8786-4CD7-8F8E-8F33E72C7A6B@ifi.lmu.de">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
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>
</blockquote>
<p>Doesn't sledgehammer have an API?<br>
</p>
<p>--</p>
<p> Peter<br>
</p>
<p><br>
</p>
<blockquote type="cite"
cite="mid:16ED96B2-8786-4CD7-8F8E-8F33E72C7A6B@ifi.lmu.de">
<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:
<a class="moz-txt-link-freetext" href="https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html">https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html</a><br>
<br>
</div>
</div>
</div>
</div>
</div>
</div>
<div><br>
<blockquote type="cite">
<div>On 26. Oct 2024, at 22:03, Makarius
<a class="moz-txt-link-rfc2396E" href="mailto:makarius@sketis.net"><makarius@sketis.net></a> 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>
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a><br>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a><br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
<br>
<fieldset class="moz-mime-attachment-header"></fieldset>
<pre class="moz-quote-pre" wrap="">_______________________________________________
isabelle-dev mailing list
<a class="moz-txt-link-abbreviated" href="mailto:isabelle-dev@in.tum.de">isabelle-dev@in.tum.de</a>
<a class="moz-txt-link-freetext" href="https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev">https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev</a>
</pre>
</blockquote>
</body>
</html>