diff options
| author | Maxime Dénès | 2018-11-21 18:33:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-21 18:42:12 +0100 |
| commit | fe9340263be1c28fb0dc4c7312cddd72e91253c8 (patch) | |
| tree | 2748374c125599edb8ad76d5125bd23bd51055a0 | |
| parent | 452cb15fd9647dc453cc36614cc469dfa91e3080 (diff) | |
Remove pidetop from CI
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 19 |
4 files changed, 0 insertions, 30 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ea7eccb47f..8feeec3883 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -436,9 +436,6 @@ ci-mtac2: ci-paramcoq: <<: *ci-template -ci-pidetop: - <<: *ci-template - ci-plugin_tutorial: <<: *ci-template diff --git a/Makefile.ci b/Makefile.ci index 88ea64974a..d0b87fc58b 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-pidetop \ ci-plugin_tutorial \ ci-quickchick \ ci-sf \ diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4d5834eeb6..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,13 +215,6 @@ : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## -# pidetop -######################################################################## -: "${pidetop_CI_REF:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" -: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" - -######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh deleted file mode 100755 index 1a9a26843c..0000000000 --- a/dev/ci/ci-pidetop.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download pidetop - -# Travis / Gitlab have different filesystem layout due to use of -# `-local`. We need to improve this divergence but if we use Dune this -# "local" oddity goes away automatically so not bothering... -if [ -d "$COQBIN/../lib/coq" ]; then - COQLIB="$COQBIN/../lib/coq/" -else - COQLIB="$COQBIN/../" -fi - -( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) - -echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds |