Email Gateway (Oct 09 2026 at 12:51): Email Gateway (Oct 09 2026 at 12:51):From: Makarius <makarius@sketis.net>
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit processes
hanging around. My original plan for the Isabelle2026 was to change its
timeout management to that of Isabelle, instead of relying on the one of veriT.
I did not do anything so far: first I was waiting for the Isabelle/HOL SMT
update, then I was busy elsewhere. The SMT update also includes a quite
different version of veriT, which could be again quite different wrt. timeouts.
So did anybody see verit processes hanging around with this new version?
Makarius
Email Gateway (Oct 11 2026 at 13:21):From: Makarius <makarius@sketis.net>
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit processes
hanging around. My original plan for the Isabelle2026 was to change its
timeout management to that of Isabelle, instead of relying on the one of veriT.I did not do anything so far: first I was waiting for the Isabelle/HOL SMT
update, then I was busy elsewhere. The SMT update also includes a quite
different version of veriT, which could be again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since
Isabelle2021, without any explanation. The critical changesets are:
changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tactic
changeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy src/HOL/SMT_Examples/Boogie_Dijkstra.certs
src/HOL/SMT_Examples/Boogie_Max.certs src/HOL/SMT_Examples/SMT_Examples.certs
src/H
OL/SMT_Examples/SMT_Word_Examples.certs src/HOL/SMT_Examples/VCC_Max.certs
src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest;
The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return to the
original smt_timeout=20 --- and no change to the invocations of the external
solvers.
Makarius
Email Gateway (Oct 11 2026 at 13:27):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I would perhaps caution against this, as at least from what I have seen,
the increase/removal of the smt timeout does in fact result in many proofs
being found that would have timed out previously, so it was useful.
If it is deemed appropriate to re-enable a timeout, I would make it much
longer: long enough that most proofs are still found, but not so long that
a runaway smt solver can persist for a very long time while sucking up CPU
and perhaps also RAM. Something on the order of 5 minutes would be
reasonable, in my opinion.
On 10/11/26 09:21, Makarius wrote:
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit processes hanging around. My original plan for
the Isabelle2026 was to change its timeout management to that of Isabelle, instead of relying on the one of veriT.I did not do anything so far: first I was waiting for the Isabelle/HOL SMT update, then I was busy elsewhere. The SMT
update also includes a quite different version of veriT, which could be again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since Isabelle2021, without any explanation. The
critical changesets are:changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tacticchangeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy src/HOL/SMT_Examples/Boogie_Dijkstra.certs src/HOL/SMT_Examples/Boogie_Max.certs src/HOL/
SMT_Examples/SMT_Examples.certs src/H
OL/SMT_Examples/SMT_Word_Examples.certs src/HOL/SMT_Examples/VCC_Max.certs src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest;The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return to the original smt_timeout=20 --- and no change
to the invocations of the external solvers.Makarius
Email Gateway (Oct 11 2026 at 13:35):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
A CPU time limit on external solvers (probably in the range of several minutes)
would seem to make the most sense to me. I tried to hack one in at one point
by interposing a shell script that set resource limits before the invocation of
verit, but I don't recall that it was completely satisfactory and I took it out.
Actually setting resource limits using a system call at the point where the
child process is invoked would be more robust, but I didn't want to spend enough
time on it to find/figure out the process invocation code and rebuild the system.
On 10/11/26 09:27, Eugene W. Stark wrote:
I would perhaps caution against this, as at least from what I have seen,
the increase/removal of the smt timeout does in fact result in many proofs
being found that would have timed out previously, so it was useful.If it is deemed appropriate to re-enable a timeout, I would make it much
longer: long enough that most proofs are still found, but not so long that
a runaway smt solver can persist for a very long time while sucking up CPU
and perhaps also RAM. Something on the order of 5 minutes would be
reasonable, in my opinion.On 10/11/26 09:21, Makarius wrote:
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit processes hanging around. My original plan for
the Isabelle2026 was to change its timeout management to that of Isabelle, instead of relying on the one of veriT.I did not do anything so far: first I was waiting for the Isabelle/HOL SMT update, then I was busy elsewhere. The SMT
update also includes a quite different version of veriT, which could be again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since Isabelle2021, without any explanation. The
critical changesets are:changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tacticchangeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy src/HOL/SMT_Examples/Boogie_Dijkstra.certs src/HOL/SMT_Examples/Boogie_Max.certs src/HOL/
SMT_Examples/SMT_Examples.certs src/H
OL/SMT_Examples/SMT_Word_Examples.certs src/HOL/SMT_Examples/VCC_Max.certs src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest;The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return to the original smt_timeout=20 --- and no change
to the invocations of the external solvers.Makarius
Email Gateway (Oct 11 2026 at 14:45):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi Makarius,
Please do not read this timeout. It is not solving problems, it is only
adding instability to the overall system and a dependency to the CPU
power of the solver.
The problem of the timeout is that it measure the time between the
beginning of the smt tactic and the moment it is proven. Except that
with isabelle build a lot of jobs and launched and it can take a lot
of time between the beginning of the tactic and the moment it is really
executed. This timeout has lead in the past to issues in the AFP
(spurious timeout that you cannot reproduce) and in Isabelle/HOL itself
(if you run Isabelle on an underpowered machine).
For everyone who has never seen this: take your favorite theory, open
the timing panel, look at the three slowest tactics. Now rerun the file
and compare the timings. Some will be faster, some will be slower by
(from what I have seen) around one order of magnitude. A hard timeout
means that you might have to run Isabelle several times to build
dependencies, because it will depend if that tactic is slow or fast
during that run.
Mathias
On 10/11/26 15:21, Makarius wrote:
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit
processes hanging around. My original plan for the Isabelle2026 was
to change its timeout management to that of Isabelle, instead of
relying on the one of veriT.I did not do anything so far: first I was waiting for the
Isabelle/HOL SMT update, then I was busy elsewhere. The SMT update
also includes a quite different version of veriT, which could be
again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since
Isabelle2021, without any explanation. The critical changesets are:changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tacticchangeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy
src/HOL/SMT_Examples/Boogie_Dijkstra.certs
src/HOL/SMT_Examples/Boogie_Max.certs
src/HOL/SMT_Examples/SMT_Examples.certs src/H
OL/SMT_Examples/SMT_Word_Examples.certs
src/HOL/SMT_Examples/VCC_Max.certs src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of
input / digest;The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return
to the original smt_timeout=20 --- and no change to the invocations of
the external solvers.Makarius
Email Gateway (Oct 11 2026 at 16:10):From: Peter <cl-isabelle-users@lists.cam.ac.uk>
Just for my understanding: Isn't the underlying problem that the veriT
process somehow becomes detached from its controlling Isabelle session?
Ideally, all processes should be killed when the underlying sledgehammer
command is cancelled, isn't it? "Fixing" that by accepting that this
doesn't happen and simply setting a timeout looks like an ad-hoc
solution to me, with potential problems for replay stability as laid out
further in this thread.
Are the rogue veriT processes only caused by sledgehammer, or also by
proper (non-diagnostic) commands like apply? If the former is the case,
couldn't we just add the timeout when invoking veriT from sledgehammer,
but leave it without timeout when invoked as tactic?
--
Peter
On 11/10/2026 15:21, Makarius wrote:
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit
processes hanging around. My original plan for the Isabelle2026 was
to change its timeout management to that of Isabelle, instead of
relying on the one of veriT.I did not do anything so far: first I was waiting for the
Isabelle/HOL SMT update, then I was busy elsewhere. The SMT update
also includes a quite different version of veriT, which could be
again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since
Isabelle2021, without any explanation. The critical changesets are:changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tacticchangeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy
src/HOL/SMT_Examples/Boogie_Dijkstra.certs
src/HOL/SMT_Examples/Boogie_Max.certs
src/HOL/SMT_Examples/SMT_Examples.certs src/H
OL/SMT_Examples/SMT_Word_Examples.certs
src/HOL/SMT_Examples/VCC_Max.certs src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of
input / digest;The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return
to the original smt_timeout=20 --- and no change to the invocations of
the external solvers.Makarius
Email Gateway (Oct 11 2026 at 16:39):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Interestingly, I had a look just now, using "top", and I happen to have a rogue cvc5-bin process (not verit).
I am using Isabelle2026-RC3 on Linux Mint 22.2:
Tasks: 435 total, 2 running, 433 sleeping, 0 stopped, 0 zombie
%Cpu(s): 5.5 us, 0.0 sy, 0.0 ni, 94.4 id, 0.1 wa, 0.0 hi, 0.0 si, 0.0 st
MiB Mem : 128623.6 total, 11739.1 free, 99920.9 used, 21077.1 buff/cache
MiB Swap: 0.0 total, 0.0 free, 0.0 used. 28702.7 avail MemPID USER PR NI VIRT RES SHR S %CPU %MEM TIME+ COMMAND
909979 gene 20 0 13.1g 12.6g 20788 R 100.0 10.1 9,16 cvc5-bin
Sledgehammer is not running, and there are no purple bars in the right-hand gutter area.
Here is a process tree output from "ps -axjf". Maybe the information in it will help someone
understand what is the relationship between the cvc5-bin process and the Isabelle session,
and why it might still be running:
12828 724318 724318 12828 pts/0 1010522 S 1000 0:00 | | \_ bash /opt/Isabelle2026-RC3/lib/Tools/java -splash:/opt/Isabelle2026-RC3/lib/logo/isabelle.gif -Dsun.java2d.metal=false -Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dapple.awt.application.appearance=system -Xms512m -Xmx4g -Xss16m isabelle.jedit.JEdit_Main
724318 724541 724318 12828 pts/0 1010522 Sl 1000 139:39 | | | \_ /opt/Isabelle2026-RC3/contrib/jdk-25.0.4/x86_64-linux/bin/java -server -Dfile.encoding=UTF-8 -Dstdin.encoding=UTF-8 -Dstdout.encoding=UTF-8 -Dstderr.encoding=UTF-8 -Disabelle.threads=0 -XX:+UseZGC -XX:+UseStringDeduplication --enable-native-access=ALL-UNNAMED --sun-misc-unsafe-memory-access=allow -classpath /opt/Isabelle2026-RC3/contrib/flatlaf-3.7.2/lib/flatlaf-3.7.2-no-natives.jar:/opt/Isabelle2026-RC3/contrib/flatlaf-3.7.2/lib/flatlaf-extras-3.7.2.jar:/opt/Isabelle2026-RC3/contrib/isabelle_setup-20260630/lib/isabelle_setup.jar:/opt/Isabelle2026-RC3/contrib/itext-2.1.5/lib/iText-2.1.5.jar:/opt/Isabelle2026-RC3/contrib/javamail-20251022/lib/jakarta.mail-api-2.1.5.jar:/opt/Isabelle2026-RC3/contrib/javamail-20251022/lib/jakarta.activation-api-2.1.4.jar:/opt/Isabelle2026-RC3/contrib/javamail-20251022/lib/angus-mail-2.0.5.jar:/opt/Isabelle2026-RC3/contrib/javamail-20251022/lib/angus-activation-2.0.3.jar:/opt/Isabelle2026-RC3/contrib/jedit-20260515/jedit5.7.0-patched/jedit.jar:/opt/Isabelle2026-RC3/contrib/jfreechart-1.5.6-1/lib/jfreechart-1.5.6.jar:/opt/Isabelle2026-RC3/contrib/jortho-1.0-2/jortho.jar:/opt/Isabelle2026-RC3/contrib/jsoup-1.21.2/lib/jsoup-1.21.2.jar:/opt/Isabelle2026-RC3/contrib/jsvg-2.0.0/lib/jsvg-2.0.0.jar:/opt/Isabelle2026-RC3/contrib/kodkodi-20260628/jar/antlr-runtime-3.1.1.jar:/opt/Isabelle2026-RC3/contrib/kodkodi-20260628/jar/kodkod-1.5.jar:/opt/Isabelle2026-RC3/contrib/kodkodi-20260628/jar/kodkodi-1.5.7.jar:/opt/Isabelle2026-RC3/contrib/kodkodi-20260628/jar/sat4j-2.3.jar:/opt/Isabelle2026-RC3/contrib/postgresql-42.7.12/lib/postgresql-42.7.12.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-library-2.13.18.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-library_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-asm-9.9.0-scala-1.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/compiler-interface-1.10.7.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-interfaces-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-compiler_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/tasty-core_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-staging_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-tasty-inspector_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/jline-reader-3.29.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/jline-terminal-3.29.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/jline-terminal-jni-3.29.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/jline-native-3.29.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-parallel-collections_3-1.2.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-parser-combinators_3-2.4.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-parser-combinators_sjs1_3-2.4.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-swing_3-3.0.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-xml_3-2.4.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-linker_2.13-1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-linker-interface_2.13-1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-ir_2.13-1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-logging_2.13-1.2.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-parallel-collections_2.13-0.2.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-library_2.13-1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-javalib-1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-scalalib_2.13-2.13.18+1.21.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala3-library_sjs1_3-3.3.8.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scalajs-dom_sjs1_3-2.8.1.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-java-time_sjs1_3-2.7.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/scala-java-locales_sjs1_3-1.5.4.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/cldr-api_sjs1_3-4.5.0.jar:/opt/Isabelle2026-RC3/contrib/scala-3.3.8-1/lib/portable-scala-reflect_sjs1_2.13-1.1.3.jar:/opt/Isabelle2026-RC3/contrib/solr-9.9.0/lib/solr-solrj-9.9.0.jar:/opt/Isabelle2026-RC3/contrib/solr-9.9.0/lib/solr-api-9.9.0.jar:/opt/Isabelle2026-RC3/contrib/solr-9.9.0/lib/solr-core-9.9.0.jar:/opt/Isabelle2026-RC3/contrib/sqlite-3.53.4.0/lib/sqlite-jdbc-3.53.4.0.jar:/opt/Isabelle2026-RC3/contrib/sqlite-3.53.4.0/lib/slf4j-api-2.0.18.jar:/opt/Isabelle2026-RC3/contrib/sqlite-3.53.4.0/lib/slf4j-nop-2.0.18.jar:/opt/Isabelle2026-RC3/contrib/xz-java-1.12/lib/xz-1.12.jar:/opt/Isabelle2026-RC3/contrib/zstd-jni-1.5.7-11/lib/zstd-jni-1.5.7-11.jar:/opt/Isabelle2026-RC3/contrib/naproche-20260903/Isabelle/naproche.jar:/opt/Isabelle2026-RC3/lib/classes/isabelle.jar:/opt/Isabelle2026-RC3/src/Tools/Demo/lib/demo.jar:/opt/Isabelle2026-RC3/lib/classes/isabelle_graphbrowser.jar:/opt/Isabelle2026-RC3/src/Tools/Scalajs_Demo/lib/scalajs_demo.jar -splash:/opt/Isabelle2026-RC3/lib/logo/isabelle.gif -Dsun.java2d.metal=false -Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle -Dapple.awt.application.appearance=system -Xms512m -Xmx4g -Xss16m isabelle.jedit.JEdit_Main
724541 724651 724318 12828 pts/0 1010522 S 1000 0:00 | | | \_ /opt/Isabelle2026-RC3/contrib/bash_process-20260628/x86_64-linux/bash_process /tmp/isabelle-gene/bash_timing12042178832686959234 bash /tmp/isabelle-gene/bash_script15557422083189852215
724651 724652 724652 724652 ? -1 Ss 1000 0:00 | | | | \_ bash /tmp/isabelle-gene/bash_script15557422083189852215
724652 724653 724652 724652 ? -1 Sl 1000 608:26 | | | | \_ /opt/Isabelle2026-RC3/contrib/polyml-5.9.2-5/x86_64-linux/poly -q --maxheap 64G --gcthreads 8 --exportstats --eval (PolyML.SaveState.loadHierarchy ["/home/gene/.isabelle/Isabelle2026-RC3/heaps/polyml-5.9.2_x86_64-linux/Pure", "/home/gene/.isabelle/Isabelle2026-RC3/heaps/polyml-5.9.2_x86_64-linux/HOL", "/home/gene/.isabelle/Isabelle2026-RC3/heaps/polyml-5.9.2_x86_64-linux/Codegen"]; PolyML.print_depth 0) --eval Print_Mode.add_modes ["brackets"] --eval Options.load_process_default () --eval Resources.init_session_env () --eval Isabelle_Process.init ()
724541 724654 724318 12828 pts/0 1010522 S 1000 0:00 | | | \_ /opt/Isabelle2026-RC3/contrib/bash_process-20260628/x86_64-linux/bash_process /tmp/isabelle-gene/bash_timing16962933835369893077 bash /tmp/isabelle-gene/bash_script10394524241022510708
724654 724656 724656 724656 ? -1 Ss 1000 0:00 | | | | \_ bash /tmp/isabelle-gene/bash_script10394524241022510708
724656 724657 724656 724656 ? -1 Sl 1000 0:00 | | | | \_ /opt/Isabelle2026-RC3/contrib/naproche-20260903/x86_64-linux/Naproche --server
724541 724731 724318 12828 pts/0 1010522 S 1000 0:00 | | | \_ /opt/Isabelle2026-RC3/contrib/bash_process-20260628/x86_64-linux/bash_process /tmp/isabelle-gene/bash_timing6915759027931769726 bash /tmp/isabelle-gene/bash_script6460271195429146234
724731 724735 724735 724735 ? -1 Ss 1000 0:00 | | | | \_ bash /tmp/isabelle-gene/bash_script6460271195429146234
724735 724739 724735 724735 ? -1 Sl 1000 2:55 | | | | \_ /opt/Isabelle2026-RC3/contrib/polyml-5.9.2-5/x86_64-linux/poly -q --use src/Pure/ML/ml_statistics.ML --eval ML_Statistics.monitor 724653 0.5
724541 909972 724318 12828 pts/0 1010522 S 1000 0:00 | | | \_ /opt/Isabelle2026-RC3/contrib/bash_process-20260628/x86_64-linux/bash_process /tmp/isabelle-gene/bash_timing7849664714219515811 bash /tmp/isabelle-gene/bash_script8574898642069030792
909972 909973 909973 909973 ? -1 Ss 1000 0:00 | | | \_ bash /tmp/isabelle-gene/bash_script8574898642069030792
909973 909978 909973 909973 ? -1 S 1000 0:00 | | | \_ bash /opt/Isabelle2026-RC3/contrib/cvc5-1.3.4/x86_64-linux/cvc5 --proof-format-mode=alethe --proof-granularity=dsl-rewrite --proof-mode=full-proof-strict --enum-inst --no-stats --sat-random-seed=1 --lang=smt2 --proof-prune --proof-prune-input --proof-e
[message truncated]
Email Gateway (Oct 11 2026 at 17:41):From: Lawrence Paulson <lp15@cam.ac.uk>
As far as I know, the problem is runaway processes (veriT and cvc5) from sledgehammer calls. So the fix should affect sledgehammer only.
Larry
On 11 Oct 2026 at 14:27 +0100, Eugene W. Stark <isabelle-users@starkeffect.com>, wrote:
I would perhaps caution against this, as at least from what I have seen,
the increase/removal of the smt timeout does in fact result in many proofs
being found that would have timed out previously, so it was useful.
If it is deemed appropriate to re-enable a timeout, I would make it much
longer: long enough that most proofs are still found, but not so long that
a runaway smt solver can persist for a very long time while sucking up CPU
and perhaps also RAM. Something on the order of 5 minutes would be
reasonable, in my opinion.
On 10/11/26 09:21, Makarius wrote:
On 09/10/2026 14:50, Makarius wrote:
Dear testers of Isabelle2026 release candidates,
in recent years, there have been occasional observations about verit processes hanging around. My original plan for
the Isabelle2026 was to change its timeout management to that of Isabelle, instead of relying on the one of veriT.I did not do anything so far: first I was waiting for the Isabelle/HOL SMT update, then I was busy elsewhere. The SMT
update also includes a quite different version of veriT, which could be again quite different wrt. timeouts.
The problem is on our side, because the smt_timeout was disabled since Isabelle2021, without any explanation. The
critical changesets are:
changeset: 72347:478b7599a1a0
parent: 72342:4195e75a92ef
user: desharna
date: Wed Sep 30 18:37:22 2020 +0200
files: src/HOL/SMT.thy src/HOL/Tools/SMT/smt_config.ML
description:
Effectively disable timeout for smt method/tactic
changeset: 73386:f3378101f555
user: wenzelm
date: Fri Mar 05 20:52:08 2021 +0100
files: src/HOL/SMT.thy src/HOL/SMT_Examples/Boogie_Dijkstra.certs src/HOL/SMT_Examples/Boogie_Max.certs src/HOL/
SMT_Examples/SMT_Examples.certs src/H
OL/SMT_Examples/SMT_Word_Examples.certs src/HOL/SMT_Examples/VCC_Max.certs src/HOL/Tools/SMT/smt_config.ML
description:
more direct unlimited smt_timeout;
update of certificates: generated command-line options are part of input / digest;
The plan for Isabelle2026-RC3 (presumably on 14-Oct-2026) is to return to the original smt_timeout=20 --- and no change
to the invocations of the external solvers.
Makarius
Email Gateway (Oct 11 2026 at 18:36):From: Makarius <makarius@sketis.net>
On 11/10/2026 18:10, Peter (via cl-isabelle-users Mailing List) wrote:
Just for my understanding: Isn't the underlying problem that the veriT process
somehow becomes detached from its controlling Isabelle session? Ideally, all
processes should be killed when the underlying sledgehammer command is
cancelled, isn't it?
I have started with these assumptions some years ago, and gave the usual
lectures on external processes that escape their process session group, and
thus cannot be killed systematically. Then I started looking at the sources
(like smt_config.ML and smt_systems.ML), and was surprised that no Isabelle
timeout management is used there, only soft limits given to the back-end tools
on the command line. So in this corner, none of our process kills will ever
happen. Today I was surprised that smt_timeout was actually not used ---
without any explanations in the history, which means that the change is
formally void, without justification.
The overall situation might turn out quite different: sledgehammer probably
has problems with the management of its tasks, and that needs to be revisited
after so many years. In particular: Why does this particular problem only
happen to the "SMT" class of tools, and not the "ATP" one?
That is a question for a future release, not the present one. We have missed
the window of opportunity already several weeks/months ago.
Makarius
Email Gateway (Oct 11 2026 at 18:49):From: Makarius <makarius@sketis.net>
On 11/10/2026 16:45, Mathias Fleury wrote:
Please do not read this timeout. It is not solving problems, it is only adding
instability to the overall system and a dependency to the CPU power of the
solver.The problem of the timeout is that it measure the time between the beginning
of the smt tactic and the moment it is proven. Except that withisabelle builda lot of jobs and launched and it can take a lot of time between the
beginning of the tactic and the moment it is really executed. This timeout has
lead in the past to issues in the AFP (spurious timeout that you cannot
reproduce) and in Isabelle/HOL itself (if you run Isabelle on an underpowered
machine).
I do agree that timeouts are generally evil, but we have different situations
for timeouts, and different partial attempts to make them more robust.
Note that it is not the case that the timeout is on the smt tactic/proof
method. The smt_timeout is for an external process running on its own, so it
is the best possible situation. The timeout could be also scaled with Isabelle
system option timeout_scale.
Despite this best case of a bad situation, I do see smt process failures
routinely, even without the timeout: notably "z3" on x86_64-darwin or
arm64-darwin. Under heavy load with many parallel build process, it is very
unreliable. That might be a problem of this particularly old z3 version, or a
general problem on the SMT setup elsewhere.
For everyone who has never seen this: take your favorite theory, open the
timing panel, look at the three slowest tactics. Now rerun the file and
compare the timings. Some will be faster, some will be slower by (from what I
have seen) around one order of magnitude. A hard timeout means that you might
have to run Isabelle several times to build dependencies, because it will
depend if that tactic is slow or fast during that run.
The timing panel is the worst-case situation on timeouts: it essentially shows
Isabelle/ML tasks running inside a parallel LISP machine with GC happening in
between. Some years ago, I have made some attempts to distinguish timeouts
with or without GC time; there is also timeout_scale applied by default. None
of this is really reliable.
The ML timeout problem remains open and needs to be revisited eventually. (Not
now, not for this release.)
Sledgehammer timeouts can probably be improved independently, by managing the
external Isabelle bash processes via Isabelle/Scala (with the existing process
timeout), instead of anything in Isabelle/ML --- nor a soft limit on the
external program.
Makarius
Email Gateway (Oct 11 2026 at 19:01):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
On 10/11/26 20:36, Makarius wrote:
I have started with these assumptions some years ago, and gave the
usual lectures on external processes that escape their process session
group, and thus cannot be killed systematically. Then I started
looking at the sources (like smt_config.ML and smt_systems.ML), and
was surprised that no Isabelle timeout management is used there, only
soft limits given to the back-end tools on the command line. So in
this corner, none of our process kills will ever happen. Today I was
surprised that smt_timeout was actually not used --- without any
explanations in the history, which means that the change is formally
void, without justification.
There are two timeouts: Sledgehammer sets a timeout (5s). This timeout
is passed to the solver. And the tool itself is invoked with a timeout:
fun get_timeout ctxt =
let val t = seconds (Config.get ctxt timeout);
in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;
fun with_time_limit ctxt error_msg timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT
(SMT_Failure.Time_Out error_msg)
On the Isabelle side:
lemma False
supply [[smt_trace]]
sledgehammer[verit]
(* --max-time=5000*)
oops
So while I understand that veriT might have bugs with the timeout: If
Timeout.apply is not the right way to run jobs with a timeout, what is
the right way then?
Mathias
The overall situation might turn out quite different: sledgehammer
probably has problems with the management of its tasks, and that needs
to be revisited after so many years. In particular: Why does this
particular problem only happen to the "SMT" class of tools, and not
the "ATP" one?That is a question for a future release, not the present one. We have
missed the window of opportunity already several weeks/months ago.Makarius
Email Gateway (Oct 11 2026 at 19:19):From: Makarius <makarius@sketis.net>
On 11/10/2026 21:01, Mathias Fleury wrote:
There are two timeouts: Sledgehammer sets a timeout (5s). This timeout is
passed to the solver. And the tool itself is invoked with a timeout:fun get_timeout ctxt =
let val t = seconds (Config.get ctxt timeout);
in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;fun with_time_limit ctxt error_msg timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT (SMT_Failure.Time_Out
error_msg)On the Isabelle side:
lemma False
supply [[smt_trace]]
sledgehammer[verit](* --max-time=5000*)
oopsSo while I understand that veriT might have bugs with the timeout: If
Timeout.apply is not the right way to run jobs with a timeout, what is the
right way then?
Timeout.apply is usually right in Isabelle/ML, but there are many
side-conditions on the overall ML runtime context. I can't say anything about
sledgehammer in this respect. Since we do see problems for some years, there
must be something wrong somewhere.
Timeouts in Isabelle/ML generally depend on more side-conditions than outside
of Isabelle/ML, notably Isabelle/Scala.
Since the current purpose is to manage an external process, it is better to
pass the timeout directly into Bash.timeout, which then ends up in a watchdog
thread on the JVM. At given times, that will produce a "kill" on the external
process. That is the most direct way to do it in Isabelle, everything else
will eventually come to that mechanism (if nothing else goes wrong on the way).
Makarius
Email Gateway (Oct 11 2026 at 19:48):From: Makarius <makarius@sketis.net>
On 11/10/2026 20:48, Makarius wrote:
I do agree that timeouts are generally evil, but we have different situations
for timeouts, and different partial attempts to make them more robust.Note that it is not the case that the timeout is on the smt tactic/proof
method. The smt_timeout is for an external process running on its own, so it
is the best possible situation. The timeout could be also scaled with Isabelle
system option timeout_scale.
We do have timeout_scale for smt_timeout already, since the following change:
changeset: 73385:a40e69fde2b4
user: wenzelm
date: Fri Mar 05 20:38:55 2021 +0100
files: src/HOL/Tools/SMT/smt_config.ML src/HOL/Tools/SMT/smt_systems.ML
src/Pure/Concurrent/timeout.ML
description:
clarified smt: support Timeout.ignored and Timeout.scale_time;
It means that e.g. "isabelle build timeout_scale=10" might have occasionally
helped, when the timeout was still there.
Makarius
Email Gateway (Oct 11 2026 at 19:57):From: Makarius <makarius@sketis.net>
On 11/10/2026 21:01, Mathias Fleury wrote:
There are two timeouts: Sledgehammer sets a timeout (5s). This timeout is
passed to the solver. And the tool itself is invoked with a timeout:fun get_timeout ctxt =
let val t = seconds (Config.get ctxt timeout);
in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;fun with_time_limit ctxt error_msg timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT (SMT_Failure.Time_Out
error_msg)
I was not aware of that.
This odd stacking of 2 timeouts for the SMT process is somewhat fragile. There
might be race conditions, which of the 2 attempts get through on time, and
there might be odd breakdowns coming from that.
I can't say if this is relevant, though. It has been like that from the very
beginning:
changeset: 36898:8e55aa1306c5
user: boehmes
date: Wed May 12 23:54:02 2010 +0200
Makarius
Email Gateway (Oct 11 2026 at 20:08):From: Makarius <makarius@sketis.net>
On 11/10/2026 21:56, Makarius wrote:
On 11/10/2026 21:01, Mathias Fleury wrote:
There are two timeouts: Sledgehammer sets a timeout (5s). This timeout is
passed to the solver. And the tool itself is invoked with a timeout:fun get_timeout ctxt =
let val t = seconds (Config.get ctxt timeout);
in if Timeout.ignored t then NONE else SOME (Timeout.scale_time t) end;fun with_time_limit ctxt error_msg timeout_config f x =
Timeout.apply (seconds (Config.get ctxt timeout_config)) f x
handle Timeout.TIMEOUT _ => raise SMT_Failure.SMT (SMT_Failure.Time_Out
error_msg)I was not aware of that.
This odd stacking of 2 timeouts for the SMT process is somewhat fragile. There
might be race conditions, which of the 2 attempts get through on time, and
there might be odd breakdowns coming from that.I can't say if this is relevant, though. It has been like that from the very
beginning:
... and there is timeout=0 anyway, so nothing happens at that point, because
of Timeout.ignored. Also note that the relevant combinator is actually
with_timeout, after with_time_limit in the above source of version
Isabelle2026-RC3.
So we are back to the question, what sledgehammer really does on its various
back-ends (ATP, SMT, ...).
Makarius
Email Gateway (Oct 13 2026 at 14:58):From: Makarius <makarius@sketis.net>
On 11/10/2026 21:18, Makarius wrote:
On 11/10/2026 21:01, Mathias Fleury wrote:
So while I understand that veriT might have bugs with the timeout: If
Timeout.apply is not the right way to run jobs with a timeout, what is the
right way then?
Timeout.apply is usually right in Isabelle/ML, but there are many side-
conditions on the overall ML runtime context. I can't say anything about
sledgehammer in this respect. Since we do see problems for some years, there
must be something wrong somewhere.
As already explained on another thread, I have now included this patch in
isabelle-release:
changeset: 85808:9d3a192c2b3f
tag: tip
user: wenzelm
date: Tue Oct 13 13:08:18 2026 +0200
files: src/Pure/Concurrent/future.ML
description:
proper Exn.reraise exn (amending 461e924cc825) --- e.g. Exn.is_interrupt
during Single_Assignment.assign, which might occur during Timeout.apply (based
on patches/Isabelle2024/future_assign_interrupt by Xu Qiyuan);
That might improve the situation, but I have no empirical proof for that. At
least 461e924cc825 is clear in being an editing mistake by myself, when I
introduced Interrupt_Break vs. Isabelle_Breakdown in recent years; and the
time span roughly corresponds to reports about verit problems.
After the release, we should dedicate some time to eliminate odd SMT options
that are better no used, e.g. smt_timeout; maybe also smt_oracle, which looks
like a sophisticated version of 'sorry'.
Makarius
Last updated: Oct 29 2026 at 04:52 UTC