clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
authorwenzelm
Thu Nov 08 16:18:12 2018 +0100 (5 months ago)
changeset 69268c1a27fce2076
parent 69267 517655a528fe
child 69269 1bee990d443c
clarified tool setup for GHC / OCaml: discontinued "isabelle ghc", "isabelle ocaml", "isabelle ocamlc" to avoid confusion with traditional settings variables for executables (these are still required in existing applications, notably in session options [condition = ISABELLE_GHC] etc. and codegen setup;
NEWS
lib/Tools/ghc
lib/Tools/ghci
lib/Tools/ocaml
lib/Tools/ocamlc
lib/scripts/getsettings
lib/scripts/ghc
lib/scripts/ocaml
lib/scripts/ocamlc
     1.1 --- a/NEWS	Thu Nov 08 15:52:10 2018 +0100
     1.2 +++ b/NEWS	Thu Nov 08 16:18:12 2018 +0100
     1.3 @@ -124,17 +124,36 @@
     1.4  presence of structurally broken sources: full consolidation of theories
     1.5  is no longer required.
     1.6  
     1.7 -* Support for OCaml via command-line tools "isabelle ocaml_setup",
     1.8 -"isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing
     1.9 -settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained
    1.10 -dynamically according the state of ISABELLE_OPAM_ROOT and
    1.11 -ISABELLE_OCAML_VERSION.
    1.12 -
    1.13 -* Support for Glasgow Haskell Compiler via command-line tools "isabelle
    1.14 -ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
    1.15 -Existing settings variable ISABELLE_GHC is maintained dynamically
    1.16 -according to the state of ISABELLE_STACK_ROOT and
    1.17 -ISABELLE_STACK_RESOLVER.
    1.18 +* Support for managed installations of Glasgow Haskell Compiler and
    1.19 +OCaml via the following command-line tools:
    1.20 +
    1.21 +  isabelle ghc_setup
    1.22 +  isabelle ghc_stack
    1.23 +
    1.24 +  isabelle ocaml_setup
    1.25 +  isabelle ocaml_opam
    1.26 +
    1.27 +The global installation state is determined by the following settings
    1.28 +(and corresponding directory contents):
    1.29 +
    1.30 +  ISABELLE_STACK_ROOT
    1.31 +  ISABELLE_STACK_RESOLVER
    1.32 +  ISABELLE_GHC_VERSION
    1.33 +
    1.34 +  ISABELLE_OPAM_ROOT
    1.35 +  ISABELLE_OCAML_VERSION
    1.36 +
    1.37 +After setup, the following Isabelle settings are automatically
    1.38 +redirected (overriding existing user settings):
    1.39 +
    1.40 + ISABELLE_GHC
    1.41 +
    1.42 + ISABELLE_OCAML
    1.43 + ISABELLE_OCAMLC
    1.44 +
    1.45 +The old meaning of these settings as locally installed executables may
    1.46 +be recovered by purging the directories ISABELLE_STACK_ROOT /
    1.47 +ISABELLE_OPAM_ROOT.
    1.48  
    1.49  * Update to Java 11: the latest long-term support version of OpenJDK.
    1.50  
     2.1 --- a/lib/Tools/ghc	Thu Nov 08 15:52:10 2018 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,12 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Author: Makarius
     2.7 -#
     2.8 -# DESCRIPTION: invoke Glasgow Haskell Compiler within the Isabelle environment
     2.9 -
    2.10 -if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then
    2.11 -  isabelle_stack ghc -- "$@"
    2.12 -else
    2.13 -  echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
    2.14 -  exit 127
    2.15 -fi
     3.1 --- a/lib/Tools/ghci	Thu Nov 08 15:52:10 2018 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,7 +0,0 @@
     3.4 -#!/usr/bin/env bash
     3.5 -#
     3.6 -# Author: Makarius
     3.7 -#
     3.8 -# DESCRIPTION: invoke GHC interaction within the Isabelle environment
     3.9 -
    3.10 -isabelle ghc --interactive "$@"
     4.1 --- a/lib/Tools/ocaml	Thu Nov 08 15:52:10 2018 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,13 +0,0 @@
     4.4 -#!/usr/bin/env bash
     4.5 -#
     4.6 -# Author: Makarius
     4.7 -#
     4.8 -# DESCRIPTION: invoke OCaml within the Isabelle environment
     4.9 -
    4.10 -if [ -d "$ISABELLE_OPAM_ROOT" -a -n "$ISABELLE_OCAML" ]
    4.11 -then
    4.12 -  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
    4.13 -else
    4.14 -  echo "Cannot execute ocaml: missing Isabelle OCaml setup" >&2
    4.15 -  exit 127
    4.16 -fi
     5.1 --- a/lib/Tools/ocamlc	Thu Nov 08 15:52:10 2018 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,13 +0,0 @@
     5.4 -#!/usr/bin/env bash
     5.5 -#
     5.6 -# Author: Makarius
     5.7 -#
     5.8 -# DESCRIPTION: invoke OCaml compiler within the Isabelle environment
     5.9 -
    5.10 -if [ -d "$ISABELLE_OPAM_ROOT" -a -n "$ISABELLE_OCAMLC" ]
    5.11 -then
    5.12 -  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
    5.13 -else
    5.14 -  echo "Cannot execute ocamlc: missing Isabelle OCaml setup" >&2
    5.15 -  exit 127
    5.16 -fi
     6.1 --- a/lib/scripts/getsettings	Thu Nov 08 15:52:10 2018 +0100
     6.2 +++ b/lib/scripts/getsettings	Thu Nov 08 16:18:12 2018 +0100
     6.3 @@ -101,18 +101,18 @@
     6.4  
     6.5  #enforce ISABELLE_OCAML
     6.6  if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
     6.7 -  ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml"
     6.8 +  ISABELLE_OCAML="$ISABELLE_HOME/lib/scripts/ocaml"
     6.9  fi
    6.10  
    6.11  #enforce ISABELLE_OCAMLC
    6.12  if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
    6.13 -  ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
    6.14 +  ISABELLE_OCAMLC="$ISABELLE_HOME/lib/scripts/ocamlc"
    6.15  fi
    6.16  
    6.17  #enforce ISABELLE_GHC
    6.18  if [ -d "$ISABELLE_STACK_ROOT" -a -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS" ]; then
    6.19    if [ -f "$(cat "$ISABELLE_STACK_ROOT/ISABELLE_GHC_PROGRAMS")/$ISABELLE_GHC_VERSION/bin/ghc" ]; then
    6.20 -    ISABELLE_GHC="$ISABELLE_HOME/lib/Tools/ghc"
    6.21 +    ISABELLE_GHC="$ISABELLE_HOME/lib/scripts/ghc"
    6.22    fi
    6.23  fi
    6.24  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/lib/scripts/ghc	Thu Nov 08 16:18:12 2018 +0100
     7.3 @@ -0,0 +1,12 @@
     7.4 +#!/usr/bin/env bash
     7.5 +#
     7.6 +# Author: Makarius
     7.7 +#
     7.8 +# Invoke ghc via "stack".
     7.9 +
    7.10 +if [ -d "$ISABELLE_STACK_ROOT" ]; then
    7.11 +  isabelle_stack ghc -- "$@"
    7.12 +else
    7.13 +  echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
    7.14 +  exit 127
    7.15 +fi
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/lib/scripts/ocaml	Thu Nov 08 16:18:12 2018 +0100
     8.3 @@ -0,0 +1,13 @@
     8.4 +#!/usr/bin/env bash
     8.5 +#
     8.6 +# Author: Makarius
     8.7 +#
     8.8 +# Invoke ocaml via "opam".
     8.9 +
    8.10 +if [ -d "$ISABELLE_OPAM_ROOT" ]
    8.11 +then
    8.12 +  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
    8.13 +else
    8.14 +  echo "Cannot execute ocaml: missing Isabelle OCaml setup" >&2
    8.15 +  exit 127
    8.16 +fi
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/lib/scripts/ocamlc	Thu Nov 08 16:18:12 2018 +0100
     9.3 @@ -0,0 +1,13 @@
     9.4 +#!/usr/bin/env bash
     9.5 +#
     9.6 +# Author: Makarius
     9.7 +#
     9.8 +# Invoke ocamlc via "opam".
     9.9 +
    9.10 +if [ -d "$ISABELLE_OPAM_ROOT" ]
    9.11 +then
    9.12 +  isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
    9.13 +else
    9.14 +  echo "Cannot execute ocamlc: missing Isabelle OCaml setup" >&2
    9.15 +  exit 127
    9.16 +fi