[isabelle-dev] Proven support for Linux ARM64

Fri Feb 16 15:10:01 CET 2024

Hi all,

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).

I thought I might make some progress by replacing the "cvc5" binary with this script:

	#!/bin/bash
	cp ${!#} "$(mktemp /tmp/foo.XXXXXXXXX).smt"
	/Users/jasminblanchette/.isabelle/contrib/cvc5-1.1.1/arm64-darwin/cvc5.bin $@

where "cvc5.bin" is the ARM64 Darwin cvc5 binary. But then the issue doesn't arise anymore!

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.

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.

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 15. Feb 2024, at 14:50, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote:
> 
> 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
> 
> _______________________________________________
> 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/20240216/f6074416/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/20240216/f6074416/attachment.bin>