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:
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.


	Makarius




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