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