From 1da90e3c1842463f2c64939d800d7c39a0c75f4b Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Tue, 16 Jul 2019 17:44:03 +0200
Subject: Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)

---
 dev/build/windows/MakeCoq_MinGW.bat              |   2 +
 dev/build/windows/makecoq_mingw.sh               | 107 ++++++++++++++++++++++-
 dev/build/windows/patches_coq/flocq.patch        |  27 ++++++
 dev/build/windows/patches_coq/gappa_plugin.patch |  52 +++++++++++
 dev/build/windows/patches_coq/gappa_tool.patch   |  49 +++++++++++
 dev/build/windows/patches_coq/interval.patch     |  38 ++++++++
 dev/ci/ci-basic-overlay.sh                       |  21 +++++
 7 files changed, 294 insertions(+), 2 deletions(-)
 create mode 100755 dev/build/windows/patches_coq/flocq.patch
 create mode 100755 dev/build/windows/patches_coq/gappa_plugin.patch
 create mode 100755 dev/build/windows/patches_coq/gappa_tool.patch
 create mode 100755 dev/build/windows/patches_coq/interval.patch

(limited to 'dev')

diff --git a/dev/build/windows/MakeCoq_MinGW.bat b/dev/build/windows/MakeCoq_MinGW.bat
index 78ca5e830a..c75acb0560 100755
--- a/dev/build/windows/MakeCoq_MinGW.bat
+++ b/dev/build/windows/MakeCoq_MinGW.bat
@@ -381,6 +381,7 @@ IF "%RUNSETUP%"=="Y" (
     -P pkg-config ^
     -P mingw64-%ARCH%-binutils,mingw64-%ARCH%-gcc-core,mingw64-%ARCH%-gcc-g++,mingw64-%ARCH%-windows_default_manifest ^
     -P mingw64-%ARCH%-headers,mingw64-%ARCH%-runtime,mingw64-%ARCH%-pthreads,mingw64-%ARCH%-zlib ^
+    -P mingw64-%ARCH%-gmp,mingw64-%ARCH%-mpfr ^
     -P adwaita-icon-theme ^
     -P libiconv-devel,libunistring-devel,libncurses-devel ^
     -P gettext-devel,libgettextpo-devel ^
@@ -389,6 +390,7 @@ IF "%RUNSETUP%"=="Y" (
     -P gtk-update-icon-cache ^
     -P libtool,automake ^
     -P intltool ^
+    -P bison,flex ^
     %EXTRAPACKAGES% ^
     || GOTO ErrorExit
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 0699e2bd44..98a5fd0a12 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1146,7 +1146,8 @@ function make_menhir {
   make_ocaml
   make_findlib
   make_ocamlbuild
-  if build_prep http://gallium.inria.fr/~fpottier/menhir menhir-20180530 tar.gz 1 ; then
+  # This is the version required by latest CompCert
+  if build_prep https://gitlab.inria.fr/fpottier/menhir/-/archive/20190626 menhir-20190626 tar.gz 1 ; then
     # Note: menhir doesn't support -j 8, so don't pass MAKE_OPT
     log2 make all PREFIX="$PREFIXOCAML"
     log2 make install PREFIX="$PREFIXOCAML"
@@ -1154,6 +1155,29 @@ function make_menhir {
   fi
 }
 
+##### CAMLP5 Ocaml Preprocessor #####
+
+function make_camlp5 {
+  make_ocaml
+  make_findlib
+
+  if build_prep https://github.com/camlp5/camlp5/archive rel707 tar.gz 1 camlp5-rel707; then
+    logn configure ./configure
+    # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
+    sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
+    # shellcheck disable=SC2086
+    log1 make world.opt $MAKE_OPT
+    log2 make install
+    log2 make clean
+    # For some reason META is not built / copied, but it is required
+    log2 make -C etc META
+    mkdir -p "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+    cp etc/META "$PREFIXOCAML/libocaml/site-lib/camlp5/"
+    log2 make clean
+    build_post
+  fi
+}
+
 ##### LABLGTK Ocaml GTK binding #####
 
 # Note: when rebuilding lablgtk by deleting the .finished file,
@@ -1805,8 +1829,9 @@ function make_addon_coquelicot {
   installer_addon_dependency_beg coquelicot
   make_addon_ssreflect
   installer_addon_dependency_end
-  if build_prep_overlay Coquelicot; then
+  if build_prep_overlay coquelicot; then
     installer_addon_section coquelicot "Coquelicot" "Coq library for real analysis" ""
+    logn autogen ./autogen.sh
     logn configure ./configure --libdir="$PREFIXCOQ/lib/coq/user-contrib/Coquelicot"
     logn remake ./remake
     logn remake-install ./remake install
@@ -1867,6 +1892,84 @@ function make_addon_quickchick {
   fi
 }
 
+# Flocq: Floating point library
+
+function make_addon_flocq {
+  if build_prep_overlay Flocq; then
+    installer_addon_section flocq "Flocq" "Coq library for floating point arithmetic" ""
+    logn autogen ./autogen.sh
+    logn configure ./configure
+    logn remake ./remake --jobs=$MAKE_THREADS
+    logn install ./remake install
+    build_post
+  fi
+}
+
+# Coq-Interval: interval arithmetic and inequality proofs
+
+function make_addon_interval {
+  installer_addon_dependency_beg interval
+  make_addon_mathcomp
+  make_addon_coquelicot
+  make_addon_bignums
+  make_addon_flocq
+  installer_addon_dependency_end
+  if build_prep_overlay interval; then
+    installer_addon_section interval "Interval" "Coq library and tactic for proving real inequalities" ""
+    logn autogen ./autogen.sh
+    logn configure ./configure
+    logn remake ./remake --jobs=$MAKE_THREADS
+    logn install ./remake install
+    build_post
+  fi
+}
+
+# Gappa: Automatic generation of arithmetic proofs (mostly on limited precision arithmetic)
+
+function install_boost {
+  # The extra tar parameter extracts only the boost headers, not the boost library source code (which is huge and takes a long time)
+  if build_prep https://dl.bintray.com/boostorg/release/1.69.0/source boost_1_69_0 tar.gz 1 boost_1_69_0 boost boost_1_69_0/boost; then
+    # Move extracted boost folder where mingw-gcc can find it
+    mv boost /usr/$TARGET_ARCH/sys-root/mingw/include
+    build_post
+  fi
+}
+
+function copy_gappa_dlls {
+  copy_coq_dll LIBGMP-10.DLL
+  copy_coq_dll LIBMPFR-6.DLL
+  copy_coq_dll LIBSTDC++-6.DLL
+}
+
+function make_addon_gappa_tool {
+  install_boost
+  if build_prep_overlay gappa_tool; then
+    installer_addon_section gappa_tool "Gappa tool" "Stand alone tool for automated generation of numerical arithmetic proofs" ""
+    logn autogen ./autogen.sh
+    logn configure ./configure --build="$HOST" --host="$HOST" --target="$TARGET" --prefix="$PREFIXCOQ"
+    logn remake ./remake --jobs=$MAKE_THREADS
+    logn install ./remake -d install
+    log1 copy_gappa_dlls
+    build_post
+  fi
+}
+
+function make_addon_gappa {
+  make_camlp5
+  installer_addon_dependency_beg gappa
+  make_addon_gappa_tool
+  make_addon_flocq
+  installer_addon_dependency_end
+  if build_prep_overlay gappa_plugin ; then
+    installer_addon_section gappa "Gappa plugin" "Coq plugin for the Gappa tool" ""
+    logn autogen ./autogen.sh
+    logn configure ./configure
+    logn remake ./remake
+    logn install ./remake install
+    build_post
+  fi
+}
+
 # Main function for building addons
 
 function make_addons {
diff --git a/dev/build/windows/patches_coq/flocq.patch b/dev/build/windows/patches_coq/flocq.patch
new file mode 100755
index 0000000000..33d909f47b
--- /dev/null
+++ b/dev/build/windows/patches_coq/flocq.patch
@@ -0,0 +1,27 @@
+diff/patch file created on Sun, Jan 20, 2019 11:55:04 AM with:
+difftar-folder.sh tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e 1
+TARFILE= tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz
+FOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e
+TARSTRIP= 1
+TARPREFIX= flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/
+ORIGFOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig
+--- Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig/configure.in	2019-01-11 15:52:30.000000000 +0100
++++ Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/configure.in	2019-01-20 11:51:49.474668300 +0100
+@@ -10,7 +10,7 @@
+ 
+ m4_divert_push([HELP_ENABLE])
+ Fine tuning of the installation directory:
+-AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@])
++AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq@:>@])
+ m4_divert_pop([HELP_ENABLE])
+ 
+ AC_PROG_CXX
+@@ -51,7 +51,7 @@
+ AC_MSG_RESULT([$COQDOC])
+ 
+ if test "$libdir" = '${exec_prefix}/lib'; then
+-  libdir="`$COQC -where`/user-contrib/Flocq"
++  libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq"
+ fi
+ 
+ AC_MSG_NOTICE([building remake...])
diff --git a/dev/build/windows/patches_coq/gappa_plugin.patch b/dev/build/windows/patches_coq/gappa_plugin.patch
new file mode 100755
index 0000000000..8bd32318d7
--- /dev/null
+++ b/dev/build/windows/patches_coq/gappa_plugin.patch
@@ -0,0 +1,52 @@
+diff/patch file created on Sat, Jun 29, 2019  9:53:06 PM with:
+difftar-folder.sh tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e 1
+TARFILE= tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz
+FOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e
+TARSTRIP= 1
+TARPREFIX= coq-04d859ea9a496f84569c3f9b8cb66784cd82313e/
+ORIGFOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig
+--- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/Remakefile.in	2019-04-09 16:57:15.000000000 +0200
++++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/Remakefile.in	2019-06-29 21:40:03.902985100 +0200
+@@ -43,7 +43,7 @@
+ 	@COQC@ -R src Gappa -I src $<
+ 
+ COQSUBTREES = clib engine kernel interp intf lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac
+-COQINCLUDES = $(addprefix -I @COQLIB@/, $(COQSUBTREES))
++COQINCLUDES = $(addprefix -I "@COQLIB@"/, $(COQSUBTREES))
+ 
+ src/gappatac.cmo: src/gappatac.ml
+ 	@OCAMLC@ -pp "@CAMLP4O@ pa_macro.cmo -D@COQDEFINE@" -rectypes $(COQINCLUDES) -c $< -o $@
+--- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/configure.in	2019-04-09 16:57:15.000000000 +0200
++++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/configure.in	2019-06-29 21:47:31.294322200 +0200
+@@ -53,7 +53,17 @@
+   if test ! "$CAMLP4O"; then
+     CAMLP4O=camlp5o
+   fi
+-  CAMLP4O=`which $CAMLP4O`
++  case `uname -s` in
++    CYGWIN*)
++      case "$CAMLP4O" in
++        *:*) CAMLP4O=`cygpath -m "$CAMLP4O"` ;;
++        *)   CAMLP4O=`cygpath -u "$CAMLP4O"` ;;
++      esac
++      ;;
++    *)
++      CAMLP4O=`which $CAMLP4O`
++      ;;
++  esac
+ fi
+ AC_MSG_RESULT([$CAMLP4O])
+ 
+@@ -81,10 +91,10 @@
+ rm -f conftest.v conftest.vo conftest.err
+ 
+ AC_SUBST(OCAMLLIB)
+-OCAMLLIB=`$OCAMLC -where`
++OCAMLLIB=`$OCAMLC -where | tr -d '\r' | tr '\\' '/'`
+ 
+ AC_SUBST(COQLIB)
+-COQLIB=`$COQC -where`
++COQLIB=`$COQC -where | tr -d '\r' | tr '\\' '/'`
+ 
+ if test "$libdir" = '${exec_prefix}/lib'; then
+   libdir="$COQLIB/user-contrib/Gappa"
diff --git a/dev/build/windows/patches_coq/gappa_tool.patch b/dev/build/windows/patches_coq/gappa_tool.patch
new file mode 100755
index 0000000000..d76b4080b7
--- /dev/null
+++ b/dev/build/windows/patches_coq/gappa_tool.patch
@@ -0,0 +1,49 @@
+diff/patch file created on Sat, Jun 29, 2019  9:58:22 PM with:
+difftar-folder.sh tarballs/gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.tar.gz gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608 1
+TARFILE= tarballs/gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.tar.gz
+FOLDER= gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608
+TARSTRIP= 1
+TARPREFIX= gappa-f53e105cd73484fc76eb58ba24ead73be502c608/
+ORIGFOLDER= gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig
+--- gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig/src/proofs/property.cpp	2019-06-17 09:39:04.000000000 +0200
++++ gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608/src/proofs/property.cpp	2019-06-29 19:05:47.321916200 +0200
+@@ -48,7 +48,7 @@
+   new(&store) interval(i);
+ }
+ 
+-property::property(predicated_real const &r, long i): real(r)
++property::property(predicated_real const &r, intptr_t i): real(r)
+ {
+   assert(r.pred_cst());
+   store._int = i;
+--- gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig/src/proofs/property.hpp	2019-06-17 09:39:04.000000000 +0200
++++ gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608/src/proofs/property.hpp	2019-06-29 19:05:47.305946500 +0200
+@@ -55,7 +55,7 @@
+ class property {
+   union store_t {
+     char _bnd[sizeof(interval)];
+-    long _int;
++    intptr_t _int;
+   };
+   store_t store;
+   interval       &_bnd()       { return *reinterpret_cast< interval       * >(&store); }
+@@ -66,16 +66,16 @@
+   { assert(real.pred_bnd()); return _bnd(); }
+   interval const &bnd() const
+   { assert(real.pred_bnd()); return _bnd(); }
+-  long &cst()
++  intptr_t &cst()
+   { assert(real.pred_cst()); return store._int; }
+-  long const &cst() const
++  intptr_t const &cst() const
+   { assert(real.pred_cst()); return store._int; }
+   property();
+   property(ast_real const *);
+   property(ast_real const *, interval const &);
+   property(predicated_real const &);
+   property(predicated_real const &, interval const &);
+-  property(predicated_real const &, long);
++  property(predicated_real const &, intptr_t);
+   property(property const &);
+   property &operator=(property const &);
+   ~property();
diff --git a/dev/build/windows/patches_coq/interval.patch b/dev/build/windows/patches_coq/interval.patch
new file mode 100755
index 0000000000..46b2b97826
--- /dev/null
+++ b/dev/build/windows/patches_coq/interval.patch
@@ -0,0 +1,38 @@
+diff/patch file created on Sat, Jun 29, 2019  6:44:56 PM with:
+difftar-folder.sh tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628 1
+TARFILE= tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz
+FOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628
+TARSTRIP= 1
+TARPREFIX= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/
+ORIGFOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig
+--- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/configure.in	2019-04-09 17:31:18.000000000 +0200
++++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/configure.in	2019-06-29 18:39:41.889749600 +0200
+@@ -10,7 +10,7 @@
+ 
+ m4_divert_push([HELP_ENABLE])
+ Fine tuning of the installation directory:
+-AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@])
++AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval@:>@])
+ m4_divert_pop([HELP_ENABLE])
+ 
+ AC_PROG_CXX
+@@ -79,7 +79,7 @@
+ rm -f conftest.v conftest.vo conftest.err
+ 
+ if test "$libdir" = '${exec_prefix}/lib'; then
+-  libdir="`$COQC -where`/user-contrib/Interval"
++  libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval"
+ fi
+ 
+ AC_MSG_NOTICE([building remake...])
+--- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/src/Interval_missing.v	2019-04-09 17:31:18.000000000 +0200
++++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/src/Interval_missing.v	2019-06-29 18:40:57.572496200 +0200
+@@ -1259,7 +1259,7 @@
+ intros Heq Hb Hd.
+ apply (Rmult_eq_reg_r (b * d)).
+ field_simplify; trivial.
+-now rewrite Heq.
++try rewrite Heq.
+ now apply Rmult_neq0.
+ Qed.
+ 
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index fa39b41565..dadb2bb8f1 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -101,6 +101,27 @@
 : "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}"
 : "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}"
 
