[isabelle-dev] Proven support for Linux ARM64

[Makarius]

On 15/02/2024 14:50, Jasmin Blanchette wrote:
> 
> Concerning cvc5: I tried downloading and running cvc5 1.1.1 for arm64 from
> 
> https://github.com/cvc5/cvc5/releases/ <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):

> /tmp/isabelle-jasminblanchette/bash_script1894380443147744112: line 1: 30873 
> Abort trap: 6           
> 
> 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.

Now I've found the problem report, that I was looking for, but too late: The 
cvc5 distribution of Isabelle/f8fb4384180e has the same problem (it uses the 
"static" versions).

I've also updated all bash_process executables already in a861b0df74b4, now 
with native arm64-darwin. This does not help here.


	Makarius