Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer



On 27/05/2019 10:19, Jasmin Blanchette wrote:
> 
>> I am unsure what to do now (approx. 2 weeks before the final launch of
>> the release).
> 
> To the best of my knowledge, the situation hasn't changed in the past year -- i.e. if we could live with it for 2017, so could we for 2018.
> 
> Maybe it would be worthwhile to try the binaries here and see if that improves the situation:
> 
> 	https://github.com/z3prover/z3/releases
> 
> If so, I could repackage Z3 and have the new package in the release.

Thanks for the offer.

I was recently discussing with Sascha Böhme if we should make a proper
update of Z3, but that requires a bit more work, so we decided against
it for the Isabelle2019 release.

I somehow suspect that the problems we see now are due to the change of
the environment, i.e. latent fragilities now become apparent due to one
or more of these reasons:

  * unknown changes in Cygwin (64bit version, other changes)
  * unknown changes in Windows 10
  * unknown changes in the hardware: much faster process creation due to
SSD etc.

(I will continue on a different side-branch of this thread.)


	Makarius




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