diff options
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | Makefile.ci | 3 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-formal-topology.sh | 8 |
4 files changed, 1 insertions, 19 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index f131a97ba5..881f474d1d 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -485,7 +485,7 @@ library:ci-fiat-crypto-legacy: library:ci-flocq: <<: *ci-template -library:ci-formal-topology: +library:ci-corn: <<: *ci-template-flambda library:ci-geocoq: diff --git a/Makefile.ci b/Makefile.ci index 2df6a792b6..6805304f55 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -27,7 +27,6 @@ CI_TARGETS= \ ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ - ci-formal-topology \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -63,8 +62,6 @@ ci-corn: ci-math-classes ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io -ci-formal-topology: ci-corn - # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..e4a18ce884 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,13 +150,6 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology -######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" - -######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) |