[isabelle-dev] Proven support for Linux ARM64

[Haniel Barbosa]

Hello,

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

  https://github.com/cvc5/cvc5/releases/tag/latest

Best,

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
https://hanielbarbosa.com/