diff options
Diffstat (limited to 'dev/ci')
7 files changed, 37 insertions, 4 deletions
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh index 0256906112..9616f3ce00 100755 --- a/dev/ci/ci-iris.sh +++ b/dev/ci/ci-iris.sh @@ -9,13 +9,13 @@ git_download iris_string_ident git_download iris_examples # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris git_download iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f672ead807..c17ec502e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-17-V88" +# CACHEKEY: "bionic_coq-V2020-10-12-V89" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.11.0" + BASE_ONLY_OPAM="elpi.1.11.4" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh new file mode 100644 index 0000000000..fb5947d218 --- /dev/null +++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then + + mtac2_CI_REF=janno/coq-12449 + mtac2_CI_GITURL=https://github.com/mtac2/mtac2 + +fi diff --git a/dev/ci/user-overlays/13088-gares-par-to-tactic.sh b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh new file mode 100644 index 0000000000..4108a1aed1 --- /dev/null +++ b/dev/ci/user-overlays/13088-gares-par-to-tactic.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13088" ] || [ "$CI_BRANCH" = "par-to-tactic" ]; then + + mtac2_CI_REF=par-to-tactic + mtac2_CI_GITURL=https://github.com/gares/Mtac2 + +fi diff --git a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh new file mode 100644 index 0000000000..654d95f205 --- /dev/null +++ b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then + + elpi_CI_REF=noinstance + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi diff --git a/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh new file mode 100644 index 0000000000..1b3121781b --- /dev/null +++ b/dev/ci/user-overlays/13143-herbelin-master+drop-misleading-arg-hbox.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "13143" ] || [ "$CI_BRANCH" = "master+drop-misleading-arg-hbox" ]; then + + aac_tactics_CI_REF=master+adapt-coq-pr13143-hbox-no-argument + aac_tactics_CI_GITURL=https://github.com/herbelin/aac-tactics + + equations_CI_REF=master+adapt-coq-pr13143-hbox-no-argument + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh new file mode 100644 index 0000000000..7d55cf6883 --- /dev/null +++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then + + elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi |