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