aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/ci-basic-overlay.sh38
-rwxr-xr-xdev/ci/ci-bedrock-facade.sh10
-rwxr-xr-xdev/ci/ci-bedrock-src.sh10
-rwxr-xr-xdev/ci/ci-bignums.sh16
-rwxr-xr-xdev/ci/ci-color.sh25
-rwxr-xr-xdev/ci/ci-formal-topology.sh4
-rwxr-xr-xdev/ci/ci-math-classes.sh4
-rwxr-xr-xdev/ci/ci-sf.sh2
-rw-r--r--dev/ci/ci-user-overlay.sh20
9 files changed, 83 insertions, 46 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index d7714274e7..99ec43e412 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -28,11 +28,11 @@
########################################################################
# Mathclasses + Corn
########################################################################
-: ${math_classes_CI_BRANCH:=v8.6}
-: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
+: ${math_classes_CI_BRANCH:=external-bignums}
+: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git}
-: ${Corn_CI_BRANCH:=v8.6}
-: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
+: ${Corn_CI_BRANCH:=external-bignums}
+: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git}
########################################################################
# Iris
@@ -73,14 +73,14 @@
########################################################################
# CompCert
########################################################################
-: ${CompCert_CI_BRANCH:=master}
-: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}
+: ${CompCert_CI_BRANCH:=less_init_plugins}
+: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git}
########################################################################
# VST
########################################################################
-: ${VST_CI_BRANCH:=master}
-: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}
+: ${VST_CI_BRANCH:=less_init_plugins}
+: ${VST_CI_GITURL:=https://github.com/letouzey/VST.git}
########################################################################
# fiat_parsers
@@ -91,20 +91,8 @@
########################################################################
# fiat_crypto
########################################################################
-: ${fiat_crypto_CI_BRANCH:=master}
-: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}
-
-########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=trunk__API}
-: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=trunk__API}
-: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git}
+: ${fiat_crypto_CI_BRANCH:=less_init_plugins}
+: ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
########################################################################
# formal-topology
@@ -133,3 +121,9 @@
########################################################################
: ${tlc_CI_BRANCH:=master}
: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}
+
+########################################################################
+# Bignums
+########################################################################
+: ${bignums_CI_BRANCH:=master}
+: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git}
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073f..0000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b3..0000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
new file mode 100755
index 0000000000..ff5935d4c7
--- /dev/null
+++ b/dev/ci/ci-bignums.sh
@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+
+# This script could be included inside other ones
+# Let's avoid to source ci-common twice in this case
+if [ -z "${CI_BUILD_DIR}"];
+then
+ source ${ci_dir}/ci-common.sh
+fi
+
+bignums_CI_DIR=${CI_BUILD_DIR}/Bignums
+
+git_checkout ${bignums_CI_BRANCH} ${bignums_CI_GITURL} ${bignums_CI_DIR}
+
+( cd ${bignums_CI_DIR} && make -j ${NJOBS} && make install)
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index 3f0716511d..a0a4e0749d 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,6 +5,31 @@ source ${ci_dir}/ci-common.sh
Color_CI_DIR=${CI_BUILD_DIR}/color
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
+# Compiles CoLoR
+
svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR}
+sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v
+sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v
+
+# Adapt to PR #220 (FunInd not loaded in Prelude anymore)
+sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v
+sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v
+sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v
+sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v
+sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v
+sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v
+sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v
+sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v
+sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v
+sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v
+
( cd ${Color_CI_DIR} && make -j ${NJOBS} )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index ecb36349fb..64b78c0396 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -9,6 +9,10 @@ Corn_CI_DIR=${CI_BUILD_DIR}/corn
formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
# Setup Math-Classes
git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index beb75773b7..46581c6381 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -7,6 +7,10 @@ math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
Corn_CI_DIR=${CI_BUILD_DIR}/corn
+# Setup Bignums
+
+source ${ci_dir}/ci-bignums.sh
+
# Setup Math-Classes
git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index 7d23ccad97..23ef41d2dd 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -7,6 +7,8 @@ source ${ci_dir}/ci-common.sh
wget ${sf_CI_TARURL}
tar xvfz sf.tgz
+sed -i.bak '15i From Coq Require Extraction.' sf/Extraction.v
+
( cd sf && sed -i.bak 's/(K,N)/((K,N))/' LibTactics.v && make clean && make -j ${NJOBS} )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 0edaf07efc..b242ce3bd9 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -33,10 +33,22 @@ fi
echo "DEBUG: ci-user-overlay.sh 0"
if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
echo "DEBUG: ci-user-overlay.sh 1"
- bedrock_src_CI_BRANCH=trunk__API
- bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
- bedrock_facade_CI_BRANCH=trunk__API
- bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
fiat_parsers_CI_BRANCH=trunk__API
fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
fi
+
+if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" ]; then
+ math_classes_CI_BRANCH=external-bignums
+ math_classes_CI_GITURL=https://github.com/letouzey/math-classes.git
+ Corn_CI_BRANCH=external-bignums
+ Corn_CI_GITURL=https://github.com/letouzey/corn.git
+fi
+
+if [ $TRAVIS_PULL_REQUEST == "220" ] || [ $TRAVIS_BRANCH == "less_init_plugins" ]; then
+ CompCert_CI_BRANCH=less_init_plugins
+ CompCert_CI_GITURL=https://github.com/letouzey/CompCert.git
+ VST_CI_BRANCH=less_init_plugins
+ VST_CI_GITURL=https://github.com/letouzey/VST.git
+ fiat_crypto_CI_BRANCH=less_init_plugins
+ fiat_crypto_CI_GITURL=https://github.com/letouzey/fiat-crypto.git
+fi
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 11:07:29 +0000