[isabelle-dev] Isabelle release test website

Makarius makarius at sketis.net
Wed Apr 18 15:38:28 CEST 2012


On Wed, 18 Apr 2012, Johannes Hölzl wrote:

> When the testboard gives me green light I will tomorrow also push a 
> reworked Probability theory which only takes 2 min to build instead of 5 
> min as before.  I also want to push a new version of the Floats which 
> uses the new lifting infrastructure.
>
> Both changes do not change any ML files, and there are only smaller
> changes to the HOL image, so I hope it is still okay to push this.

You still have this convergence interval of 2 weeks.  I recommend to push 
within 1 week, though, since there are usually fine points to be settled 
afterwards.


Concerning the "new lifting infrastructure": I've seen many things 
floating in the past few weeks, but it was never mentioned before, and is 
not covered in NEWS.  So my impression was it is not "user-relevant" for 
this release, as the NEWS title calls it.

Also, there seem to be certain ongoing things with quotients that are 
nowhere covered. The time to do so is now.  Anything not wrapped for this 
release, is for the one after it.


 	Makarius


More information about the isabelle-dev mailing list