[isabelle-dev] Supported Poly/ML versions

[Makarius]

How many versions of Poly/ML do we still need to support?

This question is relevant for the transition of isatest to Jenkins: many 
isatest jobs are there to run old Poly/ML versions, and these CPU cycles 
could be spared or put into better use.

Moreover there is a potential for simplification of Isabelle/ML system 
modules, eliminating variants of conditional compilation.


Looking through the sources and Admin/Release files a bit, my current 
conclusion is as follows:

   * Official stable Poly/ML (presently 5.6), as provided via
     Admin/components/main, is the single ML platform for all applications.

   * Old Poly/ML 5.3.0 is still needed in rare situations to obtain a
     detailed exception trace. Note that this needs to be done with
     isabelle_process or isabelle console, since PIDE requires socket I/O
     and Poly/ML 5.3.0 does not work with that anymore.

   * All other historic Poly/ML versions can be discontinued: 5.4.x, 5.5.x.

Clearing out the bottom of Isabelle/ML will also help to use more Poly/ML 
add-ons from recent years. At some point I would like to use the debugger 
in Pure, and that could actually make the old exception_trace of Poly/ML 
5.3.0 obsolete.

So eventually, there will be only one current-stable Poly/ML version, the 
one provided as Isabelle component for a particular Isabelle changeset id 
(or release).


 	Makarius