[isabelle-dev] Proven support for Linux ARM64

Makarius makarius at sketis.net
Fri Feb 16 15:33:40 CET 2024


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



More information about the isabelle-dev mailing list