[isabelle-dev] moving isatest to poly 5.4

Makarius makarius at sketis.net
Fri Dec 17 12:03:44 CET 2010


On Fri, 17 Dec 2010, Gerwin Klein wrote:

> Andreas Lochbihler pointed out that the AFP test is still running polyml 
> version 5.3 as is most of isatest.
>
> Any arguments against moving all of this to polyml 5.4?

Well, we do not have an official stable Poly/ML 5.4 for Isabelle yet.

5.4 has a problem with bigints in certain situations, so it would need at 
least one extra patch from the SVN.  So far I did not find time for 
looking more closely, and official Poly/ML 5.3 is sufficiently stable.


> If not, I'll attempt that tomorrow. This may fix some of the concurrency 
> stability problems.

There is no problem to use an internal SVN version of Poly/ML for an 
internal AFP test, if you don't care to know which one it is.  See 
/home/polyml/polyml-svn in the NFS at TUM.


 	Makarius



More information about the isabelle-dev mailing list