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
default.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
