[isabelle-dev] Proven support for Linux ARM64

[Jasmin Blanchette]

Hi Makarius,

I'm very satisfied with cvc5. I ran an evaluation on hundreds of goals from the AFP and the success rate went up from 52% for CVC4 to 64% for 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 16. Feb 2024, at 15:33, Makarius <makarius at sketis.net> wrote:
> 
> On 16/02/2024 15:10, Jasmin Blanchette wrote:
>> 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!
> 
> That could be some odd effect from switching between Intel and ARM on macOS, maybe caused by our bash_process wrapper (which is for Intel in Isabelle/0f01c575ff3e).
> 
> Apart from that, are you satisfied with cvc5-1.1.1? Does everything work with the current Intel setup?
> 
> If so, I will see how to change our process wrappers such that everything works again on all platforms.
> 
> 
> 	Makarius
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240219/a64359dd/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/20240219/a64359dd/attachment.bin>