From fe9340263be1c28fb0dc4c7312cddd72e91253c8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 21 Nov 2018 18:33:05 +0100
Subject: 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.
---
 dev/ci/ci-basic-overlay.sh |  7 -------
 dev/ci/ci-pidetop.sh       | 19 -------------------
 2 files changed, 26 deletions(-)
 delete mode 100755 dev/ci/ci-pidetop.sh

(limited to 'dev')

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
@@ -214,13 +214,6 @@
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}"
 : "${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
 ########################################################################
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
-- 
cgit v1.2.3