[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.


	Makarius



More information about the isabelle-dev mailing list