Architecture problem

[Manuel Eberl]

Just a random idea I just had: Apple might be discontinuing Rosetta, but 
the fact that Rosetta exists in the first place shows that emulation of 
x86_64 with ARM (and presumably also any other architecture with any 
other architecture) can be done in a way that's not ridiculously slow.

That ought to mean that one should be able to build a standalone tool 
that does this as well, or take an existing executable and "wrap" it 
with a kind of x86_64 interpreter that itself runs on ARM.

Obviously I'm not suggesting any of us build such a tool, but I would 
imagine somebody will, or perhaps already has. Then we could, as a last 
resort if nothing else works, use that to e.g. provide an ARM version of 
Z3 (or a version for whatever architecture of whatever software will 
give us trouble in the future). It's probably going to be slower than a 
native version, but even if it's slower by a factor of 2 or 3 it might 
not be a show stopper, especially if there aren't that many uses of Z3.

Cheers,

Manuel


On 22/10/2025 09:00, Jasmin Blanchette wrote:
> 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/57dbc570/attachment-0001.htm>