[isabelle-dev] Proven support for Linux ARM64

[Jasmin Blanchette]

Hi Makarius,

Concerning cvc5: I tried downloading and running cvc5 1.1.1 for arm64 from

https://github.com/cvc5/cvc5/releases/

and I still get errors in Isabelle. For example, adding the line

    sledgehammer[cvc5, mepo, slices=4]

before line 318 of the file "$AFP/thys/Given_Clause_Loops/DISCOUNT_Loop.thy" produces this output (nondeterministically):

Sledgehammering... 
cvc5 found a proof... 
cvc5 found a proof... 
cvc5 found a proof... 
cvc5 found a proof... 
/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 
/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 
/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 
cvc5: Try this: by (metis P0A_add_y_formula PYA_add_active_formula state.simps) (130 ms) 
cvc5: Duplicate proof 
cvc5: Duplicate proof 
cvc5: Duplicate proof 
Done

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.

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 9337
Email: jasmin.blanchette at ifi.lmu.de
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 6. Feb 2024, at 21:47, Makarius <makarius at sketis.net> wrote:
> 
> 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).
> 
> 
> 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
> 
> 
> Still missing (to be investigated further) are the following external tools:
> 
>  * 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
> 
>  * cvc4 (or rather cvc5)
> 
>  * nunchaku
> 
>  * smbc
> 
>  * ocaml / opam
> 
> 
> 	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/20240215/9425c414/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/20240215/9425c414/attachment.bin>