[isabelle-dev] Proven support for Linux ARM64

Haniel Barbosa hbarbosa at dcc.ufmg.br
Tue Mar 19 22:52:54 CET 2024


I'm happy to report that we got this working now (thanks to Daniel



Haniel Barbosa <hbarbosa at dcc.ufmg.br> writes:

> Hello,
> FYI inspired by this thread we started to look into adding arm64 into
> our CI pipeline so we can provide this binary for users. Unclear when
> that'll materialize though.
> Best,
> Makarius <makarius at sketis.net> writes:
>> 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
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

Haniel Barbosa

More information about the isabelle-dev mailing list