[isabelle-dev] Proven support for Linux ARM64

Makarius makarius at sketis.net
Thu Feb 29 23:11:27 CET 2024

On 19/02/2024 12:50, Jasmin Blanchette wrote:
> 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.

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

OK, so here is the cvc5-1.1.1 component for further testing: 

I only made some basic tests with sledgehammer in 
src/HOL/Metis_Examples/Big_O.thy --- it looks fine so far on all platforms.

Note that arm64-linux is still missing from 

They claim that ARM64 is supported via cross compilation here: 
https://github.com/cvc5/cvc5/blob/main/INSTALL.rst --- but they don't provide 
binaries for download.

Maybe you can motivate the cvc5 guys to complete their set of downloads --- to 
avoid "debianization" of this otherwise great tool --- meaning bad builds that 
appear to work superficially.


More information about the isabelle-dev mailing list