[isabelle-dev] Supported Poly/ML versions

Lars Hupel hupel at in.tum.de
Sat Feb 13 15:37:58 CET 2016


> 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.

Interesting, I wasn't even aware of that.

>   * 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.

IMHO this sounds too obscure to be useful. How many users are actually
aware of that possibility?

Cheers
Lars



More information about the isabelle-dev mailing list