Stream: Archive Mirror: Isabelle Users Mailing List

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


view this post on Zulip Email Gateway (Aug 22 2022 at 14:40):

From: Artur Gomes <gomesa@tcd.ie>
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,

view this post on Zulip Email Gateway (Aug 22 2022 at 14:53):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc


Last updated: Apr 20 2024 at 12:26 UTC