[isabelle-dev] Proven support for Linux ARM64

[Makarius]

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: 
https://isabelle-dev.sketis.net/rISABELLEf8fb4384180e

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 
https://github.com/cvc5/cvc5/releases/tag/cvc5-1.1.1

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.


	Makarius