# HG changeset patch
# User wenzelm
# Date 1553290650 -3600
# Node ID 3544cca7920f3678fe2eaebda1a37521856cc24b
# Parent  77a92e8d5167af85a69f5909b8d4285b1010b847# Parent  385458b950e1022fb0837ea3443f8c8d98ac35ee
merged

diff -r 77a92e8d5167 -r 3544cca7920f Admin/components/bundled-windows
--- a/Admin/components/bundled-windows	Fri Mar 22 19:18:09 2019 +0000
+++ b/Admin/components/bundled-windows	Fri Mar 22 22:37:30 2019 +0100
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20190320
+cygwin-20190322
 windows_app-20181006
diff -r 77a92e8d5167 -r 3544cca7920f Admin/components/components.sha1
--- a/Admin/components/components.sha1	Fri Mar 22 19:18:09 2019 +0000
+++ b/Admin/components/components.sha1	Fri Mar 22 22:37:30 2019 +0100
@@ -48,6 +48,7 @@
 c22048912b010a5a0b4f2a3eb4d318d6953761e4  cygwin-20170930.tar.gz
 5a3919e665947b820fd7f57787280c7512be3782  cygwin-20180604.tar.gz
 2aa049170e8088de59bd70eed8220f552093932d  cygwin-20190320.tar.gz
+fb898e263fcf6f847d97f564fe49ea0760bb453f  cygwin-20190322.tar.gz
 0fe549949a025d65d52d6deca30554de8fca3b6e  e-1.5.tar.gz
 2e293256a134eb8e5b1a283361b15eb812fbfbf1  e-1.6-1.tar.gz
 e1919e72416cbd7ac8de5455caba8901acc7b44d  e-1.6-2.tar.gz
diff -r 77a92e8d5167 -r 3544cca7920f lib/Tools/ocaml_setup
--- a/lib/Tools/ocaml_setup	Fri Mar 22 19:18:09 2019 +0000
+++ b/lib/Tools/ocaml_setup	Fri Mar 22 22:37:30 2019 +0100
@@ -6,11 +6,14 @@
 
 set -e
 
-if [ -e "$ISABELLE_OPAM_ROOT/config" ]
+if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
 then
-  isabelle_opam switch reinstall -y "$ISABELLE_OCAML_VERSION"
+  isabelle_opam switch -y "$ISABELLE_OCAML_VERSION"
+elif [ -e "$ISABELLE_OPAM_ROOT/config" ]
+then
+  isabelle_opam switch create -y "$ISABELLE_OCAML_VERSION"
 else
   isabelle_opam init -y --disable-sandboxing --no-setup --compiler="$ISABELLE_OCAML_VERSION"
 fi
 
-isabelle_opam install zarith -y
+isabelle_opam install -y zarith
diff -r 77a92e8d5167 -r 3544cca7920f lib/scripts/ghc
--- a/lib/scripts/ghc	Fri Mar 22 19:18:09 2019 +0000
+++ b/lib/scripts/ghc	Fri Mar 22 22:37:30 2019 +0100
@@ -4,7 +4,8 @@
 #
 # Invoke ghc via "stack".
 
-if [ -e "$ISABELLE_STACK_ROOT/config.yaml" ]; then
+if [ -f "$ISABELLE_STACK_ROOT/ISABELLE_GHC_EXE-$ISABELLE_PLATFORM_FAMILY" ]
+then
   isabelle_stack ghc -- "$@"
 else
   echo "Cannot execute ghc: missing Isabelle GHC setup" >&2
diff -r 77a92e8d5167 -r 3544cca7920f lib/scripts/ocamlfind
--- a/lib/scripts/ocamlfind	Fri Mar 22 19:18:09 2019 +0000
+++ b/lib/scripts/ocamlfind	Fri Mar 22 22:37:30 2019 +0100
@@ -4,7 +4,7 @@
 #
 # Invoke ocamlfind via "opam".
 
-if [ -e "$ISABELLE_OPAM_ROOT/config" ]
+if [ -d "$ISABELLE_OPAM_ROOT/$ISABELLE_OCAML_VERSION/bin" ]
 then
   isabelle_opam config exec --switch "$ISABELLE_OCAML_VERSION" -- ocamlfind "$@"
 else
diff -r 77a92e8d5167 -r 3544cca7920f src/HOL/Library/code_test.ML
--- a/src/HOL/Library/code_test.ML	Fri Mar 22 19:18:09 2019 +0000
+++ b/src/HOL/Library/code_test.ML	Fri Mar 22 22:37:30 2019 +0100
@@ -467,9 +467,9 @@
 
     val compiled_path = Path.append path (Path.basic "test")
     val compile_cmd =
-      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg " ^
+      "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg" ^
       " -o " ^ File.bash_path compiled_path ^ " -I " ^ File.bash_path path ^ " " ^
-      File.bash_path code_path ^ " " ^ File.bash_path driver_path
+      File.bash_path code_path ^ " " ^ File.bash_path driver_path ^ " </dev/null"
 
     val run_cmd = File.bash_path compiled_path
   in
diff -r 77a92e8d5167 -r 3544cca7920f src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala	Fri Mar 22 19:18:09 2019 +0000
+++ b/src/Pure/Admin/build_cygwin.scala	Fri Mar 22 22:37:30 2019 +0100
@@ -12,7 +12,7 @@
   val default_mirror: String = "https://isabelle.sketis.net/cygwin_2019"
 
   val packages: List[String] =
-    List("curl", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
+    List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
 
   def build_cygwin(progress: Progress,
     mirror: String = default_mirror,
diff -r 77a92e8d5167 -r 3544cca7920f src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 22 19:18:09 2019 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Fri Mar 22 22:37:30 2019 +0100
@@ -261,7 +261,7 @@
       List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
         options = "-m32 -B -M1x2,2 -t Benchmarks" +
             " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
-            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true -e ISABELLE_SMLNJ=sml" +
+            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" +
             " -e ISABELLE_SWIPL=swipl",
           args = "-N -a -d '~~/src/Benchmarks'",
           detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
@@ -296,14 +296,14 @@
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
           options = "-m32 -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
-            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
+            " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
           args = "-a",
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
         Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
           options = "-m64 -M4" +
             " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
-            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
+            " -e ISABELLE_GHC_SETUP=true" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
           args = "-a",
           detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
@@ -315,7 +315,7 @@
           options = "-m32 -M1x2 -t AFP -P" + n +
             " -e ISABELLE_GHC=ghc" +
             " -e ISABELLE_MLTON=mlton" +
-            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
+            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
             " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml",
           args = "-N -X large -X slow",
           afp = true,
diff -r 77a92e8d5167 -r 3544cca7920f src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Fri Mar 22 19:18:09 2019 +0000
+++ b/src/Tools/Code/code_ml.ML	Fri Mar 22 22:37:30 2019 +0100
@@ -889,7 +889,7 @@
         make_destination = fn p => Path.append p (Path.explode "ROOT.ml")
           (*extension demanded by OCaml compiler*),
         make_command = fn _ =>
-          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml"},
+          "\"$ISABELLE_OCAMLFIND\" ocamlopt -w pu -package zarith -linkpkg ROOT.ml </dev/null"},
       evaluation_args = []})
   #> Code_Target.set_printings (Type_Constructor ("fun",
     [(target_SML, SOME (2, fun_syntax)), (target_OCaml, SOME (2, fun_syntax))]))