Re: [isabelle] using Haskabelle with recent versions of GHC



Dear Andrew,

a problem with Haskabelle is that it is unmaintained and did not even
make it into the current Isabelle2016-1 release.  It is however part of
the earlier Isabelle2016 release, available at
http://isabelle.in.tum.de/website-Isabelle2016/index.html.  But note
that the relevant parts of the Isar language have been stable enough
that theory files generated by Haskabelle coming with older Isabelle
releases should still be usable in Isabelle2016-1.

Getting to the core of your question:

> However - we see that Haskabelle requires an earlier version of Haskell-src-exts than that installed by Artur,
> and you talk about  GHC 7.6.3 in the documentation with Isabelle-2016.

no, there isn't.

As far as I remember, at some stage after giving Haskabelle maintainance
out of my hands more than six years ago, newer versions of
haskell-src-exts changed their data model in a fashion that would have
required a substantial rethinking and reimplementation of parts of
Haskabelle, hence this stuck to a quite ancient version.

I am at a loss to explain how Haskell maintainers / users coped with
that over the last years; the documentation does not give specific hints.

My experiments just revealed that newly emerged ingredients of the
Haskell Prelude clash with symbols defined in Haskabelle for ghc 7.10.3
which is shipped with my OS.

Maybe the best solution is to place a wholly separate ghc installation
on your machine that is only used for Haskabelle.

The situation exhibits serious need for volunteers to step in and take
over Haskabelle maintainance.

Hope this helps,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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