<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 all,<div><br></div><div>I've investigated further. The issue is hard to debug. It seems to arise only when minimizing proofs (where we call the solver repeatedly on often unprovable problems) and only when at least two solvers are run in parallel (i.e., when invoking Sledgehammer with "slices=2" or above).</div><div><br></div><div>I thought I might make some progress by replacing the "cvc5" binary with this script:</div><div><br></div><div><div><span class="Apple-tab-span" style="white-space:pre"> </span>#!/bin/bash</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>cp ${!#} "$(mktemp /tmp/foo.XXXXXXXXX).smt"</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>/Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5.bin $@</div></div><div><br></div><div>where "cvc5.bin" is the ARM64 Darwin cvc5 binary. But then the issue doesn't arise anymore!</div><div><br></div><div>As far as I can tell, the issue only arises with unprovable (sat) problems anyway, and it happens in such a way that it doesn't affect the workings of Sledgehammer. What's annoying is the yellow warning message in Isabelle/jEdit.</div><div><br></div><div>It looks like we can suppress the yellow message by writing a small wrapper script like the above (but using the proper idiom for retrieving the path of "cvc5.bin"). Is that what we should do? It would be great to leave CVC4 behind and to move to cvc5.</div><div><br></div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><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 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 15. Feb 2024, at 14:50, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:</div><br class="Apple-interchange-newline"><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">Hi Makarius,<div><br></div><div>Concerning cvc5: I tried downloading and running cvc5 1.1.1 for arm64 from</div><div><br></div><div><a href="https://github.com/cvc5/cvc5/releases/">https://github.com/cvc5/cvc5/releases/</a></div><div><br></div><div>and I still get errors in Isabelle. For example, adding the line</div><div><br></div><div><div> sledgehammer[cvc5, mepo, slices=4]</div></div><div><br></div><div>before line 318 of the file "$AFP/thys/Given_Clause_Loops/DISCOUNT_Loop.thy" produces this output (nondeterministically):</div><div><br></div><div><div>Sledgehammering... </div><div>cvc5 found a proof... </div><div>cvc5 found a proof... </div><div>cvc5 found a proof... </div><div>cvc5 found a proof... </div><div>/tmp/isabelle-jasminblanchette/bash_script1894380443147744112: line 1: 30873 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --decision\=internal --simplification\=none --full-saturate-quant --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 219 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904226 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904228 2>&1 </div><div>/tmp/isabelle-jasminblanchette/bash_script936180679870508119: line 1: 30876 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --trigger-sel\=max --full-saturate-quant --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 222 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904284 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904286 2>&1 </div><div>/tmp/isabelle-jasminblanchette/bash_script2386389454125518978: line 1: 30882 Abort trap: 6 /Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5 --full-saturate-quant --inst-when\=full-last-call --inst-no-entail --term-db-mode\=relevant --multi-trigger-linear --proof-format-mode\=alethe --proof-granularity\=dsl-rewrite --no-stats --sat-random-seed\=1 --lang\=smt2 --tlimit 221 /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904420 > /tmp/isabelle-jasminblanchette/process10570530194278022654/cache-io-9904422 2>&1 </div><div>cvc5: Try this: by (metis P0A_add_y_formula PYA_add_active_formula state.simps) (130 ms) </div><div>cvc5: Duplicate proof </div><div>cvc5: Duplicate proof </div><div>cvc5: Duplicate proof </div><div>Done</div></div><div><br></div><div>I don't know what the "Abort trap" warnings mean, because the prover seems to succeed nevertheless. I need to investigate. But I don't get these errors with CVC4.</div><div><br></div><div>Jasmin</div><div><br><div>
<meta charset="UTF-8"><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 9337<br>Email: jasmin.blanchette@ifi.lmu.de<br>Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html<br><br></div></div></div>
</div>
<div><br><blockquote type="cite"><div>On 6. Feb 2024, at 21:47, Makarius <makarius@sketis.net> wrote:</div><br class="Apple-interchange-newline"><div><div>With Isabelle/37e57ac55559 we now have proven support for Linux ARM64, meaning that there is a nightly "isabelle build -a" on a virtual server (from Netcup).<br><br><br>The Admin/build_release now works on Linux ARM64, and can produce logic images for Linux ARM64. Thus regular repository snapshots (and release candidates) support that platform by default, e.g. see https://isatest.sketis.net/devel/release_snapshot<br><br><br>Still missing (to be investigated further) are the following external tools:<br><br> * z3: stuck at the rather old version 4.4.0, which lacks arm64-linux binaries; the 4.4.1 arm64 package from ancient Debian is somewhat unstable on current Ubuntu 20.04, see also failure of HOL-SMT_Examples recorded on https://isatest.sketis.net/devel/build_status/index.html<br><br> * cvc4 (or rather cvc5)<br><br> * nunchaku<br><br> * smbc<br><br> * ocaml / opam<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></div>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev<br></div></blockquote></div><br></div></body></html>