Architecture problem

[Jasmin Blanchette]

Hi all,

Tobias wrote:

> Do any other ITPs use the latest z3?

SMTCoq (sic) only uses veriT and CVC4. I think HOLyHammer (for HOL4 and HOL Light) uses Z3 to find proofs, but so do we. Tjark Weber's Z3 proof reconstruction code (ITP 2010) might still be alive in HOL4, but I suspect it might not work with a recent Z3.

> Cvc5 is a major asset, we need it!


To clarify, there are two uses of cvc5: for finding proofs and for reconstruction. I was talking about the latter. I see the consensus is for keeping cvc5, also in that role. Good! That will be less work for the "task force" (and more work for the developers of the "cvc5" integration to keep it somewhat up to date so we don't end up in the same situation as with Z3).

To answer Larry: I have no doubts that the cvc5 pipeline has improved. But suppose it's not developed further for 10 years, during which time Apple invents a new processor architecture. We'll face the same choice we're facing now with Z3: try to compile old cvc5 sources from 10 years ago for the new architecture or port our integration code.

Now, I just tried this example with Isabelle/a356fd7ca1c4:

	lemma "a = b ⟹ f a = f b"
	  using [[smt_trace]]
	  by (smt (cvc5))

and it doesn't work. I get the error "Error in option parsing: proof-format=alethe is experimental in this version. If you know what you are doing, you can try --proof-alethe-experimental". So it doesn't look to me as if we can use cvc5 for reconstruction quite yet, which also postpones the work of the "task force".

Could one of the multiple authors of Lachnitt et al. (ITP 2025) comment on the status of their project (hoping at least one of them is on this mailing list)?

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 22. Oct 2025, at 03:10, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> 
> 
> On 22/10/2025 03:44, Jasmin Blanchette wrote:
>> 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.
> 
> No problem from my perspective: cvc5 outperforms the current z3. And the new z3, well, it would be nice, but I see the problem. Do any other ITPs use the latest z3?
> 
>> 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?
> 
> I guess we haver to bite the bullet.
> 
>> 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?
> 
> Cvc5 is a major asset, we need it!
> 
> Tobias
> 
>> 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/20251022/d687e041/attachment.htm>