Re: [isabelle] Isabelle2019-RC2 sporadic smt failures

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›
> From this, two information are extracted:
>   1. the return code to indicate the kind of result (error/unknown)
>   2. the temporary_file
> Here comes the interesting part. Under heavy load*, the ‹temporary_file› might not contain what I would expect to be there. The content can be corrupted and in particular, it can be empty.
> I have no idea what changed since Isabelle2018 that could cause a change in the behaviour. I will think about it, but if anyone has an idea…

There is a change in the Cygwin version for Windows. Cygwin introduces
extra complexity and can fail in funny ways, e.g. due to extra nesting
of processes as above.

The "(exec ...) > ..." scheme goes back to the original version by
Jasmin Blanchette from 2014: -- 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:

  * Avoid extra subprocess:

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


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