Email Gateway (Aug 18 2022 at 09:49): Email Gateway (Aug 18 2022 at 09:49):From: Dirk Leinenbach <dirkl@cs.uni-sb.de>
Hi,
a few days ago David Matthews announced Poly/ML 5 beta which (besides
many other improvements) is compatible with cygwin. And really, I was
able to install it with little effort under cygwin.
Now I'm trying to use it together with Isabelle2005. But there seem to
be compatibility issues between Poly/ML 5 and Isabelle2005. I don't
understand the interaction between Isabelle and Poly/ML in detail, but
for example Poly/ML 5 seems to not use `data bases' any more (at least
I didn't find a word about them and how to get ML_dbase in the
announcement). 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. Does anybody know, if a backport of these fixes to
Isabelle2005 is feasible?
Best Regards,
Email Gateway (Aug 18 2022 at 09:51):From: Makarius <makarius@sketis.net>
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
Last updated: May 03 2024 at 08:18 UTC