diff options
| -rw-r--r-- | .circleci/config.yml | 4 | ||||
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | .travis.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 6 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 13 |
6 files changed, 30 insertions, 0 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index f811f26e1..451b711be 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -209,6 +209,9 @@ jobs: mtac2: <<: *ci-template + pidetop: + <<: *ci-template + sf: <<: *ci-template environment: @@ -266,6 +269,7 @@ workflows: - iris-lambda-rust: *req-main - ltac2: *req-main - math-comp: *req-main + - pidetop: *req-main - sf: *req-main - unimath: *req-main - vst: *req-main diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 6b42ac7eb..d16dc5b78 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -363,6 +363,9 @@ ci-math-comp: ci-mtac2: <<: *ci-template +ci-pidetop: + <<: *ci-template + ci-sf: <<: *ci-template variables: diff --git a/.travis.yml b/.travis.yml index 99e50dc72..fce19f9d9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -120,6 +120,9 @@ matrix: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: + - TEST_TARGET="ci-pidetop" + - if: NOT (type = pull_request) + env: - TEST_TARGET="ci-sf" - if: NOT (type = pull_request) env: diff --git a/Makefile.ci b/Makefile.ci index 37b14ed91..78fec466c 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,6 +29,7 @@ CI_TARGETS=ci-bignums \ ci-math-classes \ ci-math-comp \ ci-mtac2 \ + ci-pidetop \ ci-sf \ ci-tlc \ ci-unimath \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5cee72cc7..1ae2ad0ac 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -156,3 +156,9 @@ ######################################################################## : "${fcsl_pcm_CI_BRANCH:=master}" : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}" + +######################################################################## +# pidetop +######################################################################## +: "${pidetop_CI_BRANCH:=v8.9}" +: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh new file mode 100755 index 000000000..d04b9637c --- /dev/null +++ b/dev/ci/ci-pidetop.sh @@ -0,0 +1,13 @@ +#!/usr/bin/env bash + +# $0 is not the safest way, but... +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" + +git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" + +( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) + +echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop |