[isabelle-dev] Fwd: isabelle test failed

[Makarius]

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