[isabelle-dev] Supported Poly/ML versions
makarius at sketis.net
Sat Feb 13 14:42:25 CET 2016
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
So eventually, there will be only one current-stable Poly/ML version, the
one provided as Isabelle component for a particular Isabelle changeset id
More information about the isabelle-dev