Architecture problem · Mirror: Isabelle Development Mailing List

Stream: Mirror: Isabelle Development Mailing List

Topic: Architecture problem

Email Gateway (Oct 21 2025 at 17:57):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
On my M2 MacBook Pro, I’m getting

I/O error: /Users/lp15/.isabelle/contrib/polyml-5.9.2/x86_64_32-darwin/poly (No such file or directory)

And of course the x86 version isn’t the one I should be needing anyway.

f08c8e96a2b4

Larry

Email Gateway (Oct 21 2025 at 18:06):

From: Makarius <makarius@sketis.net>
On 21/10/2025 19:57, Lawrence Paulson via isabelle-dev wrote:

On my M2 MacBook Pro, I’m getting

I/O error: /Users/lp15/.isabelle/contrib/polyml-5.9.2/x86_64_32-darwin/poly
(No such file or directory)

And of course the x86 version isn’t the one I should be needing anyway.

f08c8e96a2b4

I've actually forgotten to build the Intel/macOS platform: for Poly/ML we need
to do this on an actual Intel Mac, while e.g. for VSCodium this is a hybrid
build works on ARM64 for both platforms.

What is still odd: Why does your local setup demand x86_64_32-darwin/poly? It
could be something in etc/preferences: ML_platform.

On my usual ARM64 test machines, it works fine.

And yes: We might rightly ask when the Intel Mac platform is to be
discontinued. Maybe in 2 years.

Makarius

Email Gateway (Oct 21 2025 at 18:07):

From: Makarius <makarius@sketis.net>
On 21/10/2025 20:05, Makarius wrote:

What is still odd: Why does your local setup demand x86_64_32-darwin/poly? It
could be something in etc/preferences: ML_platform.

This is how to query the local setup:

isabelle getenv ML_PLATFORM
isabelle options -g ML_platform

The default for both is empty: it means to use the standard platform, i.e.
arm64_32-darwin.

Makarius

Email Gateway (Oct 21 2025 at 18:23):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Indeed, that was it. But why did it work before?

Larry
On 21 Oct 2025 at 19:05 +0100, Makarius <makarius@sketis.net>, wrote:

What is still odd: Why does your local setup demand x86_64_32-darwin/poly? It
could be something in etc/preferences: ML_platform.

Email Gateway (Oct 21 2025 at 18:29):

From: Makarius <makarius@sketis.net>

On 21 Oct 2025 at 19:05 +0100, Makarius <makarius@sketis.net>, wrote:

What is still odd: Why does your local setup demand x86_64_32-darwin/poly? It
could be something in etc/preferences: ML_platform.

On 21/10/2025 20:11, Lawrence Paulson wrote:

Indeed, that was it. But why did it work before?

Because your settings to demand x86_64_32-darwin/poly could be resolved
properly: You merely had a slightly slower Poly/ML, without taking notice.

Of course, I will update the polyml component to provide the missing Intel
platforms.

And yes, we do need to discontinue Intel macOS in approx. 2-3 years, when
Apple is going to ship macOS 28 without Rosetta 2. E.g. see
https://arstechnica.com/gadgets/2025/06/apple-details-the-end-of-intel-mac-support-and-a-phaseout-for-rosetta-2

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

Makarius

Email Gateway (Oct 21 2025 at 18:31):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Thanks. I surely hope that we have ARM versions of all of those.

Larry
On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 21 2025 at 18:39):

From: Makarius <makarius@sketis.net>
On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 21 2025 at 18:45):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
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.

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?

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?

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@sketis.net> wrote:

On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 21 2025 at 18:47):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Did you see the ITP paper "Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL”? It was for cvc5.

Larry
On 21 Oct 2025 at 19:38 +0100, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>, wrote:

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?

Email Gateway (Oct 21 2025 at 18:49):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Strangely, fixing this (leaving ML_PLATFORM unset) had no effect on build times.

Larry
On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@sketis.net>, wrote:

Because your settings to demand x86_64_32-darwin/poly could be resolved
properly: You merely had a slightly slower Poly/ML, without taking notice.

Email Gateway (Oct 21 2025 at 18:58):

From: Makarius <makarius@sketis.net>
On 21/10/2025 20:44, Jasmin Blanchette wrote:

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?

From my side, cvc5 is OK: we merely download the executables for all
platform. See also https://github.com/cvc5/cvc5/releases

Makarius

Email Gateway (Oct 21 2025 at 20:44):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Surely this paper addresses the issues with cvc5, and it’s supposed to be included in the next release.

https://drops.dagstuhl.de/storage/00lipics/lipics-vol352-itp2025/LIPIcs.ITP.2025.26/LIPIcs.ITP.2025.26.pdf

Larry
On 21 Oct 2025 at 20:44 +0100, wrote:

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?

Email Gateway (Oct 22 2025 at 01:10):

From: Tobias Nipkow <nipkow@in.tum.de>

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@sketis.net> wrote:

On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

smime.p7s

Email Gateway (Oct 22 2025 at 07:01):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
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

On 22. Oct 2025, at 03:10, Tobias Nipkow <nipkow@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@sketis.net> wrote:

