Stream: Mirror: Isabelle Development Mailing List

Topic: SMT reconstruction failures

view this post on Zulip Email Gateway (Jul 15 2025 at 15:37):

From: Fabian Huch <huch@in.tum.de>
As of Isabelle/3e1521dc095d and AFP/8851801a38e0, I am getting SMT failures:

isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms
Running Modular_arithmetic_LLL_and_HNF_algorithms ...
Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle
build_log -H Error Modular_arithmetic_LLL_and_HNF_algorithms")
*** Failed to apply initial proof method (line 6705 of
"$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):
*** goal (1 subgoal):
***  1. A $$ (0, 0) =
***     A'' $$
***     (0, 0)
*** At command "by" (line 6705 of
"$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy")
Unfinished session(s): Modular_arithmetic_LLL_and_HNF_algorithms
0:15:36 elapsed time, 1:39:03 cpu time, factor 6.35

This is both in the build and interactive session; declaring
[[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be
improved so we don't have these timeout issues even if things are
slightly slower?

The problem appears after the merge in Isabelle/1e39653de974. But I have
the suspicion that those changes only uncovered an existing problem,
which otherwise manifests as spurious SMT failures during scheduled build.

Fabian

view this post on Zulip Email Gateway (Jul 15 2025 at 15:46):

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

This is both in the build and interactive session; declaring [[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be improved so we don't have these timeout issues even if things are slightly slower?

The obvious fix is to disable the timeout or crank it up very high. But since it's "smt_reconstruction_step_timeout" and not "smt_timeout", I'm wondering if there might be some nonmonotonic aspects to consider. E.g. is there any code of the form "try reconstruction step A for smt_reconstruction_step_timeout seconds; if this fails, try reconstruction step B". I guess the best way to find out is to try it out.

Note that I (like you) have inherited this situation. I didn't invent this timeout and am generally suspicious of tactic-specific timeouts.

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 15. Jul 2025, at 17:36, Fabian Huch <huch@in.tum.de> wrote:

As of Isabelle/3e1521dc095d and AFP/8851801a38e0, I am getting SMT failures:

isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms
Running Modular_arithmetic_LLL_and_HNF_algorithms ...
Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle build_log -H Error Modular_arithmetic_LLL_and_HNF_algorithms")
*** Failed to apply initial proof method (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):
*** goal (1 subgoal):
*** 1. A $$ (0, 0) =
*** A'' $$
*** (0, 0)
*** At command "by" (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy")
Unfinished session(s): Modular_arithmetic_LLL_and_HNF_algorithms
0:15:36 elapsed time, 1:39:03 cpu time, factor 6.35

This is both in the build and interactive session; declaring [[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be improved so we don't have these timeout issues even if things are slightly slower?

The problem appears after the merge in Isabelle/1e39653de974. But I have the suspicion that those changes only uncovered an existing problem, which otherwise manifests as spurious SMT failures during scheduled build.

Fabian

view this post on Zulip Email Gateway (Jul 15 2025 at 17:23):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
This also wasted my time. Seeing the failure, I tried to run the session locally and nothing happened. Like Jasmin I am not sure why a timeout is there.

On 15 Jul 2025, at 16:36, Fabian Huch <huch@in.tum.de> wrote:

isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms
Running Modular_arithmetic_LLL_and_HNF_algorithms ...
Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle build_log -H Error Modular_arithmetic_LLL_and_HNF_algorithms")
*** Failed to apply initial proof method (line 6705 of "$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):
*** goal (1 subgoal):
*** 1. A $$ (0, 0) =
*** A'' $$
*** (0, 0)
*** At command "by" (line 6705 of "

view this post on Zulip Email Gateway (Jul 17 2025 at 20:22):

From: Makarius <makarius@sketis.net>
On 15/07/2025 17:36, Fabian Huch wrote:

As of Isabelle/3e1521dc095d and AFP/8851801a38e0, I am getting SMT failures:

isabelle build -A: Modular_arithmetic_LLL_and_HNF_algorithms
Running Modular_arithmetic_LLL_and_HNF_algorithms ...
Modular_arithmetic_LLL_and_HNF_algorithms FAILED (see also "isabelle build_log
-H Error Modular_arithmetic_LLL_and_HNF_algorithms")
*** Failed to apply initial proof method (line 6705 of "$AFP/
Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"):
*** goal (1 subgoal):
***  1. A $$ (0, 0) =
***     A'' $$
***     (0, 0)
*** At command "by" (line 6705 of "$AFP/
Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy")
Unfinished session(s): Modular_arithmetic_LLL_and_HNF_algorithms
0:15:36 elapsed time, 1:39:03 cpu time, factor 6.35

This is both in the build and interactive session; declaring
[[smt_reconstruction_step_timeout=0]] helps. Can the SMT situation be improved
so we don't have these timeout issues even if things are slightly slower?

The problem appears after the merge in Isabelle/1e39653de974. But I have the
suspicion that those changes only uncovered an existing problem, which
otherwise manifests as spurious SMT failures during scheduled build.

I only managed to reproduce the problem by using
smt_reconstruction_step_timeout=3 instead of the default 10 --- both my local
test machine and the build cluster are too fast for it.

Doing a bisection, reveals the following result:

changeset: 82837:8aa1c98b948b
user: wenzelm
date: Fri Jul 11 14:03:09 2025 +0200
files: src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
src/Provers/classical.ML src/Pure/bires.ML
description:
maintain collective rule declarations via type Bires.decls, with netpair
operations derived from it;

I've been there many times recently, to sort out remaining omissions in the
rather delicate treatment of classical rules.

I will sort this out very soon, but not tomorrow.

Makarius

view this post on Zulip Email Gateway (Jul 21 2025 at 14:51):

From: Makarius <makarius@sketis.net>
On 17/07/2025 22:22, Makarius wrote:

Doing a bisection, reveals the following result:

changeset:   82837:8aa1c98b948b
user:        wenzelm
date:        Fri Jul 11 14:03:09 2025 +0200
files:       src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML src/Provers/
classical.ML src/Pure/bires.ML
description:
maintain collective rule declarations via type Bires.decls, with netpair
operations derived from it;

I've been there many times recently, to sort out remaining omissions in the
rather delicate treatment of classical rules.

I've finished this now, after a few more sidetracks:

changeset: 82890:72707b844734
user: wenzelm
date: Mon Jul 21 12:57:58 2025 +0200
files: NEWS src/Pure/bires.ML
description:
clarified merge order: accurately reproduce the stable status-quo from
53e56e6a67c3 --- e.g. relevant for smt proof reconstruction in (line 6705 of
"$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy") of
AFP/f1299d4f896c;

changeset: 15862:eae86974a665
tag: tip
user: wenzelm
date: Mon Jul 21 15:24:31 2025 +0200
files: thys/Buchi_Complementation/Complementation_Implement.thy
thys/Tree_Enumeration/Rooted_Tree.thy
description:
backout d06954e7388a: no longer required thanks to Isabelle/72707b844734;

I will say more about the cumulative archeological findings on a different thread.

Makarius

Last updated: Aug 31 2025 at 20:21 UTC