merged
authorwenzelm
Wed Oct 17 22:00:02 2018 +0200 (14 months ago ago)
changeset 691549d70340b565c
parent 69145 806be481aa57
parent 69153 108beabc1bc6
child 69155 12ff5e476752
merged
     1.1 --- a/Admin/components/components.sha1	Wed Oct 17 21:00:53 2018 +0200
     1.2 +++ b/Admin/components/components.sha1	Wed Oct 17 22:00:02 2018 +0200
     1.3 @@ -4,6 +4,7 @@
     1.4  97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
     1.5  9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
     1.6  a65ce644b6094d41e9f991ef851cf05eff5dd0a9  bib2xhtml-20171221.tar.gz
     1.7 +f92cff635dfba5d4d77f469307369226c868542c  cakeml-2.0.tar.gz
     1.8  e7ffe4238b61a3c1ee87aca4421e7a612e09b836  ci-extras-1.tar.gz
     1.9  70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
    1.10  2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
    1.11 @@ -189,6 +190,7 @@
    1.12  53123dc011b2d4b4e8fe307f3c9fa355718ad01a  postgresql-42.1.1.tar.gz
    1.13  3a5d31377ec07a5069957f5477a4848cfc89a594  postgresql-42.1.4.tar.gz
    1.14  e7cd5c7955e9eb5ce8cd07feb97230b23d2eec40  postgresql-42.2.2.tar.gz
    1.15 +231b33c9c3c27d47e3ba01b399103d70509e0731  postgresql-42.2.5.tar.gz
    1.16  f132329ca1045858ef456cc08b197c9eeea6881b  postgresql-9.4.1212.tar.gz
    1.17  8ee375cfc38972f080dbc78f07b68dac03efe968  ProofGeneral-3.7.1.1.tar.gz
    1.18  847b52c0676b5eb0fbf0476f64fc08c2d72afd0c  ProofGeneral-4.1.tar.gz
    1.19 @@ -226,6 +228,7 @@
    1.20  27aeac6a91353d69f0438837798ac4ae6f9ff8c5  sqlite-jdbc-3.23.1.tar.gz
    1.21  8d20968603f45a2c640081df1ace6a8b0527452a  sqlite-jdbc-3.8.11.2.tar.gz
    1.22  2369f06e8d095f9ba26df938b1a96000e535afff  ssh-java-20161009.tar.gz
    1.23 +fdc415284e031ee3eb2f65828cbc6945736fe995  stack-1.9.1.tar.gz
    1.24  1f4a2053cc1f34fa36c4d9d2ac906ad4ebc863fd  sumatra_pdf-2.1.1.tar.gz
    1.25  601e08d048d8e50b0729429c8928b667d9b6bde9  sumatra_pdf-2.3.2.tar.gz
    1.26  14d46c2eb1a34821703da59d543433f581e91df3  sumatra_pdf-2.4.tar.gz
     2.1 --- a/Admin/components/main	Wed Oct 17 21:00:53 2018 +0200
     2.2 +++ b/Admin/components/main	Wed Oct 17 22:00:02 2018 +0200
     2.3 @@ -16,9 +16,10 @@
     2.4  postgresql-42.2.5
     2.5  scala-2.12.7
     2.6  smbc-0.4.1
     2.7 -ssh-java-20161009
     2.8  spass-3.8ds-1
     2.9  sqlite-jdbc-3.23.1
    2.10 +ssh-java-20161009
    2.11 +stack-1.9.1
    2.12  vampire-4.2.2
    2.13  xz-java-1.8
    2.14  z3-4.4.0pre-2
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/Admin/haskell/stack/README	Wed Oct 17 22:00:02 2018 +0200
     3.3 @@ -0,0 +1,12 @@
     3.4 +This is stack 1.9.1 -- the Haskell Tool Stack.
     3.5 +
     3.6 +See also https://www.haskellstack.org and executables from
     3.7 +https://github.com/commercialhaskell/stack/releases as follows:
     3.8 +
     3.9 +  * x86_64-linux: stack-1.9.1-linux-x86_64-static.tar.gz
    3.10 +  * x86_64-darwin: stack-1.9.1-osx-x86_64.tar.gz
    3.11 +  * x86_64-windows: stack-1.9.1-windows-x86_64.tar.gz
    3.12 +
    3.13 +
    3.14 +    Makarius
    3.15 +    17-Oct-2018
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/Admin/haskell/stack/settings	Wed Oct 17 22:00:02 2018 +0200
     4.3 @@ -0,0 +1,3 @@
     4.4 +# -*- shell-script -*- :mode=shellscript:
     4.5 +
     4.6 +ISABELLE_STACK="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/stack"
     5.1 --- a/NEWS	Wed Oct 17 21:00:53 2018 +0200
     5.2 +++ b/NEWS	Wed Oct 17 22:00:02 2018 +0200
     5.3 @@ -95,6 +95,11 @@
     5.4  dynamically according the state of ISABELLE_OPAM_ROOT concerning
     5.5  ISABELLE_OCAML_VERSION.
     5.6  
     5.7 +* Support for Glasgow Haskell Compiler via command-line tools "isabelle
     5.8 +ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack".
     5.9 +Existing settings variable ISABELLE_GHC is maintained dynamically
    5.10 +according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER.
    5.11 +
    5.12  
    5.13  
    5.14  New in Isabelle2018 (August 2018)
     6.1 --- a/etc/settings	Wed Oct 17 21:00:53 2018 +0200
     6.2 +++ b/etc/settings	Wed Oct 17 22:00:02 2018 +0200
     6.3 @@ -142,12 +142,22 @@
     6.4  
     6.5  
     6.6  ###
     6.7 +### Haskell
     6.8 +###
     6.9 +
    6.10 +ISABELLE_STACK_ROOT="$ISABELLE_HOME_USER/stack"
    6.11 +
    6.12 +ISABELLE_STACK_RESOLVER="lts-12.13"
    6.13 +
    6.14 +ISABELLE_GHC_VERSION="ghc-8.4.3"
    6.15 +
    6.16 +
    6.17 +###
    6.18  ### Misc settings
    6.19  ###
    6.20  
    6.21  ISABELLE_GNUPLOT="gnuplot"
    6.22  
    6.23 -#ISABELLE_GHC="/usr/bin/ghc"
    6.24  #ISABELLE_MLTON="/usr/bin/mlton"
    6.25  #ISABELLE_SMLNJ="/usr/bin/sml"
    6.26  #ISABELLE_SWIPL="/usr/bin/swipl"
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/lib/Tools/ghc	Wed Oct 17 22:00:02 2018 +0200
     7.3 @@ -0,0 +1,7 @@
     7.4 +#!/usr/bin/env bash
     7.5 +#
     7.6 +# Author: Makarius
     7.7 +#
     7.8 +# DESCRIPTION: invoke Glasgow Haskell Compiler within the Isabelle environment
     7.9 +
    7.10 +isabelle_stack ghc -- "$@"
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/lib/Tools/ghc_setup	Wed Oct 17 22:00:02 2018 +0200
     8.3 @@ -0,0 +1,8 @@
     8.4 +#!/usr/bin/env bash
     8.5 +#
     8.6 +# Author: Makarius
     8.7 +#
     8.8 +# DESCRIPTION: setup Glasgow Haskell Compiler setup via Stack
     8.9 +
    8.10 +isabelle_stack setup --resolver "$ISABELLE_STACK_RESOLVER" &&
    8.11 +  isabelle_stack ghci --ghci-options --version
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/lib/Tools/ghc_stack	Wed Oct 17 22:00:02 2018 +0200
     9.3 @@ -0,0 +1,7 @@
     9.4 +#!/usr/bin/env bash
     9.5 +#
     9.6 +# Author: Makarius
     9.7 +#
     9.8 +# DESCRIPTION: invoke Haskell Tool Stack within the Isabelle environment
     9.9 +
    9.10 +isabelle_stack "$@"
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/lib/Tools/ghci	Wed Oct 17 22:00:02 2018 +0200
    10.3 @@ -0,0 +1,7 @@
    10.4 +#!/usr/bin/env bash
    10.5 +#
    10.6 +# Author: Makarius
    10.7 +#
    10.8 +# DESCRIPTION: invoke GHC interaction within the Isabelle environment
    10.9 +
   10.10 +isabelle_stack ghci "$@"
    11.1 --- a/lib/Tools/ocaml_setup	Wed Oct 17 21:00:53 2018 +0200
    11.2 +++ b/lib/Tools/ocaml_setup	Wed Oct 17 22:00:02 2018 +0200
    11.3 @@ -2,7 +2,7 @@
    11.4  #
    11.5  # Author: Makarius
    11.6  #
    11.7 -# DESCRIPTION: OCaml setup via OPAM
    11.8 +# DESCRIPTION: setup OCaml setup via OPAM
    11.9  
   11.10  if [ -d "$ISABELLE_OPAM_ROOT" ]
   11.11  then
    12.1 --- a/lib/scripts/getfunctions	Wed Oct 17 21:00:53 2018 +0200
    12.2 +++ b/lib/scripts/getfunctions	Wed Oct 17 22:00:02 2018 +0200
    12.3 @@ -37,6 +37,18 @@
    12.4  }
    12.5  export -f isabelle_opam
    12.6  
    12.7 +#GHC management via Stack
    12.8 +function isabelle_stack()
    12.9 +{
   12.10 +  if [ -z "$ISABELLE_STACK" ]; then
   12.11 +    echo "Unknown ISABELLE_STACK -- GHC management tools unavailable" >&2
   12.12 +    return 127
   12.13 +  else
   12.14 +    env STACK_ROOT="$(platform_path "$ISABELLE_STACK_ROOT")" "$ISABELLE_STACK" "$@"
   12.15 +  fi
   12.16 +}
   12.17 +export -f isabelle_stack
   12.18 +
   12.19  #robust invocation via ISABELLE_JDK_HOME
   12.20  function isabelle_jdk ()
   12.21  {
    13.1 --- a/lib/scripts/getsettings	Wed Oct 17 21:00:53 2018 +0200
    13.2 +++ b/lib/scripts/getsettings	Wed Oct 17 22:00:02 2018 +0200
    13.3 @@ -99,14 +99,23 @@
    13.4    ML_IDENTIFIER="${ML_SYSTEM}_${ML_PLATFORM}"
    13.5  fi
    13.6  
    13.7 -#OCaml
    13.8 -if [ -z "$ISABELLE_OCAML" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
    13.9 +#enforce ISABELLE_OCAML
   13.10 +if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocaml" ]; then
   13.11    ISABELLE_OCAML="$ISABELLE_HOME/lib/Tools/ocaml"
   13.12  fi
   13.13 -if [ -z "$ISABELLE_OCAMLC" -a -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
   13.14 +
   13.15 +#enforce ISABELLE_OCAMLC
   13.16 +if [ -f "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin/ocamlc" ]; then
   13.17    ISABELLE_OCAMLC="$ISABELLE_HOME/lib/Tools/ocamlc"
   13.18  fi
   13.19  
   13.20 +#enforce ISABELLE_GHC
   13.21 +if [ -d "$ISABELLE_STACK_ROOT" ]; then
   13.22 +  if [ -f "$(isabelle_stack path --programs)/$ISABELLE_GHC_VERSION/ghc" ]; then
   13.23 +    ISABELLE_GHC="$ISABELLE_HOME/lib/Tools/ghc"
   13.24 +  fi
   13.25 +fi
   13.26 +
   13.27  #enforce JAVA_HOME
   13.28  if [ -d "$ISABELLE_JDK_HOME/jre" ]
   13.29  then