Architecture problem

[Tobias Nipkow]

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 --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 4856 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251022/644ff698/attachment-0001.bin>