On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 22 2025 at 07:07):

From: Manuel Eberl <manuel@pruvisto.org>
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@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@sketis.net> wrote:

On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 22 2025 at 10:32):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
I'm pretty sure Hanna said that this would be in the next release. Hanna, can you offer any more details?

Larry

On 22 Oct 2025, at 08:00, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:

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)?

Email Gateway (Oct 22 2025 at 10:35):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
They appeared to be nearly 1300 occurrences of “smt (z3" in over 300 different files. Ideally the change would be automated. One would like to think that one of the other solvers would be good enough to serve as a drop-in replacement for 15 year-old code, but maybe not.

Larry

On 21 Oct 2025, at 19:44, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de> wrote:

So we might consider getting rid of Z3 support.

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?

Email Gateway (Oct 22 2025 at 12:48):

From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,

On 10/22/25 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.

Irvin on Zulip (#General > Making isabelle run on modern z3.
<https://isabelle.zulipchat.com/#narrow/channel/202961-General/topic/Making.20isabelle.20run.20on.20modern.20z3.2E/with/546366457>)
tried to update it and found how HOL4 is supporting the new version:

https://github.com/HOL-Theorem-Prover/HOL/commit/8f8bd67b8c5a3d799144a14206aa8d4266edd36b
https://github.com/HOL-Theorem-Prover/HOL/commit/def62b7000cb313b19c84cabe8c1867e63a9c624
https://github.com/HOL-Theorem-Prover/HOL/commit/4324a79a32b7cccf11efbef4ecee637784ad28c4
https://github.com/HOL-Theorem-Prover/HOL/commit/313365a0e83c847c9767d67ab52b2f69135dcaba
https://github.com/HOL-Theorem-Prover/HOL/commit/4b763209b040de35cf9d408e76a9c4898ce848d5
https://github.com/HOL-Theorem-Prover/HOL/commit/120e7bb43bc3ffcca4efb2cafbeed0605d620bff
https://github.com/HOL-Theorem-Prover/HOL/commit/525694a1f1c7016dea954894bea6e6e396f7d6b3

So it should be possible to port this to Isabelle. However, Irvin gave up.

Mathias

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@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@sketis.net> wrote:

On 21/10/2025 20:31, Lawrence Paulson wrote:

On 21 Oct 2025 at 19:28 +0100, Makarius <makarius@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

Email Gateway (Oct 23 2025 at 07:37):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Hi Hanna,

Thanks for the update. I wish you good luck with the last steps! The icing on the cake of any programming project is of course when it gets integrated upstream. Let me know if there's anything I can do to help (but I suspect the combined expertise of you and your coauthors is more than enough to succeed).

Best,
Jasmin

On 23. Oct 2025, at 02:13, Hanna Elif Lachnitt <lachnitt@stanford.edu> wrote:

Hi everyone,

unfortunately we don't think that we can have it ready for the RC1 in two weeks. We strive to put it in the official repo as soon as possible.

We made extensive changes and additions to the code as cvc5's proofs are far more detailed than veriT's. We also want to optimize good performance before users start using it. Since parsing is slow, having more steps can be detrimental, so we are investigating how to improve the size of cvc5 proofs.

Best,
Hanna

From: Lawrence Paulson <lp15@cam.ac.uk <mailto:lp15@cam.ac.uk>>
Sent: Wednesday, October 22, 2025 03:32
To: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de <mailto:jasmin.blanchette@ifi.lmu.de>>; Hanna Elif Lachnitt <lachnitt@stanford.edu <mailto:lachnitt@stanford.edu>>
Cc: DEV Isabelle Mailinglist <isabelle-dev@in.tum.de <mailto:isabelle-dev@in.tum.de>>
Subject: Re: Architecture problem

I'm pretty sure Hanna said that this would be in the next release. Hanna, can you offer any more details?

Larry

On 22 Oct 2025, at 08:00, Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de <mailto:jasmin.blanchette@ifi.lmu.de>> wrote:

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)?

Email Gateway (Oct 23 2025 at 12:23):

From: Tjark Weber <tjark.weber@it.uu.se>
On Wed, 2025-10-22 at 09:00 +0200, Jasmin Blanchette wrote:
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.

Ricardo Correia has made numerous improvements to that code and recently updated the supported Z3 version to 4.15.3 (the latest release).

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Email Gateway (Oct 23 2025 at 12:32):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>
Thanks for the clarification!

Inspired by this successful porting effort, we could consider updating our code to the latest Z3 as well. I have a bad memory of a previous such port (from 2010 to 2014), but maybe it would go more smoothly this time.

Jasmin

On 23. Oct 2025, at 14:22, Tjark Weber <tjark.weber@it.uu.se> wrote:

On Wed, 2025-10-22 at 09:00 +0200, Jasmin Blanchette wrote:

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.

Ricardo Correia has made numerous improvements to that code and recently updated the supported Z3 version to 4.15.3 (the latest release).

Best,
Tjark

När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy

Last updated: Nov 05 2025 at 08:30 UTC