<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>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.</p>
<p>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.</p>
<p>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.</p>
<p>Cheers,</p>
<p>Manuel</p>
<p><br>
</p>
<div class="moz-cite-prefix">On 22/10/2025 09:00, Jasmin Blanchette
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:4B4EAA32-567F-4742-974A-895DFC9626C9@ifi.lmu.de">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
Hi all,
<div><br>
</div>
<div>Tobias wrote:</div>
<div><br>
</div>
<div>
<blockquote type="cite">Do any other ITPs use the latest z3?</blockquote>
<br>
</div>
<div>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.</div>
<div><br>
</div>
<div>
<blockquote type="cite">Cvc5 is a major asset, we need it!<br>
</blockquote>
</div>
<div><br>
</div>
<div>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).</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>Now, I just tried this example with Isabelle/a356fd7ca1c4:</div>
<div><br>
</div>
<div>
<div><span class="Apple-tab-span" style="white-space:pre"> </span>lemma
"a = b ⟹ f a = f b"</div>
<div><span class="Apple-tab-span" style="white-space:pre"> </span>
using [[smt_trace]]</div>
<div><span class="Apple-tab-span" style="white-space:pre"> </span>
by (smt (cvc5))</div>
</div>
<div><br>
</div>
<div>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".</div>
<div><br>
</div>
<div>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)?</div>
<div><br>
</div>
<div>Best,</div>
<div>Jasmin</div>
<div><br>
<div>
<meta charset="UTF-8">
<div dir="auto"
style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div dir="auto"
style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0); letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div dir="auto"
style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div dir="auto"
style="text-align: start; text-indent: 0px; overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">
<div>--<br>
Prof. Dr. Jasmin Blanchette<br>
Chair of Theoretical Computer Science and Theorem
Proving<br>
Ludwig-Maximilians-Universität München<br>
Oettingenstr. 67, 80538 München, Germany<br>
Tel.: +49 (0)89 2180 9341<br>
Web:
<a class="moz-txt-link-freetext" href="https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html">https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html</a><br>
<br>
</div>
</div>
</div>
</div>
</div>
</div>
<div><br>
<blockquote type="cite">
<div>On 22. Oct 2025, at 03:10, Tobias Nipkow
<a class="moz-txt-link-rfc2396E" href="mailto:nipkow@in.tum.de"><nipkow@in.tum.de></a> wrote:</div>
<br class="Apple-interchange-newline">
<div>
<div><br>
<br>
On 22/10/2025 03:44, Jasmin Blanchette wrote:<br>
<blockquote type="cite">Hi Makarius,<br>
<blockquote type="cite">In particular, the z3
situation is very bad: Could we update that
eventually, or discontinue it altogether?<br>
</blockquote>
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.<br>
</blockquote>
<br>
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?<br>
<br>
<blockquote type="cite">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?<br>
</blockquote>
<br>
I guess we haver to bite the bullet.<br>
<br>
<blockquote type="cite">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?<br>
</blockquote>
<br>
Cvc5 is a major asset, we need it!<br>
<br>
Tobias<br>
<br>
<blockquote type="cite">Best,<br>
Jasmin<br>
--<br>
Prof. Dr. Jasmin Blanchette<br>
Chair of Theoretical Computer Science and Theorem
Proving<br>
Ludwig-Maximilians-Universität München<br>
Oettingenstr. 67, 80538 München, Germany<br>
Tel.: +49 (0)89 2180 9341<br>
Web:
<a class="moz-txt-link-freetext" href="https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html">https://www.tcs.ifi.lmu.de/mitarbeiter/jasmin-blanchette_de.html</a><br>
<blockquote type="cite">On 21. Oct 2025, at 20:38,
Makarius <a class="moz-txt-link-rfc2396E" href="mailto:makarius@sketis.net"><makarius@sketis.net></a> wrote:<br>
<br>
On 21/10/2025 20:31, Lawrence Paulson wrote:<br>
<blockquote type="cite">On 21 Oct 2025 at 19:28
+0100, Makarius <a class="moz-txt-link-rfc2396E" href="mailto:makarius@sketis.net"><makarius@sketis.net></a>,
wrote:<br>
<blockquote type="cite"><br>
That means me need to make more efforts to phase
out remaining x86_64-darwin<br>
executables, of some external tools. In
particular:<br>
<br>
- spass<br>
- vampire<br>
- verit<br>
- smbc<br>
- zipperposition<br>
- z3<br>
</blockquote>
</blockquote>
<br>
> Thanks. I surely hope that we have ARM versions
of all of those.<br>
<br>
I also hope it, but this hope is sometimes
unfounded.<br>
<br>
In recent years, I have tried hard to support
arm64-linux, but a few executables are still
missing.<br>
<br>
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.<br>
<br>
<br>
In particular, the z3 situation is very bad: Could
we update that eventually, or discontinue it
altogether?<br>
<br>
<br>
Makarius<br>
<br>
</blockquote>
</blockquote>
<br>
</div>
</div>
</blockquote>
</div>
<br>
</div>
</blockquote>
</body>
</html>