[isabelle-dev] Proven support for Linux ARM64

Makarius makarius at sketis.net
Thu Feb 15 10:03:48 CET 2024

On 14/02/2024 09:08, Jasmin Blanchette wrote:
>>  * nunchaku
>>  * smbc
> Nunchaku (and its backend SMBC) never left the experimental stage. Maybe we 
> could move them out of "HOL" and mark them more clearly as experimental? I 
> haven't given up all hopes of developing Nunchaku further and indeed just this 
> week I was talking with a candidate about doing this, but it shouldn't block 
> Isabelle releases.

I would say we just leave the status-quo for the Isabelle2024 release, i.e. 
these tools are implicitly "experimental" and there is no arm64-linux support.


More information about the isabelle-dev mailing list