[isabelle-dev] Proven support for Linux ARM64

[Haniel Barbosa]

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/