<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>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></body></html>