diff options
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-flocq.sh | 2 | ||||
| -rw-r--r-- | dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh | 24 | ||||
| -rw-r--r-- | dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh | 15 |
3 files changed, 40 insertions, 1 deletions
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index e9f8324f28..7a9531216e 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download Flocq -( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh new file mode 100644 index 0000000000..cd6b408813 --- /dev/null +++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh @@ -0,0 +1,24 @@ +if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then + + coqhammer_CI_REF="evar-inst-list" + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + elpi_CI_REF="evar-inst-list" + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + equations_CI_REF="evar-inst-list" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + metacoq_CI_REF="evar-inst-list" + metacoq_CI_GITURL=https://github.com/ppedrot/metacoq + + mtac2_CI_REF="evar-inst-list" + mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 + + quickchick_CI_REF="evar-inst-list" + quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick + + unicoq_CI_REF="evar-inst-list" + unicoq_CI_GITURL=https://github.com/ppedrot/unicoq + +fi diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh new file mode 100644 index 0000000000..6bee3c7bb6 --- /dev/null +++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then + + fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto + + mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 + + metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + metacoq_CI_GITURL=https://github.com/herbelin/template-coq + + unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file + unimath_CI_GITURL=https://github.com/herbelin/UniMath + +fi |