Remove bedrock from test suite.

Bedrock relies on the 8.4 compat flag that we are removing, and we heard
from MIT that they did not plan to port bedrock to more recent versions
of Coq.

7 files changed, 0 insertions, 46 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index d5351f5738..1de9e7f7c8 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -244,12 +244,6 @@ validate:32bit:
 ci-bignums:
   <<: *ci-template
 
-ci-bedrock-src:
-  <<: *ci-template
-
-ci-bedrock-facade:
-  <<: *ci-template
-
 ci-color:
   <<: *ci-template
   variables:
diff --git a/.travis.yml b/.travis.yml
index 01680583f0..224dfe2f57 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -38,8 +38,6 @@ env:
   - TEST_TARGET="validate"                           TW="travis_wait"
   - TEST_TARGET="validate"   COMPILER="4.02.3+32bit" TW="travis_wait"
   - TEST_TARGET="ci-bignums"
-  - TEST_TARGET="ci-bedrock-src"
-  - TEST_TARGET="ci-bedrock-facade"
   - TEST_TARGET="ci-color"
   - TEST_TARGET="ci-compcert"
   - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph"
diff --git a/Makefile.ci b/Makefile.ci
index 2f7fcd48a5..3be90c0a31 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,7 +1,5 @@
 CI_TARGETS=ci-all \
     ci-bignums \
-    ci-bedrock-facade \
-    ci-bedrock-src \
     ci-color \
     ci-compcert \
     ci-coq-dpdgraph \
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 7f66dfb3b0..0099e815f4 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,18 +95,6 @@
 : ${fiat_crypto_CI_GITURL:=https://github.com/letouzey/fiat-crypto.git}
 
 ########################################################################
-# bedrock_src
-########################################################################
-: ${bedrock_src_CI_BRANCH:=master}
-: ${bedrock_src_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
-# bedrock_facade
-########################################################################
-: ${bedrock_facade_CI_BRANCH:=master}
-: ${bedrock_facade_CI_GITURL:=https://github.com/mit-plv/bedrock.git}
-
-########################################################################
 # formal-topology
 ########################################################################
 : ${formal_topology_CI_BRANCH:=ci}
diff --git a/dev/ci/ci-bedrock-facade.sh b/dev/ci/ci-bedrock-facade.sh
deleted file mode 100755
index 95cfa3073f..0000000000
--- a/dev/ci/ci-bedrock-facade.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_facade_CI_DIR=${CI_BUILD_DIR}/bedrock-facade
-
-git_checkout ${bedrock_facade_CI_BRANCH} ${bedrock_facade_CI_GITURL} ${bedrock_facade_CI_DIR}
-
-( cd ${bedrock_facade_CI_DIR} && make -j ${NJOBS} facade )
diff --git a/dev/ci/ci-bedrock-src.sh b/dev/ci/ci-bedrock-src.sh
deleted file mode 100755
index 532611d4b3..0000000000
--- a/dev/ci/ci-bedrock-src.sh
+++ /dev/null
@@ -1,10 +0,0 @@
-#!/usr/bin/env bash
-
-ci_dir="$(dirname "$0")"
-source ${ci_dir}/ci-common.sh
-
-bedrock_src_CI_DIR=${CI_BUILD_DIR}/bedrock-src
-
-git_checkout ${bedrock_src_CI_BRANCH} ${bedrock_src_CI_GITURL} ${bedrock_src_CI_DIR}
-
-( cd ${bedrock_src_CI_DIR} && make -j ${NJOBS} src )
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 2ecd40416f..b242ce3bd9 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -33,10 +33,6 @@ fi
 echo "DEBUG: ci-user-overlay.sh 0"
 if [ $TRAVIS_PULL_REQUEST = "707" ] || [ $TRAVIS_BRANCH == "trunk__API__coq_makefile" ]; then
     echo "DEBUG: ci-user-overlay.sh 1"
-    bedrock_src_CI_BRANCH=trunk__API
-    bedrock_src_CI_GITURL=https://github.com/matejkosik/bedrock.git
-    bedrock_facade_CI_BRANCH=trunk__API
-    bedrock_facade_CI_GITURL=https://github.com/matejkosik/bedrock.git
     fiat_parsers_CI_BRANCH=trunk__API
     fiat_parsers_CI_GITURL=https://github.com/matejkosik/fiat.git
 fi