[isabelle-dev] NEWS: support for GHC

[Makarius]

On 08/11/2018 12:16, 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.
> 
> 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.

A remaining use of "unmanaged" ghc is actually ocaml: I would like to
keep these tools as uniform as possible, see also current a41f49148525.
Unfortunately, OPAM is not as advanced as stack yet, e.g. it does not
quite work on Windows so the Cygwin ocaml is still needed.

We could move the other way and discontinue the meaning of $ISABELLE_GHC
and $ISABELLE_OCAMLC as actual executables: the settings would merely
indicate the presence of these tools, e.g. for options [condition =
ISABELLE_GHC] in session ROOT entries.

It probably would require some changes of the Codegen setup, because
that wants to see a single environment variable instead of a
command-line fragment like "isabelle ghc" or "isabelle ocamlc".


	Makarius