[isabelle-dev] NEWS: support for GHC

Makarius makarius at sketis.net
Thu Nov 8 12:16:38 CET 2018

On 08/11/2018 11:30, Bertram Felgenhauer wrote:
> Makarius wrote:
>> Nonetheless, it is still possible to use "isabelle ghc" without stack:
>> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the
>> Isabelle settings mechanism to override ISABELLE_GHC with the
>> stack-based tools.
> After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about
> a missing GHC setup, since there's no fallback on a custom
> $ISABELLE_GHC. I've added such a fallback in the attached patch,
> does that look reasonable?

I've misunderstood the problem. You intend to invoke old-style
$ISABELLE_GHC via the new-style "isabelle ghc" interface, but within
Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases.

So just the usual question: What are remaining uses of this? Why not
uninstall the "system ghc" and only use stack? It should be possible to
direct ISABELLE_STACK_ROOT to an existing stack setup, and worth sorting
out remaining problems on that side.

My impression is that up-to-date Haskell projects are all using stack by


More information about the isabelle-dev mailing list