Email Gateway (Nov 15 2021 at 13:25): Email Gateway (Nov 15 2021 at 13:25):From: Dominique Unruh <unruh@ut.ee>
Hi,
I have some theories that work fine under RC3 on Linux, but fail on
Windows in several places.
Examples of offending commands are:
by (smt (verit, ccfv_threshold) Int_Collect fun_upd_def fun_upd_triv
fun_upd_upd mem_Collect_eq)
by (smt (verit, del_insts) SigmaE case_prod_conv comp_def
fun_upd_def insert.hyps(1) insert.hyps(2) prod.cong prod.insert
summable_on_cong)
by (smt (verit, ccfv_threshold) Int_Collect fun_upd_def fun_upd_triv
fun_upd_upd mem_Collect_eq)
Under Linux, the whole theory processes in a few seconds. Under Windows,
some of the verit processes grow in memory consumption slowly until
~25GB at which point my Windows laptop runs out of swap, and some give
errors such as this:
have summable2: (λ(p, y). f x y * (∏x'∈F. f x' (p x'))) summable_on
Pi⇩E F B × B x
Tactic failed
The error(s) above occurred for the goal statement⌂:
SMT.fun_app (λ(uu, y). uu(x := y)) veriT_sk1 ≠ SMT.fun_app (λ(uu,
y). uu(x := y)) (veriT_sk5, veriT_sk6) ∨
(λuua. f uua (SMT.fun_app (λ(uu, y). uu(x := y)) veriT_sk1 uua)) =
(λuua. f uua (SMT.fun_app (λ(uu, y). uu(x := y)) (veriT_sk5,
veriT_sk6) uua))
Note: the problem is not that verit fails or does not terminate (after
all, on an unprovable problem, it is well allowed to do so), but that a
theory that works under Linux fails under Windows.
The whole offending theory is here:
https://github.com/dominique-unruh/qrhl-tool/blob/master/isabelle-thys/Infinite_Sum_Missing.thy
(it has no dependencies from that github archive, so it can be
downloaded and tested on its own).
I also had transient problems when compiling HOL-Analysis on the same
Windows computer (veriT failures in theory Infinite_Sum), and
AFP/Complex_Bounded_Operators. Those were, however, overcome by repeated
compilation attempts and now I have working heap images. The problems in
the theory I am linking here however persist.
Best wishes,
Dominique.
Email Gateway (Nov 15 2021 at 16:35):From: Mathias Fleury <mathias.fleury12@gmail.com>
Thank you a lot for your report.
We have pinned the issue to a behavior difference between Windows and
Linux in the "--inst-deletion" option in veriT itself. Hans-Jörg (in CC)
is currently investigating the issue in the veriT source code.
Mathias
Email Gateway (Nov 18 2021 at 12:56):From: Martin Desharnais <martin.desharnais@posteo.de>
Hi all,
Hans-Jörg and Mathias have been hard at work in the last days debugging
this issue, finding a fix, and testing a new patched version
2021.06.2-rmx. The proof search heuristics changed as a result, but no
failing smt calls were observed in the AFP.
The source code is available at the following address.
https://verit.loria.fr/download/2021.06.2/verit-2021.06.2-rmx.tar.gz
And it can now be built and added as default component for both the
release candidate and the development version.
Cheers,
Martin
Email Gateway (Nov 19 2021 at 20:02):From: Makarius <makarius@sketis.net>
It is now on
https://isabelle.sketis.net/repos/isabelle-release/rev/ed3adabf0dbe for the
next release candidate, to be expected within a few days. (It will come back
to the development repository later.)
Makarius
Email Gateway (Dec 04 2021 at 22:09):From: Dominique Unruh <unruh@ut.ee>
I can confirm that my developments (that revealed the problem in the
first place) now work the same (i.e., successfully) on Windows, Linux,
MacOS.
Best wishes,
Dominique.
Last updated: Jul 15 2022 at 23:21 UTC