diff options
Diffstat (limited to 'dev/ci')
25 files changed, 126 insertions, 44 deletions
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index 6a740b9033..88d08a1724 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil ### Experimental automatic overlay creation and building If you break external projects that are hosted on GitHub, you can use -the `create-overlays.sh` script to automatically perform most of the +the `create_overlays.sh` script to automatically perform most of the above steps. In order to do so, call the script as: ``` -./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac +./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac ``` replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR number. The script will: diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 7b3e2703b8..64936cd236 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c +OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index c18e556da8..b87a9c0392 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -46,9 +46,9 @@ : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" -: "${Corn_CI_REF:=master}" -: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}" -: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}" +: "${corn_CI_REF:=master}" +: "${corn_CI_GITURL:=https://github.com/coq-community/corn}" +: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}" ######################################################################## # Iris @@ -59,19 +59,19 @@ : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" -: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" -: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}" +: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" +: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}" -: "${lambdaRust_CI_REF:=master}" -: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" -: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}" +: "${lambda_rust_CI_REF:=master}" +: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}" +: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}" ######################################################################## # HoTT ######################################################################## -: "${HoTT_CI_REF:=master}" -: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}" -: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" +: "${hott_CI_REF:=master}" +: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}" +: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}" ######################################################################## # CoqHammer @@ -83,16 +83,23 @@ ######################################################################## # GeoCoq ######################################################################## -: "${GeoCoq_CI_REF:=master}" -: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" -: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}" +: "${geocoq_CI_REF:=master}" +: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" +: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}" ######################################################################## # Flocq ######################################################################## -: "${Flocq_CI_REF:=master}" -: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" -: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}" +: "${flocq_CI_REF:=master}" +: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" +: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}" + +######################################################################## +# coq-tools +######################################################################## +: "${coq_tools_CI_REF:=master}" +: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}" +: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}" ######################################################################## # Coquelicot @@ -242,7 +249,7 @@ # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" -: "${ext_lib_CI_GITURL:=https://github.com/coq-ext-lib/coq-ext-lib}" +: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}" : "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" ######################################################################## diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index 756f54dfbd..a21310cbd5 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download bignums -( cd "${CI_BUILD_DIR}/bignums" && make && make install) +( cd "${CI_BUILD_DIR}/bignums" && make && make install && cd tests && make) diff --git a/dev/ci/ci-coq_tools.sh b/dev/ci/ci-coq_tools.sh new file mode 100755 index 0000000000..9c95c49c9f --- /dev/null +++ b/dev/ci/ci-coq_tools.sh @@ -0,0 +1,9 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coq_tools + +( cd "${CI_BUILD_DIR}/coq_tools" && make check || \ + { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } ) diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh index 7d5d70cf90..ac3978dc8d 100755 --- a/dev/ci/ci-corn.sh +++ b/dev/ci/ci-corn.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Corn +git_download corn -( cd "${CI_BUILD_DIR}/Corn" && make && make install ) +( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install ) diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross_crypto.sh index 900d12c1dd..900d12c1dd 100755 --- a/dev/ci/ci-cross-crypto.sh +++ b/dev/ci/ci-cross_crypto.sh diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext_lib.sh index 5eb167d97d..5eb167d97d 100755 --- a/dev/ci/ci-ext-lib.sh +++ b/dev/ci/ci-ext_lib.sh diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl_pcm.sh index cb951630c8..cb951630c8 100755 --- a/dev/ci/ci-fcsl-pcm.sh +++ b/dev/ci/ci-fcsl_pcm.sh diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat_crypto.sh index 811fefda35..811fefda35 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat_crypto.sh diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index e87483df0a..a3a704091b 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download Flocq +git_download flocq -( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" ) +( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 8c57318477..e4fc983e68 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -5,6 +5,6 @@ ci_dir="$(dirname "$0")" install_ssralg -git_download GeoCoq +git_download geocoq -( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make ) +( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index c8e6fe690f..4b92c8cb4d 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" . "${ci_dir}/ci-common.sh" -git_download HoTT +git_download hott -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-lambda_rust.sh index d99e140bce..1ef0c2cb8f 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-lambda_rust.sh @@ -5,17 +5,17 @@ ci_dir="$(dirname "$0")" install_ssreflect -# Setup lambdaRust first -git_download lambdaRust +# Setup lambda_rust first +git_download lambda_rust # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/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}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris -git_download 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/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp @@ -24,7 +24,7 @@ git_download stdpp ( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) # Build and validate Iris -( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install ) +( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) -# Build lambdaRust -( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install ) +# Build lambda_rust +( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math_classes.sh index ae31a8e7f8..ae31a8e7f8 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math_classes.sh diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-mathcomp.sh index cae127ee7b..cae127ee7b 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-mathcomp.sh diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple_io.sh index e7bcd80de7..e7bcd80de7 100755 --- a/dev/ci/ci-simple-io.sh +++ b/dev/ci/ci-simple_io.sh diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi_raft.sh index 3bcd52c464..3bcd52c464 100755 --- a/dev/ci/ci-verdi-raft.sh +++ b/dev/ci/ci-verdi_raft.sh diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index e56e4d38ea..e240ea3ba1 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-03-19-V29" +# CACHEKEY: "bionic_coq-V2020-03-13-V69" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -22,7 +22,7 @@ RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. -RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam +RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam # Basic OPAM setup ENV NJOBS="2" \ @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `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.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" @@ -56,8 +56,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.09.1" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" +ENV COMPILER_EDGE="4.10.0" \ + BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix index c8ea59f08a..b3ced999f6 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -22,7 +22,7 @@ let ssreflect = coqPackages.ssreflect.overrideAttrs (o: { }); in let coq-ext-lib = coqPackages.coq-ext-lib.overrideAttrs (o: { - src = fetchTarball "https://github.com/coq-ext-lib/coq-ext-lib/tarball/master"; + src = fetchTarball "https://github.com/coq-community/coq-ext-lib/tarball/master"; }); in let simple-io = diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh new file mode 100644 index 0000000000..e3a8eb07f3 --- /dev/null +++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then + + metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + metacoq_CI_GITURL=https://github.com/ejgallego/metacoq + + elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual + paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq + + equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual + equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh new file mode 100644 index 0000000000..4170799be7 --- /dev/null +++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then + + elpi_CI_REF=partial-import + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi 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 diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh new file mode 100644 index 0000000000..b5faabcfe1 --- /dev/null +++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then + + elpi_CI_REF=no-mod-univs + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + +fi |