Email Gateway (Jul 15 2025 at 15:37): 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
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.35This 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
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 "
Last updated: Jul 17 2025 at 01:56 UTC