diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 18 | ||||
| -rwxr-xr-x | dev/ci/ci-coq-dpdgraph.sh | 10 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 10 |
3 files changed, 32 insertions, 6 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index d75011de3..3adc31935 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -85,8 +85,8 @@ ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=master} -: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} +: ${fiat_parsers_CI_BRANCH:=trunk__API} +: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git} ######################################################################## # fiat_crypto @@ -97,14 +97,14 @@ ######################################################################## # bedrock_src ######################################################################## -: ${bedrock_src_CI_BRANCH:=master} -: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git} +: ${bedrock_src_CI_BRANCH:=trunk__API} +: ${bedrock_src_CI_GITURL:=https://github.com/matejkosik/bedrock.git} ######################################################################## # bedrock_facade ######################################################################## -: ${bedrock_facade_CI_BRANCH:=master} -: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git} +: ${bedrock_facade_CI_BRANCH:=trunk__API} +: ${bedrock_facade_CI_GITURL:=https://github.com/matejkosik/bedrock.git} ######################################################################## # formal-topology @@ -113,6 +113,12 @@ : ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} ######################################################################## +# coq-dpdgraph +######################################################################## +: ${coq_dpdgraph_CI_BRANCH:=coq-trunk} +: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} + +######################################################################## # CoLoR ######################################################################## : ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} diff --git a/dev/ci/ci-coq-dpdgraph.sh b/dev/ci/ci-coq-dpdgraph.sh new file mode 100755 index 000000000..e8018158b --- /dev/null +++ b/dev/ci/ci-coq-dpdgraph.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +coq_dpdgraph_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph + +git_checkout ${coq_dpdgraph_CI_BRANCH} ${coq_dpdgraph_CI_GITURL} ${coq_dpdgraph_CI_DIR} + +( cd ${coq_dpdgraph_CI_DIR} && autoconf && ./configure && make -j ${NJOBS} && make tests && (make tests | tee tmp.log) && (if grep DIFFERENCES tmp.log ; then exit 1 ; else exit 0 ; fi) ) diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 195ede6d0..0edaf07ef 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -30,3 +30,13 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git 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 |