support for OCaml via command-line tools;
authorwenzelm
Mon Oct 08 15:42:43 2018 +0200 (13 months ago ago)
changeset 69135be20f5f6feb9
parent 69134 a142ec271d83
child 69136 90fce429e1bc
child 69137 d4baf535f845
support for OCaml via command-line tools;
NEWS
etc/settings
lib/Tools/ocaml
lib/Tools/ocaml_opam
lib/Tools/ocaml_setup
lib/Tools/ocamlc
lib/scripts/getsettings
     1.1 --- a/NEWS	Mon Oct 08 12:52:28 2018 +0200
     1.2 +++ b/NEWS	Mon Oct 08 15:42:43 2018 +0200
     1.3 @@ -25,7 +25,6 @@
     1.4  (legacy feature since Isabelle2016).
     1.5  
     1.6  
     1.7 -
     1.8  *** HOL ***
     1.9  
    1.10  * Simplified syntax setup for big operators under image. In rare
    1.11 @@ -90,6 +89,12 @@
    1.12  presence of structurally broken sources: full consolidation of theories
    1.13  is no longer required.
    1.14  
    1.15 +* Support for OCaml via command-line tools "isabelle ocaml_setup",
    1.16 +"isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing
    1.17 +settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained
    1.18 +dynamically according the state of ISABELLE_OPAM_ROOT concerning
    1.19 +ISABELLE_OCAML_VERSION.
    1.20 +
    1.21  
    1.22  
    1.23  New in Isabelle2018 (August 2018)
     2.1 --- a/etc/settings	Mon Oct 08 12:52:28 2018 +0200
     2.2 +++ b/etc/settings	Mon Oct 08 15:42:43 2018 +0200
     2.3 @@ -138,6 +138,8 @@
     2.4  
     2.5  ISABELLE_OPAM_ROOT="$ISABELLE_HOME_USER/opam"
     2.6  
     2.7 +ISABELLE_OCAML_VERSION="4.05.0"
     2.8 +
     2.9  
    2.10  ###
    2.11  ### Misc settings
    2.12 @@ -147,7 +149,5 @@
    2.13  
    2.14  #ISABELLE_GHC="/usr/bin/ghc"
    2.15  #ISABELLE_MLTON="/usr/bin/mlton"
    2.16 -#ISABELLE_OCAML="/usr/bin/ocaml"
    2.17 -#ISABELLE_OCAMLC="/usr/bin/ocamlc"
    2.18  #ISABELLE_SMLNJ="/usr/bin/sml"
    2.19  #ISABELLE_SWIPL="/usr/bin/swipl"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/lib/Tools/ocaml	Mon Oct 08 15:42:43 2018 +0200
     3.3 @@ -0,0 +1,7 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# Author: Makarius
     3.7 +#
     3.8 +# DESCRIPTION: invoke OCaml within the Isabelle environment
     3.9 +
    3.10 +isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocaml "$@"
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/lib/Tools/ocaml_opam	Mon Oct 08 15:42:43 2018 +0200
     4.3 @@ -0,0 +1,7 @@
     4.4 +#!/usr/bin/env bash
     4.5 +#
     4.6 +# Author: Makarius
     4.7 +#
     4.8 +# DESCRIPTION: invoke OCaml Package Manager within the Isabelle environment
     4.9 +
    4.10 +isabelle_opam "$@"
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/lib/Tools/ocaml_setup	Mon Oct 08 15:42:43 2018 +0200
     5.3 @@ -0,0 +1,7 @@
     5.4 +#!/usr/bin/env bash
     5.5 +#
     5.6 +# Author: Makarius
     5.7 +#
     5.8 +# DESCRIPTION: OCaml setup via OPAM
     5.9 +
    5.10 +isabelle_opam init --no-setup --compiler="$ISABELLE_OCAML_VERSION" "$@"
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/lib/Tools/ocamlc	Mon Oct 08 15:42:43 2018 +0200
     6.3 @@ -0,0 +1,7 @@
     6.4 +#!/usr/bin/env bash
     6.5 +#
     6.6 +# Author: Makarius
     6.7 +#
     6.8 +# DESCRIPTION: invoke OCaml compiler within the Isabelle environment
     6.9 +
    6.10 +isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlc "$@"
     7.1 --- a/lib/scripts/getsettings	Mon Oct 08 12:52:28 2018 +0200
     7.2 +++ b/lib/scripts/getsettings	Mon Oct 08 15:42:43 2018 +0200
     7.3 @@ -99,6 +99,14 @@
     7.4    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
     7.5  fi
     7.6  
     7.7 +#OCaml
     7.8 +if [ -z "$ISABELLE_OCAML" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
     7.9 +  ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml"
    7.10 +fi
    7.11 +if [ -z "$ISABELLE_OCAMLC" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
    7.12 +  ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
    7.13 +fi
    7.14 +
    7.15  #enforce JAVA_HOME
    7.16  if [ -d "$ISABELLE_JDK_HOME/jre" ]
    7.17  then