diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 16 | ||||
| -rwxr-xr-x | dev/ci/ci-bignums.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-ltac2.sh | 10 |
3 files changed, 22 insertions, 6 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9be882bb3c..cb1493d6aa 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:=external-bignums} -: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git} +: ${math_classes_CI_BRANCH:=master} +: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} -: ${Corn_CI_BRANCH:=external-bignums} -: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git} +: ${Corn_CI_BRANCH:=master} +: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} ######################################################################## # Iris @@ -53,6 +53,12 @@ : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## +# Ltac2 +######################################################################## +: ${ltac2_CI_BRANCH:=master} +: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git} + +######################################################################## # GeoCoq ######################################################################## : ${GeoCoq_CI_BRANCH:=master} @@ -80,7 +86,7 @@ # VST ######################################################################## : ${VST_CI_BRANCH:=master} -: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} ######################################################################## # fiat_parsers diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index ff5935d4c7..d68674381a 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -4,7 +4,7 @@ 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}"]; +if [ -z "${CI_BUILD_DIR}" ]; then source ${ci_dir}/ci-common.sh fi diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh new file mode 100755 index 0000000000..4865be31ec --- /dev/null +++ b/dev/ci/ci-ltac2.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph + +git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} + +( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install ) |