<!DOCTYPE html>
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi all,</p>
<div class="moz-cite-prefix">On 10/22/25 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>
</blockquote>
<p><br>
</p>
<p>Irvin on Zulip (<a
href="https://isabelle.zulipchat.com/#narrow/channel/202961-General/topic/Making.20isabelle.20run.20on.20modern.20z3.2E/with/546366457">#General
> Making isabelle run on modern z3.</a>) tried to update it
and found how HOL4 is supporting the new version:</p>
<p><a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/8f8bd67b8c5a3d799144a14206aa8d4266edd36b"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/8f8bd67b8c5a3d799144a14206aa8d4266edd36b"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/8f8bd67b8c5a3d799144a14206aa8d4266edd36b</a><br>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/def62b7000cb313b19c84cabe8c1867e63a9c624"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/def62b7000cb313b19c84cabe8c1867e63a9c624"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/def62b7000cb313b19c84cabe8c1867e63a9c624</a>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/4324a79a32b7cccf11efbef4ecee637784ad28c4"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/4324a79a32b7cccf11efbef4ecee637784ad28c4"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/4324a79a32b7cccf11efbef4ecee637784ad28c4</a>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/313365a0e83c847c9767d67ab52b2f69135dcaba"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/313365a0e83c847c9767d67ab52b2f69135dcaba"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/313365a0e83c847c9767d67ab52b2f69135dcaba</a>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/4b763209b040de35cf9d408e76a9c4898ce848d5"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/4b763209b040de35cf9d408e76a9c4898ce848d5"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/4b763209b040de35cf9d408e76a9c4898ce848d5</a>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/120e7bb43bc3ffcca4efb2cafbeed0605d620bff"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/120e7bb43bc3ffcca4efb2cafbeed0605d620bff"
class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/120e7bb43bc3ffcca4efb2cafbeed0605d620bff</a>
<a
href="https://github.com/HOL-Theorem-Prover/HOL/commit/525694a1f1c7016dea954894bea6e6e396f7d6b3"
target="_blank" rel="noopener noreferrer"
title="https://github.com/HOL-Theorem-Prover/HOL/commit/525694a1f1c7016dea954894bea6e6e396f7d6b3"
moz-do-not-send="true" class="moz-txt-link-freetext">https://github.com/HOL-Theorem-Prover/HOL/commit/525694a1f1c7016dea954894bea6e6e396f7d6b3</a></p>
<p>So it should be possible to port this to Isabelle. However, Irvin
gave up.</p>
<p><br>
</p>
<p><br>
</p>
<p>Mathias</p>
<blockquote type="cite"
cite="mid:4B4EAA32-567F-4742-974A-895DFC9626C9@ifi.lmu.de">
<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>