Re: [isabelle] Isabelle2005 with Poly/ML 5 and cygwin
On Wed, 25 Oct 2006, Dirk Leinenbach wrote:
> a few days ago David Matthews announced Poly/ML 5 beta
> Now I'm trying to use it together with Isabelle2005. But there seem to
> be compatibility issues between Poly/ML 5 and Isabelle2005.
Well, Isabelle2005 simply lacks the compatibility layer required between
Isabelle and any ML system -- Poly/ML 4.1.4 is the latest version
Poly/ML 5 is quite dissimilar to the 4.x line in many respects. We have
started to work with Poly/ML 5 in recent internal development versions of
Isabelle, see http://isabelle.in.tum.de/devel/ for the usual snapshots.
There are still some fine points to be sorted out, e.g. compiling logic
images for 32bit x86 on a x86_64 platform. (Maybe somebody out there knows
the magic option for cc/ld to do this.)
> Nevertheless, David wrote on his web page that Makarius was able to run
> Isabelle with Poly/ML 5 after some bug fixes. I guess that these bug
> fixes have been applied to the development version of Isabelle.
David refers to bug fixes in Poly/ML, not Isabelle.
> Does anybody know, if a backport of these fixes to Isabelle2005 is
It should be in principle feasible, but there are no plans to do that.
Producing an official Isabelle distribution takes many weeks -- even if
the actual changes are minimal. The next official Isabelle release will
certainly support Poly/ML 5.
This archive was generated by a fusion of
Pipermail (Mailman edition) and