Email Gateway (Aug 31 2023 at 03:14): Email Gateway (Aug 31 2023 at 03:14):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear developers,
I fail building HOL-Analysis using RC4 on Windows 11 Pro, version 22H2.
It seems smt fails. My processor is 12th Gen Intel(R) Core(TM) i7-1255U
2.60 GHz, Installed RAM is 32.0 GB (31.7 GB usable).
Actually, the same seems ocasionally happen in Isabelle 2022, but with
less frequency and often build succeeds.
This is as shown in the window of jEdit:
Build started for Isabelle/HOL-Analysis ...
Building HOL-Analysis ...
HOL-Analysis: theory HOL-Library.FuncSet
HOL-Analysis: theory HOL-Combinatorics.Transposition
HOL-Analysis: theory HOL-Library.Cancellation
HOL-Analysis: theory HOL-Library.Infinite_Set
HOL-Analysis: theory HOL-Library.Nat_Bijection
HOL-Analysis: theory HOL-Library.Old_Datatype
HOL-Analysis: theory HOL-Library.Product_Plus
HOL-Analysis: theory HOL-Library.Phantom_Type
HOL-Analysis: theory HOL-Library.Product_Order
HOL-Analysis: theory HOL-Library.Set_Algebras
HOL-Analysis: theory HOL-Analysis.Metric_Arith
HOL-Analysis: theory HOL-Analysis.Inner_Product
HOL-Analysis: theory HOL-Analysis.L2_Norm
HOL-Analysis: theory HOL-Library.Disjoint_Sets
HOL-Analysis: theory HOL-Analysis.Operator_Norm
HOL-Analysis: theory HOL-Library.Countable
HOL-Analysis: theory HOL-Library.Multiset
HOL-Analysis: theory HOL-Analysis.Poly_Roots
HOL-Analysis: theory HOL-Analysis.Product_Vector
HOL-Analysis: theory HOL-Library.Cardinality
HOL-Analysis: theory HOL-Library.Complex_Order
HOL-Analysis: theory HOL-Library.Discrete
HOL-Analysis: theory HOL-Library.Indicator_Function
HOL-Analysis: theory HOL-Library.Liminf_Limsup
HOL-Analysis: theory HOL-Library.Nonpos_Ints
HOL-Analysis: theory HOL-Library.Periodic_Fun
HOL-Analysis: theory HOL-Library.Sum_of_Squares
HOL-Analysis: theory HOL-Library.Numeral_Type
HOL-Analysis: theory HOL-Library.Countable_Set
HOL-Analysis: theory HOL-Library.Countable_Complete_Lattices
HOL-Analysis: theory HOL-Library.Equipollence
HOL-Analysis: theory HOL-Library.Set_Idioms
HOL-Analysis: theory HOL-Analysis.Continuum_Not_Denumerable
HOL-Analysis: theory HOL-Analysis.Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Abstract_Topology
HOL-Analysis: theory HOL-Analysis.Elementary_Topology
HOL-Analysis: theory HOL-Analysis.Norm_Arith
HOL-Analysis: theory HOL-Analysis.Finite_Cartesian_Product
HOL-Analysis: theory HOL-Analysis.Linear_Algebra
HOL-Analysis: theory HOL-Library.Order_Continuity
HOL-Analysis: theory HOL-Computational_Algebra.Factorial_Ring
HOL-Analysis: theory HOL-Combinatorics.Permutations
HOL-Analysis: theory HOL-Library.Extended_Nat
HOL-Analysis: theory HOL-Analysis.Affine
HOL-Analysis: theory HOL-Analysis.Abstract_Limits
HOL-Analysis: theory HOL-Analysis.FSigma
HOL-Analysis: theory HOL-Analysis.Sum_Topology
HOL-Analysis: theory HOL-Analysis.Convex
HOL-Analysis: theory HOL-Analysis.Cartesian_Space
HOL-Analysis: theory HOL-Analysis.Abstract_Topology_2
HOL-Analysis: theory HOL-Library.Extended_Real
HOL-Analysis: theory HOL-Analysis.Determinants
HOL-Analysis: theory HOL-Analysis.Connected
HOL-Analysis: theory HOL-Analysis.Elementary_Metric_Spaces
HOL-Analysis: theory HOL-Analysis.Function_Topology
HOL-Analysis: theory HOL-Analysis.Product_Topology
HOL-Analysis: theory HOL-Library.Extended_Nonnegative_Real
HOL-Analysis: theory HOL-Analysis.T1_Spaces
HOL-Analysis: theory HOL-Analysis.Lindelof_Spaces
HOL-Analysis: theory HOL-Analysis.Elementary_Normed_Spaces
HOL-Analysis: theory HOL-Analysis.Function_Metric
HOL-Analysis: theory HOL-Analysis.Isolated
HOL-Analysis: theory HOL-Analysis.Infinite_Sum
HOL-Analysis: theory HOL-Analysis.Sigma_Algebra
HOL-Analysis: theory HOL-Analysis.Topology_Euclidean_Space
HOL-Analysis: theory HOL-Computational_Algebra.Euclidean_Algorithm
HOL-Analysis: theory HOL-Analysis.Measurable
HOL-Analysis: theory HOL-Analysis.Convex_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Measure_Space
HOL-Analysis: theory HOL-Analysis.Extended_Real_Limits
HOL-Analysis: theory HOL-Analysis.Line_Segment
HOL-Analysis: theory HOL-Analysis.Tagged_Division
HOL-Analysis: theory HOL-Analysis.Ordered_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Starlike
HOL-Analysis: theory HOL-Analysis.Summation_Tests
HOL-Analysis: theory HOL-Analysis.Caratheodory
HOL-Analysis: theory HOL-Analysis.Continuous_Extension
HOL-Analysis: theory HOL-Analysis.Path_Connected
HOL-Analysis: theory HOL-Analysis.Uniform_Limit
HOL-Analysis: theory HOL-Analysis.Locally
HOL-Analysis: theory HOL-Analysis.Uncountable_Sets
HOL-Analysis: theory HOL-Analysis.Homotopy
HOL-Analysis: theory HOL-Analysis.Bounded_Continuous_Function
HOL-Analysis: theory HOL-Analysis.Bounded_Linear_Function
HOL-Analysis: theory HOL-Analysis.Abstract_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Homeomorphism
HOL-Analysis: theory HOL-Analysis.Abstract_Topological_Spaces
HOL-Analysis: theory HOL-Analysis.Derivative
HOL-Analysis: theory HOL-Computational_Algebra.Primes
HOL-Analysis: theory HOL-Computational_Algebra.Formal_Power_Series
HOL-Analysis: theory HOL-Analysis.Arcwise_Connected
HOL-Analysis: theory HOL-Analysis.Borel_Space
HOL-Analysis: theory HOL-Analysis.Cartesian_Euclidean_Space
HOL-Analysis: theory HOL-Analysis.Complex_Analysis_Basics
HOL-Analysis: theory HOL-Analysis.Abstract_Metric_Spaces
HOL-Analysis: theory HOL-Analysis.Brouwer_Fixpoint
HOL-Analysis: theory HOL-Analysis.Weierstrass_Theorems
HOL-Analysis: theory HOL-Analysis.Cross3
HOL-Analysis: theory HOL-Analysis.Polytope
HOL-Analysis: theory HOL-Analysis.Fashoda_Theorem
HOL-Analysis: theory HOL-Analysis.Retracts
HOL-Analysis: theory HOL-Analysis.Complex_Transcendental
HOL-Analysis: theory HOL-Analysis.Nonnegative_Lebesgue_Integration
HOL-Analysis: theory HOL-Analysis.Regularity
HOL-Analysis: theory HOL-Analysis.Smooth_Paths
HOL-Analysis: theory HOL-Analysis.Lipschitz
HOL-Analysis: theory HOL-Analysis.Urysohn
HOL-Analysis: theory HOL-Analysis.Generalised_Binomial_Theorem
HOL-Analysis: theory HOL-Analysis.Harmonic_Numbers
HOL-Analysis: theory HOL-Analysis.Infinite_Products
HOL-Analysis: theory HOL-Analysis.FPS_Convergence
HOL-Analysis: theory HOL-Analysis.Binary_Product_Measure
HOL-Analysis: theory HOL-Analysis.Multivariate_Analysis
HOL-Analysis: theory HOL-Analysis.Embed_Measure
HOL-Analysis: theory HOL-Analysis.Finite_Product_Measure
HOL-Analysis: theory HOL-Analysis.Bochner_Integration
HOL-Analysis: theory HOL-Analysis.Complete_Measure
HOL-Analysis: theory HOL-Analysis.Radon_Nikodym
HOL-Analysis: theory HOL-Analysis.Set_Integral
HOL-Analysis: theory HOL-Analysis.Lebesgue_Measure
HOL-Analysis: theory HOL-Analysis.Infinite_Set_Sum
HOL-Analysis: theory HOL-Analysis.Henstock_Kurzweil_Integration
HOL-Analysis: theory HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration
HOL-Analysis: theory HOL-Analysis.Integral_Test
HOL-Analysis: theory HOL-Analysis.Further_Topology
HOL-Analysis: theory HOL-Analysis.Gamma_Function
HOL-Analysis: theory HOL-Analysis.Improper_Integral
HOL-Analysis: theory HOL-Analysis.Interval_Integral
HOL-Analysis: theory HOL-Analysis.Vitali_Covering_Theorem
HOL-Analysis: theory HOL-Analysis.Equivalence_Measurable_On_Borel
HOL-Analysis: theory HOL-Analysis.Lebesgue_Integral_Substitution
HOL-Analysis: theory HOL-Analysis.Change_Of_Vars
HOL-Analysis: theory HOL-Analysis.Simplex_Content
HOL-Analysis: theory HOL-Analysis.Jordan_Curve
HOL-Analysis: theory HOL-Analysis.Ball_Volume
HOL-Analysis: theory HOL-Analysis.Analysis
HOL-Analysis FAILED (see also "isabelle build_log -H Error HOL-Analysis")
...
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 1195 of "~~/src/HOL/Analysis/Homotopy.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "qed" (line 966 of "~~/src/HOL/Analysis/Locally.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 58 of "~~/src/HOL/Analysis/Locally.thy")
*** Solver z3: Solver "z3" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 1964 of "~~/src/HOL/Analysis/Infinite_Sum.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 286 of "~~/src/HOL/Analysis/Path_Connected.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 649 of "~~/src/HOL/Analysis/Infinite_Sum.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 3216 of "~~/src/HOL/Analysis/Measure_Space.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 3487 of "~~/src/HOL/Analysis/Measure_Space.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 2009 of "~~/src/HOL/Analysis/Tagged_Division.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 583 of "~~/src/HOL/Analysis/Line_Segment.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 1037 of "~~/src/HOL/Analysis/Tagged_Division.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 243 of
"~~/src/HOL/Analysis/Topology_Euclidean_Space.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 244 of "~~/src/HOL/Analysis/Isolated.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 338 of "~~/src/HOL/Analysis/Connected.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for de
[message truncated]
Email Gateway (Aug 31 2023 at 15:20):From: Makarius <makarius@sketis.net>
...
This is bad.
On my only real Windows 11 test machine, I get exactly these kind of failures
of veriT. E.g. in the session HOL-SMT_Examples.
On my 3 virtual Windows test machines it all works fine: Windows Server 2012
R2, Windows 10, Windows 11.
The option "smt_trace" produces more information about the input to veriT, but
no clue about the actual failure.
Maybe an expert on the veriT setup can say more about it (and reproduce it in
the first place).
In the meantime, I have also made a quick experiment with a different Windows
executable from https://www.verit-solver.org/download --- namely
verit-windows-x85_64-2021.06.2-rmx.zip
No difference, same problem ...
(In contrast, our executable has been built from Source via MinGW.)
Makarius
Email Gateway (Sep 01 2023 at 06:54):From: Mathias Fleury <mathias.fleury12@gmail.com>
Hi all,
I have managed to reproduce this in Isabelle/jEdit, but only
non-deterministically and very very rarely (only twice so far) on
Windows: It seems to be related to the number of jobs running in
parallel (rerunning the faulty line always worked in my tests).
I don't really know where to start debugging this :/ but I am
unconvinced that this is veriT problem.
Does anyone have any idea how I can increase the "threading pressure" (I
have no idea how to call that) to make the issue easier to reproduce? I
have tried to copy-paste the faulty line (to have several smt calls
running at the same time) but this was not enough to help me reproduce it.
Mathias
Email Gateway (Sep 01 2023 at 07:02):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Hi, thank you for debugging this.
I don't really know where to start debugging this :/ but I am
unconvinced that this is veriT problem.
I also observe z3 (though rarely) so it's not only for veriT.
Akihisa
Does anyone have any idea how I can increase the "threading pressure" (I
have no idea how to call that) to make the issue easier to reproduce? I
have tried to copy-paste the faulty line (to have several smt calls
running at the same time) but this was not enough to help me reproduce it.Mathias
On 8/31/23 17:20, Makarius wrote:
On 31/08/2023 05:04, YAMADA, Akihisa wrote:
I fail building HOL-Analysis using RC4 on Windows 11 Pro, version 22H2.
HOL-Analysis FAILED (see also "isabelle build_log -H Error
HOL-Analysis")
...
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "by" (line 1195 of "~~/src/HOL/Analysis/Homotopy.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
"smt_trace" option for details
*** At command "qed" (line 966 of "~~/src/HOL/Analysis/Locally.thy")
*** Solver verit: Solver "verit" failed -- enable tracing using the
...This is bad.
On my only real Windows 11 test machine, I get exactly these kind of
failures of veriT. E.g. in the session HOL-SMT_Examples.On my 3 virtual Windows test machines it all works fine: Windows
Server 2012 R2, Windows 10, Windows 11.The option "smt_trace" produces more information about the input to
veriT, but no clue about the actual failure.Maybe an expert on the veriT setup can say more about it (and
reproduce it in the first place).In the meantime, I have also made a quick experiment with a different
Windows executable from https://www.verit-solver.org/download ---
namely verit-windows-x85_64-2021.06.2-rmx.zipNo difference, same problem ...
(In contrast, our executable has been built from Source via MinGW.)
Makarius
Email Gateway (Sep 01 2023 at 08:38):From: Makarius <makarius@sketis.net>
Problems with many parallel processes on Windows have occurred frequently in
the past. So my first test is always with Isabelle system option "threads=1"
for sequential mode, or a high number for more parallelism.
Even in sequential mode, I see this particular problem occur reliably.
Makarius
Email Gateway (Sep 01 2023 at 08:44):From: Makarius <makarius@sketis.net>
That is a very important observation. I derive the following working
hypotheses from it:
(1) There is something wrong with very old executables running on brand-new
Windows 11.
(2) There is something wrong with the Isabelle bash_process wrapper built
on rather old Cygwin.
Or even:
(3) There is something wrong with the Cygwin version that is used in
Isabelle2023-RC1..4.
Makarius
Email Gateway (Sep 01 2023 at 09:17):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
On 2023/09/01 17:44, Makarius wrote:
On 01/09/2023 09:02, YAMADA, Akihisa wrote:
Hi, thank you for debugging this.
I don't really know where to start debugging this :/ but I am
unconvinced that this is veriT problem.I also observe z3 (though rarely) so it's not only for veriT.
That is a very important observation. I derive the following working
hypotheses from it:(1) There is something wrong with very old executables running on
brand-new Windows 11.(2) There is something wrong with the Isabelle bash_process wrapper
built on rather old Cygwin.
Unfortunately, replacing all Cygwin binaries with the current one didn't
solve the problem.
Best - Akihisa
Or even:
(3) There is something wrong with the Cygwin version that is used in
Isabelle2023-RC1..4.Makarius
Email Gateway (Sep 01 2023 at 09:42):From: Mathias Fleury <mathias.fleury12@gmail.com>
On 9/1/23 10:38, Makarius wrote:
On 01/09/2023 08:53, Mathias Fleury wrote:
I have managed to reproduce this in Isabelle/jEdit, but only
non-deterministically and very very rarely (only twice so far) on
Windows: It seems to be related to the number of jobs running in
parallel (rerunning the faulty line always worked in my tests).Problems with many parallel processes on Windows have occurred
frequently in the past. So my first test is always with Isabelle
system option "threads=1" for sequential mode, or a high number for
more parallelism.
Maybe. But as far as I understand, with threads=1 only one thread is
running, but other tasks are scheduled (even though not executed yet).
And this seems to be key here. Otherwise, I cannot explain how hard it
is to reproduce the behavior in Isabelle/jEdit.
My current reproducer is take a goal (proven with an smt call),
duplicate it 30 times (via application of theorem of the form "P ==> P
==> ...==> P"), and running smt in a subgoal (for parallelism). Every
3rd time (or so), I get such an error.
Internally, the following happens:
1. smt is running solvers on bash by "solver input_file > proof_file
2>&1" (by default with files in the cache).
2. the output proof_file is read
The issue here is that in 2 the file is empty.
I managed to read the proof_file (by specifying the names of the files
supply [[smt_debug_files="/tmp/test"]] and making sure that the names
are unique!) and the files contain the right proof (md5sum identical to
the working ones).
Mathias
Even in sequential mode, I see this particular problem occur reliably.
Makarius
Email Gateway (Sep 01 2023 at 10:01):From: Mathias Fleury <mathias.fleury12@gmail.com>
I finally got a proper error message:
exception Io {cause =
SysErr
("The process cannot access the file because it is
being used by another process.",
SOME ERROR_SHARING_VIOLATION),
function = "BinIO.openIn", name =
"C:\\Users\\zmath\\Desktop\\Isabelle2023-RC4\\contrib\\cygwin\\tmp\\X12.smt_out"}
raised (line 116 of "./basis/BinIO.sml")
It seems to be a Windows-only error …
So I guess that the file is still opened by some process (but which?
bash? Windows defender?), explaining why Isabelle considers it as empty
(all errors are swallowed) and checking the proof later works.
Mathias
Email Gateway (Sep 01 2023 at 13:55):From: Makarius <makarius@sketis.net>
That is an important hint. I will dig further into the Isabelle/ML
implementations behind this particular tmp-file management ...
Makarius
Email Gateway (Sep 01 2023 at 16:00):From: Makarius <makarius@sketis.net>
I was confused by the above /tmp/X12.smt_out, but now I guess it is probably
the result use manual insertion of smt_debug_files="/tmp/X12" --- Is that correct?
Makarius
Email Gateway (Sep 01 2023 at 16:32):From: mathias.fleury12@gmail.com
Yes exactly. This is the only way I found to read file in order to check if there is a proof there or not.
Mathias Fleury
Email Gateway (Sep 01 2023 at 21:23):From: Makarius <makarius@sketis.net>
On 01/09/2023 11:41, Mathias Fleury wrote:
Internally, the following happens:
1. smt is running solvers on bash by "solver input_file > proof_file 2>&1"
(by default with files in the cache).
2. the output proof_file is readThe issue here is that in 2 the file is empty.
Email Gateway (Sep 04 2023 at 06:25):From: "YAMADA, Akihisa" <ayamada@trs.cm.is.nagoya-u.ac.jp>
Dear Makarius, Mathias,
thank you for debugging and fixing this! RC5 works, and I don't
experience any problem so far.
Best,
Akihisa
Last updated: Apr 28 2024 at 16:17 UTC