[isabelle-dev] Poly/ML 5.7

[Makarius]

David Matthews has made the Poly/ML 5.7 release snapshot some weeks ago
(see https://github.com/polyml/polyml/releases/tag/v5.7), but announced
it only last week.

I have wrapped that up as a component in Isabelle/d3c5898f1a5e, but that
is only for testing, not for production use. Some results can be seen here:

http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux/index.html
http://isabelle.in.tum.de/devel/build_status/Poly_ML_5.7_Linux_2_threads/index.html

The test hardware is similar or actually the same as "Linux A", but this
needs to be investigated further. It is also important to compare
timings for the *same* Isabelle versions, but the Poly_ML_5.7_Linux task
is still busy digging into older history.


After the substantial changes of the code generator and representation
of ML values in memory, there are various open questions concerning
performance and robustness of Isabelle applications.

This means, we need to skip the Poly/ML 5.7 release and stay on the last
Poly/ML 5.6 until the situation becomes more clear.


This is how to use the polyml-5.7 component locally:

  $ edit $ISABELLE_HOME_USER/etc/settings

  init_component "$HOME/.isabelle/contrib/polyml-5.7"

  $ isabelle components -a


	Makarius