[isabelle-dev] Proven support for Linux ARM64

[Florian Haftmann]

Hi all,

> 1. Replace the "smt" calls. Most of them could use the "(verit)" option 
> instead, and for the others, we'd have to come up with alternative 
> proofs. This possibly entails a lot of work, but it could be done by a 
> "task force".
> 
> 2. Use certificates for the AFP (and require their use in the future). 
> Certificates take the form of low-level (SMT input, SMT output) pairs, 
> so that when "smt" generates a given SMT input in the cache, the SMT 
> output is used directly instead of running the SMT solver.

just my 5 cent: the certificates are helpful, but strictly relying on 
them in distribution or AFP rules out people having no access to certain 
provers to do work requiring potentially pervasive maintenance of proofs.

Cheers,
	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0xA707172232CFA4E9.asc
Type: application/pgp-keys
Size: 19161 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240217/1500f77c/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240217/1500f77c/attachment-0001.sig>