[isabelle-dev] moving isatest to poly 5.4

[Gerwin Klein]

On 17/12/2010, at 10:03 PM, Makarius wrote:

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

Ok, that's bad. This means I should probably move only one of the isatests to poly-svn (as you suggest) and run AFP on that. That's not ideal, though. It should run with whatever we recommend users run.


> So far I did not find time for looking more closely, and official Poly/ML 5.3 is sufficiently stable.

Well, no, it's not, that's the whole point. It's been flaky with concurrency and current Isabelle, not so much for small sessions, but certainly for big ones. According to Andreas, after his changes to JinjaThreads, the AFP test crashes more often than not on his local machine with poly 5.3, but works fine with poly 5.4. He's holding back pushing his change, because he's afraid it will just fail all the time.

If poly 5.4 has other problems, we can't make it the official platform, of course. Does DM know about this and is happy to make another poly release in time for the next Isabelle release?

Cheers,
Gerwin