[isabelle-dev] Fwd: isabelle test failed
makarius at sketis.net
Sat Oct 15 13:23:08 CEST 2011
On Sat, 15 Oct 2011, Gerwin Klein wrote:
> This may be similar to the recent AFP failure:
> /mnt/home/isatest/isadist/Isabelle_15-Oct-2011/lib/scripts/run-polyml: line 77: 13186 Aborted "$POLY" -q $ML_OPTIONS
> HOL-MicroJava FAILED
> (see also /home/isatest/isabelle-at64-poly/heaps/polyml-5.2.1_x86_64-linux/log/HOL-MicroJava)
> Does anyone see a problem with updating that test to use poly-5.4.1?
In principle you are the one main responsible for isatest, although I did
most of the recent updates. The collective isatest/settings somehow need
to cover the officially Poly/ML versions:
Here 5.4.2 means some SVN version according to the accidental state of
/home/polyml/polyml-svn at TUM.
I now realize that I've missed the release of polyml-5.4.1 from this
summer, otherwise I had shipped that with the Isabelle release.
So for the moment the main obstable for switching at64-poly to 5.4.1 is
the lack of an installation in /home/polyml which I will produce soon.
More information about the isabelle-dev