[isabelle-dev] NEWS: support for GHC

Bertram Felgenhauer bertram.felgenhauer at googlemail.com
Thu Nov 8 14:59:28 CET 2018


Makarius wrote:
> 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.

This may be premature, but I foresee that now that `isabelle ghc`
and `isabelle ghci` exist, we will have scripts that use them.

> So just the usual question: What are remaining uses of this? Why not
> uninstall the "system ghc" and only use stack?

I don't think that the desire of using an existing ghc installation is
unusual. I'm not sure how common maintaining a ghc installation without
stack is these days, but ghc + cabal-install are still quite sufficient
for Haskell development. I don't care much about disk space, but I do
resent stack's propensity for downloading huge tarballs without even
prompting; my bandwidth is often limited. So I try hard to avoid that
particular tool.

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

My desire is to be able to override the default, not to change it.

Cheers,

Bertram



More information about the isabelle-dev mailing list