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

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 
> feasible?

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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.