diff options
| author | Maxime Dénès | 2017-06-14 12:32:05 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-14 12:32:05 +0200 |
| commit | 81243d8ac2c10fb4a3f8b1236a8947d5d60fe6cd (patch) | |
| tree | 1b6ef74ee2bbeefaed3a09e27ed14a2b2d0fd44c /dev/ci | |
| parent | b240771a3661883ca0cc0497efee5b48519bddea (diff) | |
| parent | bb6dbba6a76f83c7cbac7a1f8d6eaa14da2d3d40 (diff) | |
Merge PR#220: Less init plugins
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-color.sh | 14 | ||||
| -rwxr-xr-x | dev/ci/ci-sf.sh | 2 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 9 |
3 files changed, 25 insertions, 0 deletions
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 57f569858b..a0a4e0749d 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -18,4 +18,18 @@ sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${C 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-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 200d431bcb..2ecd40416f 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -47,3 +47,12 @@ if [ $TRAVIS_PULL_REQUEST == "498" ] || [ $TRAVIS_BRANCH == "outsource-bignums" 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 |