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:
isatest/settings/afp-poly: ML_SYSTEM="polyml-5.4.0"
isatest/settings/at64-poly: ML_SYSTEM="polyml-5.2.1"
isatest/settings/at-poly: ML_SYSTEM="polyml-5.3.0"
isatest/settings/at-poly-test: ML_SYSTEM="polyml-5.4.2"
isatest/settings/at-sml-dev-e:ML_SYSTEM=smlnj
isatest/settings/cygwin-poly-e: ML_SYSTEM="polyml-5.4.2"
isatest/settings/mac-poly: ML_SYSTEM="polyml-5.2.1"
isatest/settings/mac-poly64-M2: ML_SYSTEM="polyml-5.4.0"
isatest/settings/mac-poly64-M4: ML_SYSTEM="polyml-5.4.2"
isatest/settings/mac-poly64-M8: ML_SYSTEM="polyml-5.4.2"
isatest/settings/mac-poly-M2: ML_SYSTEM="polyml-5.4.0"
isatest/settings/mac-poly-M4: ML_SYSTEM="polyml-5.4.0"
isatest/settings/mac-poly-M8: ML_SYSTEM="polyml-5.4.0"
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
