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



Dear Florian,

Thank you for your replies. I've managed to work with Haskabelle using the
2015 version of Isabelle, and I think I'll stick with it. It works for me.
Moreover, I wrote a small script that extracts only the Haskell code from
my
latex+Haskell mixture. I'm not begin able to translate a few things, but
I'll have
a closer look before coming back to you with further questions.

Best regards,

On 17 December 2016 at 18:11, Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:

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


-- 
Artur Oliveira Gomes
PhD Student - SCSS - Trinity College Dublin
Professor - Sistemas de InformaÃÃo - UFMS



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