+########################################################################
+# Coq-interval
+########################################################################
+: "${interval_CI_REF:=master}"
+: "${interval_CI_GITURL:=https://gitlab.inria.fr/coqinterval/interval}"
+: "${interval_CI_ARCHIVEURL:=${interval_CI_GITURL}/-/archive}"
+
+########################################################################
+# Gappa stand alone tool
+########################################################################
+: "${gappa_tool_CI_REF:=master}"
+: "${gappa_tool_CI_GITURL:=https://gitlab.inria.fr/gappa/gappa}"
+: "${gappa_tool_CI_ARCHIVEURL:=${gappa_tool_CI_GITURL}/-/archive}"
+
+########################################################################
+# Gappa plugin
+########################################################################
+: "${gappa_plugin_CI_REF:=master}"
+: "${gappa_plugin_CI_GITURL:=https://gitlab.inria.fr/gappa/coq}"
+: "${gappa_plugin_CI_ARCHIVEURL:=${gappa_plugin_CI_GITURL}/-/archive}"
+
 ########################################################################
 # CompCert
 ########################################################################
-- 
cgit v1.2.3


From c3d3f2123a341c974c2f33dad3a53c653ce0f50b Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Tue, 16 Jul 2019 18:18:35 +0200
Subject: Enable Coquelicot, Flocq, Interval and Gappa in extended/release
 Windows builds

