Re: [isabelle] Isabelle2021-1-RC3: smt (verit) behaves differently under Linux and Windows

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.


On 15/11/2021 14:23, Dominique Unruh wrote:


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: (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,

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.