diff options
| -rw-r--r-- | .circleci/config.yml | 6 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 6 | ||||
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-elpi.sh | 10 |
6 files changed, 31 insertions, 1 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 9b0cc2119..441d89d42 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -191,7 +191,7 @@ jobs: environment: <<: *envvars EXTRA_PACKAGES: *coqide-packages - EXTRA_OPAM: "ocamlgraph" + EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" opam-boot-32bit: <<: *opam-boot-template @@ -286,6 +286,9 @@ jobs: <<: *ci-template-vars EXTRA_PACKAGES: "time python autoconf automake" + elpi: + <<: *ci-template + equations: <<: *ci-template @@ -369,6 +372,7 @@ workflows: - compcert: *req-main - coq-dpdgraph: *req-main - coquelicot: *req-main + - elpi: *req-main - equations: *req-main - geocoq: *req-main - fiat-crypto: *req-main diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6b52870ce..5dd376079 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -285,6 +285,12 @@ ci-coquelicot: <<: *ci-template-vars EXTRA_PACKAGES: "$TIMING_PACKAGES autoconf" +ci-elpi: + <<: *ci-template + variables: + <<: *ci-template-vars + EXTRA_OPAM: "ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" + ci-equations: <<: *ci-template diff --git a/.travis.yml b/.travis.yml index 19e7075f2..f4f01d2f0 100644 --- a/.travis.yml +++ b/.travis.yml @@ -76,6 +76,9 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-elpi" EXTRA_OPAM="ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: diff --git a/Makefile.ci b/Makefile.ci index 80fbd7bbe..4e92264d6 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -5,6 +5,7 @@ CI_TARGETS=ci-bignums \ ci-coquelicot \ ci-corn \ ci-cpdt \ + ci-elpi \ ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 784da6f97..48e01e9e9 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -144,3 +144,9 @@ ######################################################################## : "${Equations_CI_BRANCH:=8.8+alpha}" : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" + +######################################################################## +# Elpi +######################################################################## +: "${Elpi_CI_BRANCH:=coq-master}" +: "${Elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi.git}" diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh new file mode 100755 index 000000000..c44e0a655 --- /dev/null +++ b/dev/ci/ci-elpi.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +Elpi_CI_DIR=${CI_BUILD_DIR}/elpi + +git_checkout ${Elpi_CI_BRANCH} ${Elpi_CI_GITURL} ${Elpi_CI_DIR} + +( cd ${Elpi_CI_DIR} && make && make install ) |