Email Gateway (Nov 10 2025 at 22:10): Email Gateway (Nov 10 2025 at 22:10):From: Makarius <makarius@sketis.net>
On 06/11/2025 19:24, Lawrence Paulson via isabelle-dev wrote:
While we are thinking about the next release, I thought I would bring up an intermittent issue. I use sledgehammer quite a lot, and sometimes things grind to a halt. Then I check the process monitor and find many copies of veriT seemingly looping. It's okay to just kill them. But I imagine this annoys a lot of people and I wonder if there is a way of preventing it. Does anybody else experience this?
I have made a pro-forma update of the verit component for macOS:
changeset: 83544:d1a66e53c15c
tag: tip
user: wenzelm
date: Mon Nov 10 22:28:18 2025 +0100
summary: rebuild "verit" for arm64-darwin (new) and x86_64-darwin, using
current platform baseline (macOS 12);
I had done that before for Linux:
changeset: 79563:76ad72736e9e
user: wenzelm
date: Wed Jan 31 22:36:12 2024 +0100
files: Admin/components/PLATFORMS Admin/components/components.sha1
Admin/components/main
description:
rebuild "verit" for arm64-linux for more robustness, e.g. relevant for theory
"HOL-ex.BigO";
uniform baseline for "linux" and "linux_arm";
That was always the same veriT version from 4 years ago:
changeset: 74812:ed3adabf0dbe
user: wenzelm
date: Fri Nov 19 20:35:35 2021 +0100
files: Admin/components/components.sha1 Admin/components/main
src/Pure/Admin/build_verit.scala
description:
updated to verit-2021.06.2-rmx;
... actually from 5 years ago, see https://verit.loria.fr/download
Under the heading "UNSTABLE" I see this notable Changelog entry:
Maybe that helps. So it might be a good time to prompt the veriT guys to make
a new stable release eventually. (The sledgehammer and/or SMT guys need to do
this.)
Makarius
Email Gateway (Nov 10 2025 at 23:22):From: Alexander Pach via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
Am 10.11.25 um 23:09 schrieb Makarius:
Maybe that helps. So it might be a good time to prompt the veriT guys
to make a new stable release eventually. (The sledgehammer and/or SMT
guys need to do this.)
Dear Makarius, dear list,
for completeness sake:
There is a newer stable release (and a bugfix release based upon that)
currently available on <https://www.verit-solver.org/download/>, the
latest of which is version 2024.12.1 from 2025-03-01.
The changelog
<https://www.verit-solver.org/download/2024.12.1/CHANGELOG>
mentions some (incompatible) changes to the proof output and the Alethe
specification.
Alexander
Email Gateway (Nov 11 2025 at 00:10):From: Makarius <makarius@sketis.net>
On 11/11/2025 00:22, Alexander Pach via isabelle-dev wrote:
Dear Makarius, dear list,
for completeness sake:
There is a newer stable release (and a bugfix release based upon that)
currently available on <https://www.verit-solver.org/download/>, the latest of
which is version 2024.12.1 from 2025-03-01.
Thanks for the hint. That is a new download URL, which I have recorded here:
changeset: 83545:b7d4dddac250
tag: tip
user: wenzelm
date: Tue Nov 11 01:03:45 2025 +0100
summary: update URL for veriT download, without change of its version;
The changelog <https://www.verit-solver.org/download/2024.12.1/CHANGELOG>
mentions some (incompatible) changes to the proof output and the Alethe
specification.
I can only make pro-forma updates. It is up to our "SMT guys" to say when a
new version should be used. Currently, I proceed under the assumption of "not
now and not for this Isabelle release".
Makarius
Last updated: Nov 16 2025 at 12:39 UTC