---
 dev/ci/gitlab.bat | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 6c4ccfc14d..3998fc6514 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -48,9 +48,13 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=compcert ^
     -addon=extlib ^
     -addon=quickchick ^
+    -addon=coquelicot ^
     -addon=vst ^
-    -addon=aactactics
-REM -addon=coquelicot ^
+    -addon=aactactics ^
+    -addon=flocq ^
+    -addon=interval ^
+    -addon=gappa_tool ^
+    -addon=gappa
 ) ELSE (
   SET "EXTRA_ADDONS= "
 )
-- 
cgit v1.2.3


From 72d93ff7ea837b2d70dfff0ef3fe90749609e1be Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Tue, 16 Jul 2019 20:12:00 +0200
Subject: Removed patch for Gappa tool (verified that changes in gappa master
 fixed the windows crash)

---
 dev/build/windows/patches_coq/gappa_tool.patch | 49 --------------------------
 1 file changed, 49 deletions(-)
 delete mode 100755 dev/build/windows/patches_coq/gappa_tool.patch

(limited to 'dev')

diff --git a/dev/build/windows/patches_coq/gappa_tool.patch b/dev/build/windows/patches_coq/gappa_tool.patch
deleted file mode 100755
index d76b4080b7..0000000000
--- a/dev/build/windows/patches_coq/gappa_tool.patch
+++ /dev/null
@@ -1,49 +0,0 @@
-diff/patch file created on Sat, Jun 29, 2019  9:58:22 PM with:
-difftar-folder.sh tarballs/gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.tar.gz gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608 1
-TARFILE= tarballs/gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.tar.gz
-FOLDER= gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608
-TARSTRIP= 1
-TARPREFIX= gappa-f53e105cd73484fc76eb58ba24ead73be502c608/
-ORIGFOLDER= gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig
---- gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig/src/proofs/property.cpp	2019-06-17 09:39:04.000000000 +0200
-+++ gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608/src/proofs/property.cpp	2019-06-29 19:05:47.321916200 +0200
-@@ -48,7 +48,7 @@
-   new(&store) interval(i);
- }
- 
--property::property(predicated_real const &r, long i): real(r)
-+property::property(predicated_real const &r, intptr_t i): real(r)
- {
-   assert(r.pred_cst());
-   store._int = i;
---- gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608.orig/src/proofs/property.hpp	2019-06-17 09:39:04.000000000 +0200
-+++ gappa_tool-f53e105cd73484fc76eb58ba24ead73be502c608/src/proofs/property.hpp	2019-06-29 19:05:47.305946500 +0200
-@@ -55,7 +55,7 @@
- class property {
-   union store_t {
-     char _bnd[sizeof(interval)];
--    long _int;
-+    intptr_t _int;
-   };
-   store_t store;
-   interval       &_bnd()       { return *reinterpret_cast< interval       * >(&store); }
-@@ -66,16 +66,16 @@
-   { assert(real.pred_bnd()); return _bnd(); }
-   interval const &bnd() const
-   { assert(real.pred_bnd()); return _bnd(); }
--  long &cst()
-+  intptr_t &cst()
-   { assert(real.pred_cst()); return store._int; }
--  long const &cst() const
-+  intptr_t const &cst() const
-   { assert(real.pred_cst()); return store._int; }
-   property();
-   property(ast_real const *);
-   property(ast_real const *, interval const &);
-   property(predicated_real const &);
-   property(predicated_real const &, interval const &);
--  property(predicated_real const &, long);
-+  property(predicated_real const &, intptr_t);
-   property(property const &);
-   property &operator=(property const &);
-   ~property();
-- 
cgit v1.2.3


From d796a830f9b566f2a18bf00f364eb9b8cb235f6e Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Wed, 17 Jul 2019 17:03:46 +0200
Subject: Make windows build fail immediately if plugin patches fail

---
 dev/build/windows/makecoq_mingw.sh | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 98a5fd0a12..0c8213b8f5 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -315,7 +315,7 @@ function get_expand_source_tar {
       find "$(ls)" -mindepth 1 -maxdepth 1 -exec mv -- "{}" . \;
     else
       echo "Unzip strip count not supported"
-      return 1
+      exit 1
     fi
   else
     logn untar tar xvaf "$TARBALLS/$name.$3" --strip $strip
@@ -323,10 +323,11 @@ function get_expand_source_tar {
 
   # Patch if patch file exists
   # First try specific patch file name then generic patch file name
+  # Note: set -o errexit does not work inside a function called in an if, so exit explicity.
   if [ -f "$PATCHES/$name.patch" ] ; then
-    log1 patch -p1 -i "$PATCHES/$name.patch"
+    log1 patch -p1 -i "$PATCHES/$name.patch" || exit 1
   elif  [ -f "$PATCHES/$basename.patch" ] ; then
-    log1 patch -p1 -i "$PATCHES/$basename.patch"
+    log1 patch -p1 -i "$PATCHES/$basename.patch" || exit 1
   fi
 
   # Go back to base folder
-- 
cgit v1.2.3


From a029e231f7f2e22b36f662e6e488815ef273b107 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Wed, 17 Jul 2019 17:05:04 +0200
Subject: Adjust VST patch to latest changes in VST

---
 dev/build/windows/patches_coq/VST.patch | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch
index 2c8c46373f..d047eb107f 100644
--- a/dev/build/windows/patches_coq/VST.patch
+++ b/dev/build/windows/patches_coq/VST.patch
@@ -1,8 +1,7 @@
 diff --git a/Makefile b/Makefile
-index 4a119042..fdfac13e 100755
 --- a/Makefile
 +++ b/Makefile
-@@ -76,8 +76,8 @@ endif
+@@ -82,8 +82,8 @@ endif
 
  COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND)
 
@@ -10,6 +9,6 @@ index 4a119042..fdfac13e 100755
 -EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d))
 +COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d))
 +EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d))
