diff options
Diffstat (limited to 'dev/ci')
26 files changed, 180 insertions, 51 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index 64936cd236..f2397cdcee 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.10.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.11.1+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 @@ -10,4 +10,4 @@ bash opam64/install.sh opam init default -a -y "https://github.com/fdopen/opam-repository-mingw.git#opam2" -c $OPAM_VARIANT --disable-sandboxing eval "$(opam env)" -opam install -y num ocamlfind dune ounit +opam install -y num ocamlfind dune ounit zarith diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 2725e6b56c..75d9efaadc 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -62,9 +62,17 @@ : "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" : "${iris_CI_ARCHIVEURL:=${iris_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}" +: "${autosubst_CI_REF:=coq86-devel}" +: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}" +: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}" + +: "${iris_string_ident_CI_REF:=master}" +: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}" +: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}" + +: "${iris_examples_CI_REF:=master}" +: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}" +: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}" ######################################################################## # HoTT diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index c01bc57f72..f9187d53a6 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -97,9 +97,9 @@ make() if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; then # Not submake and parallel make requested - command make -j "$NJOBS" "$@" + command make --output-sync -j "$NJOBS" "$@" else - command make "$@" + command make --output-sync "$@" fi } diff --git a/dev/ci/ci-coqtail.sh b/dev/ci/ci-coqtail.sh index b8b5c6c724..ab538ecc07 100755 --- a/dev/ci/ci-coqtail.sh +++ b/dev/ci/ci-coqtail.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download coqtail -( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/test_coqtop.py ) +( cd "${CI_BUILD_DIR}/coqtail" && PYTHONPATH=python python3 -m pytest tests/coq ) diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh new file mode 100755 index 0000000000..9616f3ce00 --- /dev/null +++ b/dev/ci/ci-iris.sh @@ -0,0 +1,36 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +# Setup iris_examples and separate dependencies first +git_download autosubst +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/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/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') + +# Setup std++ +git_download stdpp + +# Build std++ +( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) + +# Build and validate Iris +( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) + +# Build autosubst +( cd "${CI_BUILD_DIR}/autosubst" && make && make install ) + +# Build iris-string-ident +( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install ) + +# Build Iris examples +( cd "${CI_BUILD_DIR}/iris_examples" && make && make install ) diff --git a/dev/ci/ci-lambda_rust.sh b/dev/ci/ci-lambda_rust.sh deleted file mode 100755 index 1ef0c2cb8f..0000000000 --- a/dev/ci/ci-lambda_rust.sh +++ /dev/null @@ -1,30 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -install_ssreflect - -# 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}/lambda_rust/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/') - -# Setup std++ -git_download stdpp - -# Build std++ -( cd "${CI_BUILD_DIR}/stdpp" && make && make install ) - -# Build and validate Iris -( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install ) - -# Build lambda_rust -( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install ) diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh index cae127ee7b..b1aa56ec4e 100755 --- a/dev/ci/ci-mathcomp.sh +++ b/dev/ci/ci-mathcomp.sh @@ -6,7 +6,7 @@ ci_dir="$(dirname "$0")" git_download mathcomp -( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make install ) +( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install ) git_download fourcolor diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 1302065961..27876d68de 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download metacoq -( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make .merlin && make ci-local && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 7570b17095..c17ec502e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-07-21-V38" +# CACHEKEY: "bionic_coq-V2020-10-12-V89" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -6,9 +6,14 @@ LABEL maintainer="e@x80.org" ENV DEBIAN_FRONTEND="noninteractive" +# We need libgmp-dev:i386 for zarith; maybe we could also install GTK +RUN dpkg --add-architecture i386 + RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of the image, the test-suite and external projects m4 automake autoconf time wget rsync git gcc-multilib build-essential unzip jq \ + # Dependencies of ZArith + perl libgmp-dev libgmp-dev:i386 \ # Dependencies of lablgtk (for CoqIDE) libgtksourceview-3.0-dev \ # Dependencies of stdlib and sphinx doc @@ -35,12 +40,10 @@ ENV NJOBS="2" \ # Base opam is the set of base packages required by Coq 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 ounit.2.2.2 odoc.1.5.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" @@ -52,13 +55,14 @@ ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" RUN opam init -a --disable-sandboxing --compiler="$COMPILER" default https://opam.ocaml.org && eval $(opam env) && opam update && \ opam install $BASE_OPAM $COQIDE_OPAM $CI_OPAM $BASE_ONLY_OPAM -# base+32bit switch +# base+32bit switch, note the zarith hack RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ - opam install $BASE_OPAM + i386 env CC='gcc -m32' opam install zarith.1.10 && \ + opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.10.0" \ - BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.14.2" +ENV COMPILER_EDGE="4.11.1" \ + BASE_OPAM_EDGE="dune.2.5.1 dune-release.1.3.3 ocamlformat.0.15.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 05624ff4a1..7863af842a 100644 --- a/dev/ci/nix/default.nix +++ b/dev/ci/nix/default.nix @@ -114,6 +114,7 @@ let projects = { mtac2 = callPackage ./mtac2.nix {}; oddorder = callPackage ./oddorder.nix {}; quickchick = callPackage ./quickchick.nix {}; + simple-io = callPackage ./simple-io.nix {}; verdi-raft = callPackage ./verdi-raft.nix {}; VST = callPackage ./VST.nix {}; }; in @@ -130,7 +131,8 @@ stdenv.mkDerivation { name = "shell-for-${project}-in-${branch}"; buildInputs = - optional withCoq coq + [ python ] + ++ optional withCoq coq ++ (prj.buildInputs or []) ++ optionals withCoq (prj.coqBuildInputs or []) ; diff --git a/dev/ci/nix/simple-io.nix b/dev/ci/nix/simple-io.nix new file mode 100644 index 0000000000..3b7b6c09b1 --- /dev/null +++ b/dev/ci/nix/simple-io.nix @@ -0,0 +1,5 @@ +{ ocamlPackages, ssreflect, coq-ext-lib, simple-io }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib ocamlbuild num ]; + coqBuildInputs = [ ssreflect coq-ext-lib ]; +} diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh new file mode 100644 index 0000000000..da1d30c1e9 --- /dev/null +++ b/dev/ci/user-overlays/08743-ejgallego-zarith.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then + + bignums_CI_REF=zarith + bignums_CI_GITURL=https://github.com/ejgallego/bignums + +fi 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/12565-ppedrot-fix-tc-search-opacity.sh b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh new file mode 100644 index 0000000000..7c04608403 --- /dev/null +++ b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12565" ] || [ "$CI_BRANCH" = "fix-tc-search-opacity" ]; then + + coqhammer_CI_REF=fix-tc-search-opacity + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh new file mode 100644 index 0000000000..56a69abbf7 --- /dev/null +++ b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then + + coqhammer_CI_REF=hint-pattern-out + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh new file mode 100644 index 0000000000..e57f95ef19 --- /dev/null +++ b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then + + coqhammer_CI_REF=factor-class-hint-clenv + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + +fi diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh new file mode 100644 index 0000000000..54fdd87566 --- /dev/null +++ b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then + + mathcomp_CI_REF=dont-refresh-argument-names-overlay + mathcomp_CI_GITURL=https://github.com/jashug/math-comp + + oddorder_CI_REF=dont-refresh-argument-names-overlay + oddorder_CI_GITURL=https://github.com/jashug/odd-order + +fi diff --git a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh new file mode 100644 index 0000000000..6a9cf78687 --- /dev/null +++ b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "12801" ] || [ "$CI_BRANCH" = "CyclicSet" ]; then + + bignums_CI_REF=CyclicSet + bignums_CI_GITURL=https://github.com/VincentSe/bignums + + coqprime_CI_REF=CyclicSet + coqprime_CI_GITURL=https://github.com/VincentSe/coqprime +fi diff --git a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh new file mode 100644 index 0000000000..bb08c13ef3 --- /dev/null +++ b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then + + elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh new file mode 100644 index 0000000000..f0878202d3 --- /dev/null +++ b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then + + elpi_CI_REF=update-s-univs + elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi + + equations_CI_REF=update-s-univs + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh new file mode 100644 index 0000000000..ee75944a52 --- /dev/null +++ b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then + + equations_CI_REF=delay-frozen-evarconv + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh new file mode 100644 index 0000000000..7bed43afe1 --- /dev/null +++ b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "12977" ] || [ "$CI_BRANCH" = "static-hint-poly" ]; then + + equations_CI_REF=static-hint-poly + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + fiat_parsers_CI_REF=static-hint-poly + fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat + +fi diff --git a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh new file mode 100644 index 0000000000..3407c2db39 --- /dev/null +++ b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13028" ] || [ "$CI_BRANCH" = "master+fix-quotations-printing" ]; then + + equations_CI_REF=master+adapt-coq-pr13028-quotation-qualifier-printing + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +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 |