[isabelle-dev] Proven support for Linux ARM64

Lawrence Paulson lp15 at cam.ac.uk
Wed Feb 14 11:42:29 CET 2024

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. 


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

More information about the isabelle-dev mailing list