[isabelle] Isabelle2005 with Poly/ML 5 and cygwin



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,


--

Dirk Leinenbach
Computer Science Department
Saarland University
Germany
Building E1 1, Room 4.06

phone: +49 - 681 / 302 - 57379
fax:   +49 - 681 / 302 - 4132 

Attachment: pgpBPO2AHWlpJ.pgp
Description: PGP signature



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