Re: [isabelle] Isabelle2019-RC2 sporadic smt failures



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.

On my various test machines (Linux, macOS, Windows) I don't see any such
problems.


	Makarius




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