Fix #9351 in master (Add Flocq, CoqInterval, Gappa tool and Gappa)

7 files changed, 294 insertions, 2 deletions

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
@@ -102,6 +102,27 @@
 : "${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
 ########################################################################
 : "${compcert_CI_REF:=master}"