diff options
Diffstat (limited to 'dev/ci')
8 files changed, 60 insertions, 4 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 95fceb773a..fa39b41565 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,7 +215,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=dev}" +: "${simple_io_CI_REF:=master}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index bba17314f7..e8c8d22678 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -11,7 +11,7 @@ git_download fiat_crypto # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 fiat_crypto_CI_TARGETS1="c-files printlite lite" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" +fiat_crypto_CI_TARGETS2="coq" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s 32768 && \ diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 8eebb3af64..818454dbbc 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-04-20-V1" +# CACHEKEY: "bionic_coq-V2019-06-11-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -38,7 +38,7 @@ ENV COMPILER="4.05.0" # `num` does not have a version number as the right version to install varies # with the compiler version. ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.6.2 ounit.2.0.8 odoc.1.4.0" \ - CI_OPAM="menhir.20181113 elpi.1.2.0 ocamlgraph.1.8.8" + CI_OPAM="menhir.20181113 elpi.1.3.1 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6 lablgtk3-sourceview3.3.0.beta5" diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh new file mode 100644 index 0000000000..242b177d71 --- /dev/null +++ b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh @@ -0,0 +1,23 @@ +if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then + + fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726 + fiat_parsers_CI_REF=master+change-for-coq-pr8726 + fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat + + elpi_CI_BRANCH=coq-master+fix-global-pr8726 + elpi_CI_REF=coq-master+fix-global-pr8726 + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + + equations_CI_BRANCH=master+fix-global-pr8726 + equations_CI_REF=master+fix-global-pr8726 + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + + mtac2_CI_BRANCH=master+fix-global-pr8726 + mtac2_CI_REF=master+fix-global-pr8726 + mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 + + paramcoq_CI_BRANCH=master+fix-global-pr8726 + paramcoq_CI_REF=master+fix-global-pr8726 + paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq + +fi diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh new file mode 100644 index 0000000000..e4cf74aa51 --- /dev/null +++ b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then + + aac_tactics_CI_REF=proof_global+move_termination_routine_out + aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics + + equations_CI_REF=proof_global+move_termination_routine_out + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + paramcoq_CI_REF=proof_global+move_termination_routine_out + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + +fi diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh new file mode 100644 index 0000000000..c5f1510357 --- /dev/null +++ b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then + + mtac2_CI_REF=vernac-when-sideff + mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 + + equations_CI_REF=vernac-when-sideff + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh new file mode 100644 index 0000000000..2c3f490c03 --- /dev/null +++ b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then + + equations_CI_REF=rm-kernel-sideeff-role + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/10358-gares-elpi13.sh b/dev/ci/user-overlays/10358-gares-elpi13.sh new file mode 100644 index 0000000000..d2ba9b5ddf --- /dev/null +++ b/dev/ci/user-overlays/10358-gares-elpi13.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10358" ] || [ "$CI_BRANCH" = "elpi-13-coq" ]; then + + elpi_CI_REF="elpi-13-coq" + elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi + +fi |