-
- # for SSReflect
- ifdef MATHCOMP
+ # for ITrees
+ ifeq ($(wildcard InteractionTrees/the?ries),"InteractionTrees/theories")
+ EXTFLAGS:=$(EXTFLAGS) -Q InteractionTrees/theories ITree
-- 
cgit v1.2.3


From b349791f7d683f25a79081082218d78fa01b408f Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Wed, 17 Jul 2019 20:58:11 +0200
Subject: Fixed Windows patch for Quickchick

---
 dev/build/windows/patches_coq/quickchick.patch | 41 +++++++++++++++++++-------
 1 file changed, 31 insertions(+), 10 deletions(-)

(limited to 'dev')

diff --git a/dev/build/windows/patches_coq/quickchick.patch b/dev/build/windows/patches_coq/quickchick.patch
index 1afa6e7f95..4b7b86ff05 100644
--- a/dev/build/windows/patches_coq/quickchick.patch
+++ b/dev/build/windows/patches_coq/quickchick.patch
@@ -1,12 +1,12 @@
-diff/patch file created on Mon, Aug 27, 2018  9:21:52 AM with:
-difftar-folder.sh tarballs/quickchick-v1.0.2.tar.gz quickchick-v1.0.2 1
-TARFILE= tarballs/quickchick-v1.0.2.tar.gz
-FOLDER= quickchick-v1.0.2
+diff/patch file created on Wed, Jul 17, 2019  8:06:45 PM with:
+difftar-folder.sh tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0 1
+TARFILE= tarballs/quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.tar.gz
+FOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0
 TARSTRIP= 1
