Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



On 5/25/2019 7:18 PM, Makarius wrote:
On 24/05/2019 20:59, Makarius wrote:
On 24/05/2019 19:09, Mathias Fleury wrote:

I managed to find an old windows machine and I can reproduce the bug (sometimes at least). And the results are just weird.

smt works as follows:
   (exec 2>&1; z3 ‹input_file›)> ‹temporary_file›

The "(exec ...) > ..." scheme goes back to the original version by
Jasmin Blanchette from 2014:
http://isabelle.in.tum.de/repos/isabelle/rev/624faeda77b5#l12.56 -- so
the history does not say anything about the reasons for that. Maybe
Jasmin can recall them.


To robustify that bash script, I have made the following changes for the
next release candidate:

   * Update of Cygwin:
https://isabelle.sketis.net/repos/isabelle-release/rev/b0fd8167bb9b

   * Avoid extra subprocess:
https://isabelle.sketis.net/repos/isabelle-release/rev/2e101846ad8f


I will publish Isabelle2019-RC3 tomorrow, with all the other minor
changes that have accumulated in the past 2 weeks.

The above changes are already in Isabelle2019-RC3. Can you try if it
makes a difference.
It is better now, but I still get 6-7 failures in 400 runs. (It was 20 failures with Isabelle2019-RC2)

On 5/24/2019 7:09 PM, Mathias Fleury wrote:
Out of curiosity, do you have an SSD or a hard drive?
I have an SSD.

Fabian

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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