[isabelle-dev] Proven support for Linux ARM64

Jasmin Blanchette jasmin.blanchette at ifi.lmu.de
Wed Feb 14 13:09:46 CET 2024

Hi Larry,

"smt(z3" occurs seldom because z3 is the default for "smt", so often it's omitted. (I believe it used to be omitted and now it's explicit.)


Prof. Dr. Jasmin Blanchette
Chair of Theoretical Computer Science and Theorem Proving
Ludwig-Maximilians-Universität München
Oettingenstr. 67, 80538 München, Germany
Tel.: +49 (0)89 2180 9337
Email: jasmin.blanchette at ifi.lmu.de
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html

> On 14. Feb 2024, at 11:42, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Somewhat to my surprise, there seem to be 1004 occurrences of “smt(z3" in the libraries and repository (I've never allowed it personally). It is outnumbered by verit more than 3 to 1, again a surprisingly low ratio. 
> Getting rid of them all would be a tedious business. One day we might consider automated tools to crawl over old the proofs and get rid of ugly things. 
> Larry
>> On 14 Feb 2024, at 07:47, Jasmin Blanchette <jasmin.blanchette at ifi.lmu.de> wrote:
>> 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".

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240214/8fded9c7/attachment.htm>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4674 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240214/8fded9c7/attachment.bin>

More information about the isabelle-dev mailing list