-TARPREFIX= QuickChick-1.0.2/
-ORIGFOLDER= quickchick-v1.0.2.orig
---- quickchick-v1.0.2.orig/Makefile	2018-08-22 18:21:39.000000000 +0200
-+++ quickchick-v1.0.2/Makefile	2018-08-27 09:21:04.710461100 +0200
+TARPREFIX= QuickChick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/
+ORIGFOLDER= quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig
+--- quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0.orig/Makefile	2019-06-26 12:09:01.000000000 +0200
++++ quickchick-741fb98eb865129a70c4ef7a64db2739c4a5eab0/Makefile	2019-07-17 20:05:44.322251200 +0200
 @@ -2,7 +2,7 @@
  .PHONY: plugin install install-plugin clean quickChickTool
  
@@ -16,11 +16,32 @@ ORIGFOLDER= quickchick-v1.0.2.orig
  QCTOOL_SRC=$(QCTOOL_DIR)/quickChickTool.ml \
  		   $(QCTOOL_DIR)/quickChickToolTypes.ml \
  		   $(QCTOOL_DIR)/quickChickToolLexer.mll \
+@@ -20,8 +20,8 @@
+ 
+ all: quickChickTool plugin documentation-check
+ 
+-plugin: Makefile.coq 
+-	$(MAKE) -f Makefile.coq 
++plugin: Makefile.coq
++	$(MAKE) -f Makefile.coq
+ 
+ documentation-check: plugin
+ 	coqc -R src QuickChick -I src QuickChickInterface.v
 @@ -32,7 +32,7 @@
  install: all
  	$(V)$(MAKE) -f Makefile.coq install > $(TEMPFILE)
  # Manually copying the remaining files
