Architecture problem

[Jasmin Blanchette]

Hi Makarius,

> In particular, the z3 situation is very bad: Could we update that eventually, or discontinue it altogether?

To summarize a discussion we had together one or two months ago: Z3 has moved on in 11 years, and it would probably be hard to support its new proofs. It's not hard enough for a research project and probably too hard for a BSc and possibly MSc (or at least very supervision-intensive). So we might consider getting rid of Z3 support.

This means: (1) Sledgehammer should stop generating Z3-based "smt" proofs; (2) we should ask the AFP authors to get rid of their Z3-smt calls (using the more stable veriT or other proofs), maybe with some help from a task force (which I could lead). Do we agree?

Also unclear in all of this is the role of cvc5. Unlike veriT, it's under active development and is a more complex piece of software (i.e., harder to build). Do we also want to avoid it?

Best,
Jasmin

--
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 9341
Web: https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html


> On 21. Oct 2025, at 20:38, Makarius <makarius at sketis.net> wrote:
> 
> On 21/10/2025 20:31, Lawrence Paulson wrote:
>> On 21 Oct 2025 at 19:28 +0100, Makarius <makarius at sketis.net>, wrote:
>>> 
>>> That means me need to make more efforts to phase out remaining x86_64-darwin
>>> executables, of some external tools. In particular:
>>> 
>>> - spass
>>> - vampire
>>> - verit
>>> - smbc
>>> - zipperposition
>>> - z3
> 
> > Thanks. I surely hope that we have ARM versions of all of those.
> 
> I also hope it, but this hope is sometimes unfounded.
> 
> In recent years, I have tried hard to support arm64-linux, but a few executables are still missing.
> 
> This year, I have continued under the assumption that x86_64-darwin will stop working soon, but did not yet manage to build all tools yet.
> 
> 
> In particular, the z3 situation is very bad: Could we update that eventually, or discontinue it altogether?
> 
> 
> 	Makarius
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251021/a64659e6/attachment-0001.htm>