Skip to content

Commit

Permalink
[ci] add job for interval
Browse files Browse the repository at this point in the history
(cherry picked from commit 6637004)
  • Loading branch information
gares committed Nov 26, 2020
1 parent f376ac1 commit a068228
Show file tree
Hide file tree
Showing 3 changed files with 27 additions and 0 deletions.
16 changes: 16 additions & 0 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -794,6 +794,22 @@ library:ci-flocq:
library:ci-menhir:
extends: .ci-template-flambda

library:ci-interval:
extends: .ci-template-flambda
stage: stage-3
needs:
- build:edge+flambda
- library:ci-coquelicot
- library:ci-flocq
- library:ci-mathcomp
- plugin:ci-bignums
dependencies:
- build:edge+flambda
- library:ci-coquelicot
- library:ci-flocq
- library:ci-mathcomp
- plugin:ci-bignums

library:ci-corn:
extends: .ci-template-flambda
stage: stage-4
Expand Down
3 changes: 3 additions & 0 deletions Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ CI_TARGETS= \
ci-geocoq \
ci-coqhammer \
ci-hott \
ci-interval \
ci-iris \
ci-math_classes \
ci-mathcomp \
Expand Down Expand Up @@ -79,6 +80,8 @@ ci-mtac2: ci-unicoq
ci-fiat_crypto: ci-coqprime ci-rewriter
ci-fiat_crypto_ocaml: ci-fiat_crypto

ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums

ci-simple_io: ci-ext_lib
ci-quickchick: ci-ext_lib ci-simple_io

Expand Down
8 changes: 8 additions & 0 deletions dev/ci/ci-interval.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
#!/usr/bin/env bash

ci_dir="$(dirname "$0")"
. "${ci_dir}/ci-common.sh"

git_download interval

( cd "${CI_BUILD_DIR}/interval" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )

0 comments on commit a068228

Please sign in to comment.