--	$(V)cp $(QCTOOL_EXE) $(shell opam config var bin)/quickChick
-+	$(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick"
+-	$(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) $(shell opam config var bin)/quickChick
++	$(V)cp $(QCTOOL_DIR)/$(QCTOOL_EXE) "$(COQBIN)/quickChick"
  #	 $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick
  #	 $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick
+ 
+@@ -56,7 +56,7 @@
+ 	$(MAKE) -C examples/RedBlack test
+ #	cd examples/stlc; make clean && make
+ 	$(MAKE) -C examples/multifile-mutation test
+-# This takes too long. 
++# This takes too long.
+ #	$(MAKE) -C examples/c-mutation test
+ #	coqc examples/BSTTest.v
+ 	coqc examples/DependentTest.v
-- 
cgit v1.2.3


From 7341d286d4a9b440810097352fe257e476a8903c Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Fri, 19 Jul 2019 12:01:59 +0200
Subject: Removed patches for Flocq, Interval and Gappa (merged upstream)

---
 dev/build/windows/patches_coq/flocq.patch        | 27 ------------
 dev/build/windows/patches_coq/gappa_plugin.patch | 52 ------------------------
 dev/build/windows/patches_coq/interval.patch     | 38 -----------------
 3 files changed, 117 deletions(-)
 delete mode 100755 dev/build/windows/patches_coq/flocq.patch
 delete mode 100755 dev/build/windows/patches_coq/gappa_plugin.patch
 delete mode 100755 dev/build/windows/patches_coq/interval.patch

(limited to 'dev')

diff --git a/dev/build/windows/patches_coq/flocq.patch b/dev/build/windows/patches_coq/flocq.patch
deleted file mode 100755
index 33d909f47b..0000000000
--- a/dev/build/windows/patches_coq/flocq.patch
+++ /dev/null
@@ -1,27 +0,0 @@
-diff/patch file created on Sun, Jan 20, 2019 11:55:04 AM with:
-difftar-folder.sh tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e 1
-TARFILE= tarballs/Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.tar.gz
-FOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e
-TARSTRIP= 1
-TARPREFIX= flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/
-ORIGFOLDER= Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig
---- Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e.orig/configure.in	2019-01-11 15:52:30.000000000 +0100
-+++ Flocq-c006474201a8e9ce084c126e3a69a82e14f7cc7e/configure.in	2019-01-20 11:51:49.474668300 +0100
-@@ -10,7 +10,7 @@
- 
- m4_divert_push([HELP_ENABLE])
- Fine tuning of the installation directory:
--AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Flocq@:>@])
-+AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq@:>@])
- m4_divert_pop([HELP_ENABLE])
- 
- AC_PROG_CXX
-@@ -51,7 +51,7 @@
- AC_MSG_RESULT([$COQDOC])
- 
- if test "$libdir" = '${exec_prefix}/lib'; then
--  libdir="`$COQC -where`/user-contrib/Flocq"
-+  libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Flocq"
- fi
- 
- AC_MSG_NOTICE([building remake...])
diff --git a/dev/build/windows/patches_coq/gappa_plugin.patch b/dev/build/windows/patches_coq/gappa_plugin.patch
deleted file mode 100755
index 8bd32318d7..0000000000
--- a/dev/build/windows/patches_coq/gappa_plugin.patch
+++ /dev/null
@@ -1,52 +0,0 @@
-diff/patch file created on Sat, Jun 29, 2019  9:53:06 PM with:
-difftar-folder.sh tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e 1
-TARFILE= tarballs/gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.tar.gz
-FOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e
-TARSTRIP= 1
-TARPREFIX= coq-04d859ea9a496f84569c3f9b8cb66784cd82313e/
-ORIGFOLDER= gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig
---- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/Remakefile.in	2019-04-09 16:57:15.000000000 +0200
-+++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/Remakefile.in	2019-06-29 21:40:03.902985100 +0200
-@@ -43,7 +43,7 @@
- 	@COQC@ -R src Gappa -I src $<
- 
- COQSUBTREES = clib engine kernel interp intf lib library ltac parsing pretyping printing proofs tactics toplevel vernac plugins/ltac
--COQINCLUDES = $(addprefix -I @COQLIB@/, $(COQSUBTREES))
-+COQINCLUDES = $(addprefix -I "@COQLIB@"/, $(COQSUBTREES))
- 
- src/gappatac.cmo: src/gappatac.ml
- 	@OCAMLC@ -pp "@CAMLP4O@ pa_macro.cmo -D@COQDEFINE@" -rectypes $(COQINCLUDES) -c $< -o $@
---- gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e.orig/configure.in	2019-04-09 16:57:15.000000000 +0200
-+++ gappa_plugin-04d859ea9a496f84569c3f9b8cb66784cd82313e/configure.in	2019-06-29 21:47:31.294322200 +0200
-@@ -53,7 +53,17 @@
-   if test ! "$CAMLP4O"; then
-     CAMLP4O=camlp5o
-   fi
--  CAMLP4O=`which $CAMLP4O`
-+  case `uname -s` in
-+    CYGWIN*)
-+      case "$CAMLP4O" in
-+        *:*) CAMLP4O=`cygpath -m "$CAMLP4O"` ;;
-+        *)   CAMLP4O=`cygpath -u "$CAMLP4O"` ;;
-+      esac
-+      ;;
-+    *)
-+      CAMLP4O=`which $CAMLP4O`
-+      ;;
-+  esac
- fi
- AC_MSG_RESULT([$CAMLP4O])
- 
-@@ -81,10 +91,10 @@
- rm -f conftest.v conftest.vo conftest.err
- 
- AC_SUBST(OCAMLLIB)
--OCAMLLIB=`$OCAMLC -where`
-+OCAMLLIB=`$OCAMLC -where | tr -d '\r' | tr '\\' '/'`
- 
- AC_SUBST(COQLIB)
--COQLIB=`$COQC -where`
-+COQLIB=`$COQC -where | tr -d '\r' | tr '\\' '/'`
- 
- if test "$libdir" = '${exec_prefix}/lib'; then
-   libdir="$COQLIB/user-contrib/Gappa"
diff --git a/dev/build/windows/patches_coq/interval.patch b/dev/build/windows/patches_coq/interval.patch
deleted file mode 100755
index 46b2b97826..0000000000
--- a/dev/build/windows/patches_coq/interval.patch
+++ /dev/null
@@ -1,38 +0,0 @@
-diff/patch file created on Sat, Jun 29, 2019  6:44:56 PM with:
-difftar-folder.sh tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628 1
-TARFILE= tarballs/interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.tar.gz
-FOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628
-TARSTRIP= 1
-TARPREFIX= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/
-ORIGFOLDER= interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig
---- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/configure.in	2019-04-09 17:31:18.000000000 +0200
-+++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/configure.in	2019-06-29 18:39:41.889749600 +0200
-@@ -10,7 +10,7 @@
- 
- m4_divert_push([HELP_ENABLE])
- Fine tuning of the installation directory:
--AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where`/user-contrib/Interval@:>@])
-+AS_HELP_STRING([--libdir=DIR], [library @<:@DIR=`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval@:>@])
- m4_divert_pop([HELP_ENABLE])
- 
- AC_PROG_CXX
-@@ -79,7 +79,7 @@
- rm -f conftest.v conftest.vo conftest.err
- 
- if test "$libdir" = '${exec_prefix}/lib'; then
--  libdir="`$COQC -where`/user-contrib/Interval"
-+  libdir="`$COQC -where | tr -d '\r' | tr '\\' '/'`/user-contrib/Interval"
- fi
- 
- AC_MSG_NOTICE([building remake...])
---- interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628.orig/src/Interval_missing.v	2019-04-09 17:31:18.000000000 +0200
-+++ interval-86d4a7138aaf2923dff9b6fe096ccec497bd7628/src/Interval_missing.v	2019-06-29 18:40:57.572496200 +0200
-@@ -1259,7 +1259,7 @@
- intros Heq Hb Hd.
- apply (Rmult_eq_reg_r (b * d)).
- field_simplify; trivial.
--now rewrite Heq.
-+try rewrite Heq.
- now apply Rmult_neq0.
- Qed.
- 
-- 
cgit v1.2.3