Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
We probably still have a few occurrences of these, but no problem phasing them
out.
Cheers,
Gerwin
On 09.11.2018, at 10:03, Peter Lammich
mailto:lamm...@in.tum.de>> wrote:
I sometimes see {* *} in old theory files, and find it funny to be reminded
that this was standard only 5 years ago ... from my side there are no uses of
this quotation remaining that I'd know of
However, (* *) is still very important for informally andquickly commenting
things out, also in inner syntax!
Peter
Original Message
Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?
From: Makarius
To: isabelle-dev
CC:
Over the decades we have accumulated funny quotation forms in Isabelle
syntax that are often hard to explain to new users (also to old users).
In particular, what are the remaining uses of {* ... *}?
It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get rid of it (as well as `alt_string`).
The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ... from my side there are no uses of this quotation remaining that I'd know ofHowever, (* *) is still very important for informally andquickly commenting things out, also in inner syntax!Peter Original Message Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?From: Makarius To: isabelle-dev CC: Over the decades we have accumulated funny quotation forms in Isabellesyntax that are often hard to explain to new users (also to old users).In particular, what are the remaining uses of {* ... *}?It should already be superseded by cartouches. There is also "isabelleupdate_cartouches" to get rid of it (as well as `alt_string`).The long-term trend is to converge to cartouches or double-quotes almosteverywhere. Cartouches are for nested languages, and double quotes forstring literals or names that are in conflict with other syntax. Makarius___isabelle-dev mailing listisabelle-...@in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Remaining uses of {* ... *} quotation?
> On 8 Nov 2018, at 20:32, Makarius wrote:
>
> In particular, what are the remaining uses of {* ... *}?
I didn’t even know that existed.
But I use (*...*) to enclose arbitrary text or comment material out.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Remaining uses of {* ... *} quotation?
Over the decades we have accumulated funny quotation forms in Isabelle
syntax that are often hard to explain to new users (also to old users).
In particular, what are the remaining uses of {* ... *}?
It should already be superseded by cartouches. There is also "isabelle
update_cartouches" to get rid of it (as well as `alt_string`).
The long-term trend is to converge to cartouches or double-quotes almost
everywhere. Cartouches are for nested languages, and double quotes for
string literals or names that are in conflict with other syntax.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
This is the updated situation according to Isabelle/c1a27fce2076: *** System *** * Support for managed installations of Glasgow Haskell Compiler and OCaml via the following command-line tools: isabelle ghc_setup isabelle ghc_stack isabelle ocaml_setup isabelle ocaml_opam The global installation state is determined by the following settings (and corresponding directory contents): ISABELLE_STACK_ROOT ISABELLE_STACK_RESOLVER ISABELLE_GHC_VERSION ISABELLE_OPAM_ROOT ISABELLE_OCAML_VERSION After setup, the following Isabelle settings are automatically redirected (overriding existing user settings): ISABELLE_GHC ISABELLE_OCAML ISABELLE_OCAMLC The old meaning of these settings as locally installed executables may be recovered by purging the directories ISABELLE_STACK_ROOT / ISABELLE_OPAM_ROOT. I have also started experimenting with the following in $ISABELLE_HOME_USER/etc/settings: ISABELLE_STACK_ROOT="$HOME/.stack" ISABELLE_OPAM_ROOT="$HOME/.opam" The Isabelle scripts should ensure that the specified versions are used, independently of other versions that a user might have installed already. In any case, both "stack" and "opam" stack-up considerable material: it is easy to fill 5-15 GB of disk space after working some time. Only docker requires even more space. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
Makarius wrote: > On 08/11/2018 14:59, Bertram Felgenhauer wrote: > >> > >> 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. > > There is indeed some confusion here. > > My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained > by the odd recursive setup: in the stack situation, $ISABELLE_GHC points > to lib/Tools/ghc, and some mistake in the configuration could lead to > infinite recursion of sub-processes (potential bombing of the OS). > > It is probably better to leave the meaning of ISABELLE_GHC (and > ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle > ghc" tool entry points: these auxiliary scripts should go into > $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular > Isabelle tools. Sounds good to me. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
On 08/11/2018 14:59, Bertram Felgenhauer wrote: >> >> 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. There is indeed some confusion here. My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained by the odd recursive setup: in the stack situation, $ISABELLE_GHC points to lib/Tools/ghc, and some mistake in the configuration could lead to infinite recursion of sub-processes (potential bombing of the OS). It is probably better to leave the meaning of ISABELLE_GHC (and ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle ghc" tool entry points: these auxiliary scripts should go into $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular Isabelle tools. I have now also learned that "ghci" is just "ghc --interactive", so there is no point to treat it too prominently. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
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
Re: [isabelle-dev] NEWS: support for GHC
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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
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
Re: [isabelle-dev] NEWS: support for GHC
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? Cheers, Bertram diff -r 0a9688695a1b lib/Tools/ghc --- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghc -- "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" "$@" else echo "Cannot execute ghc: missing Isabelle GHC setup" >&2 exit 127 diff -r 0a9688695a1b lib/Tools/ghci --- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghci "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" --interactive "$@" else echo "Cannot execute ghci: missing Isabelle GHC setup" >&2 exit 127 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
