diff options
Diffstat (limited to 'dev/ci')
| -rw-r--r-- | dev/ci/README.md | 5 | ||||
| -rw-r--r-- | dev/ci/appveyor.sh | 10 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh | 4 | ||||
| -rw-r--r-- | dev/ci/user-overlays/07495-gares-elpi-test-bug.sh | 8 |
5 files changed, 29 insertions, 2 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md index 697a160ca9..dc586c61fb 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -89,6 +89,11 @@ We are currently running tests on the following platforms: - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. +GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit +message to bypass CI. Do not use this unless your commit only changes files +that are not compiled (e.g. Markdown files like this one, or files under +[`.github/`](/.github/)). + You can anticipate the results of most of these tests prior to submitting your PR by running GitLab CI on your private branches. To do so follow these steps: diff --git a/dev/ci/appveyor.sh b/dev/ci/appveyor.sh index c72705c7f7..7bf9ad8c9b 100644 --- a/dev/ci/appveyor.sh +++ b/dev/ci/appveyor.sh @@ -1,9 +1,15 @@ #!/bin/bash + set -e -x + +APPVEYOR_OPAM_SWITCH=4.06.1+mingw64c + wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.1/opam64.tar.xz tar -xf opam64.tar.xz bash opam64/install.sh -opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp 4.02.3+mingw64c --switch 4.02.3+mingw64c + +opam init -a mingw https://github.com/fdopen/opam-repository-mingw.git --comp $APPVEYOR_OPAM_SWITCH --switch $APPVEYOR_OPAM_SWITCH eval "$(opam config env)" -opam install -y ocamlfind camlp5 ounit +opam install -y num ocamlfind camlp5 ounit + cd "$APPVEYOR_BUILD_FOLDER" && ./configure -local && make && make byte && make -C test-suite all INTERACTIVE= && make validate diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index 8d490591b6..0b0e06e29f 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,6 +5,10 @@ ci_dir="$(dirname "$0")" CompCert_CI_DIR="${CI_BUILD_DIR}/CompCert" +# Temporal workaround, to be removed when upstream decides what to do +# with their problem. +opam install -y menhir.20180528 + git_checkout "${CompCert_CI_BRANCH}" "${CompCert_CI_GITURL}" "${CompCert_CI_DIR}" ( cd "${CompCert_CI_DIR}" && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh new file mode 100644 index 0000000000..e6c48d10a6 --- /dev/null +++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then + Equations_CI_BRANCH=unification-returns-option + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh new file mode 100644 index 0000000000..6939ead2ba --- /dev/null +++ b/dev/ci/user-overlays/07495-gares-elpi-test-bug.sh @@ -0,0 +1,8 @@ +if [ "$CI_PULL_REQUEST" = "7495" ] || [ "$CI_BRANCH" = "fix-restrict" ]; then + + # this branch contains a commit not present on coq-master that triggers + # the universe restriction bug #7472 + Elpi_CI_BRANCH=overlay-7495 + Elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi.git + +fi |