aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/build/windows/MakeCoq_MinGW.bat2
-rwxr-xr-xdev/build/windows/makecoq_mingw.sh114
-rw-r--r--dev/build/windows/patches_coq/VST.patch9
-rw-r--r--dev/build/windows/patches_coq/quickchick.patch41
-rwxr-xr-xdev/ci/ci-basic-overlay.sh21
-rwxr-xr-xdev/ci/gitlab.bat8
6 files changed, 173 insertions, 22 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..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
@@ -1146,7 +1147,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 +1156,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 +1830,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 +1893,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/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
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
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}"
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= "
)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:27:03 +0000