diff options
Diffstat (limited to '.circleci/config.yml')
| -rw-r--r-- | .circleci/config.yml | 176 |
1 files changed, 53 insertions, 123 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml index 352ec5a51..cff461295 100644 --- a/.circleci/config.yml +++ b/.circleci/config.yml @@ -8,135 +8,73 @@ defaults: # reference syntax) working_directory: ~/coq docker: - - image: ocaml/opam:ubuntu + - image: $CI_REGISTRY_IMAGE:$CACHEKEY environment: &envvars - # required by some of the targets, e.g. compcert, passed for - # instance to opam to configure the number of parallel jobs - # allowed - NJOBS: 2 - COMPILER: "system" - CAMLP5_VER: "6.14" - NATIVE_COMP: "yes" - - # some useful values - TIMING_PACKAGES: &timing-packages "time python" + CACHEKEY: "bionic_coq-V2018-06-04-V2" + CI_REGISTRY_IMAGE: registry.gitlab.com/coq/coq version: 2 before_script: &before_script - name: Install system packages + name: Setup OPAM Switch command: | echo export TERM=xterm >> ~/.profile source ~/.profile - printenv - if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi - -opam-switch: &opam-switch - name: Select opam switch - command: | - source ~/.profile - opam switch ${COMPILER} + echo . ~/.profile >> $BASH_ENV + printenv | sort + opam switch "$COMPILER" opam config list opam list -.opam-boot-template: &opam-boot-template - <<: *params - steps: - - checkout - - run: *before_script - - run: - name: Cache selection - command: | - source ~/.profile - # We can't use environment variables in cache names - # So put it in a file and use the checksum - echo "$COMPILER" > COMPILER - - restore_cache: - keys: - - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- - - coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}- # this grabs old cache if checksum doesn't match - - run: - name: Update opam lists - command: | - source ~/.profile - opam repository set-url default https://opam.ocaml.org - opam update - - run: - name: Install opam packages - command: | - source ~/.profile - opam switch -j ${NJOBS} ${COMPILER} - opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM} - - run: - name: Clean cache - command: | - source ~/.profile - rm -rf ~/.opam/log/ - - save_cache: - key: coq-opam-cache-v1-{{ arch }}-{{ checksum "COMPILER" }}-{{ checksum ".circleci/config.yml" }}- - paths: - - ~/.opam - - persist_to_workspace: - root: &workspace ~/ - paths: - - .opam/ - .build-template: &build-template <<: *params steps: - checkout - run: *before_script - - attach_workspace: &attach_workspace - at: *workspace - - run: *opam-switch + - run: &build-clean + name: Clean + command: | + make clean # ensure that `make clean` works on a fresh clone - run: &build-configure name: Configure command: | - source ~/.profile - ./configure -local -native-compiler ${NATIVE_COMP} -coqide no - run: &build-build name: Build command: | - source ~/.profile make -j ${NJOBS} byte make -j ${NJOBS} make test-suite/misc/universes/all_stdlib.v - persist_to_workspace: - root: *workspace + root: &workspace ~/ paths: - coq/ - environment: *envvars + environment: + <<: *envvars + NATIVE_COMP: "yes" .ci-template: &ci-template <<: *params steps: - run: *before_script - - attach_workspace: *attach_workspace + - attach_workspace: &attach_workspace + at: *workspace + - run: name: Test command: | - source ~/.profile dev/ci/ci-wrapper.sh ${CIRCLE_JOB} - persist_to_workspace: root: *workspace paths: - coq/ - environment: &ci-template-vars - <<: *envvars - EXTRA_PACKAGES: *timing-packages + environment: *envvars # Defines individual jobs, see the workflows section below for job orchestration jobs: - opam-boot: - <<: *opam-boot-template - environment: - <<: *envvars - EXTRA_OPAM: "ocamlgraph ppx_tools_versioned ppx_deriving ocaml-migrate-parsetree" - # Build and prepare test environment build: *build-template @@ -145,24 +83,18 @@ jobs: color: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: *timing-packages compcert: <<: *ci-template coq-dpdgraph: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" coquelicot: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" + + cross-crypto: + <<: *ci-template elpi: <<: *ci-template @@ -173,20 +105,17 @@ jobs: geocoq: <<: *ci-template + fcsl-pcm: + <<: *ci-template + fiat-crypto: <<: *ci-template fiat-parsers: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: *timing-packages flocq: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" math-classes: <<: *ci-template @@ -199,9 +128,6 @@ jobs: hott: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python autoconf automake" iris-lambda-rust: <<: *ci-template @@ -212,11 +138,14 @@ jobs: math-comp: <<: *ci-template + mtac2: + <<: *ci-template + + pidetop: + <<: *ci-template + sf: <<: *ci-template - environment: - <<: *ci-template-vars - EXTRA_PACKAGES: "time python wget" unimath: <<: *ci-template @@ -226,14 +155,11 @@ jobs: workflows: version: 2 + # Run on each push main: jobs: - - opam-boot - - - build: - requires: - - opam-boot + - build - bignums: &req-main requires: @@ -242,19 +168,22 @@ workflows: requires: - build - bignums - - compcert: *req-main - - coq-dpdgraph: *req-main - - coquelicot: *req-main - - elpi: *req-main - - equations: *req-main - - geocoq: *req-main - - fiat-crypto: *req-main - - fiat-parsers: *req-main - - flocq: *req-main + # - compcert: *req-main + # - coq-dpdgraph: *req-main + # - coquelicot: *req-main + # - cross-crypto: *req-main + # - elpi: *req-main + # - equations: *req-main + # - geocoq: *req-main + # - fcsl-pcm: *req-main + # - fiat-crypto: *req-main + # - fiat-parsers: *req-main + # - flocq: *req-main - math-classes: requires: - build - bignums + # - mtac2: *req-main - corn: requires: - build @@ -263,10 +192,11 @@ workflows: requires: - build - corn - - hott: *req-main - - iris-lambda-rust: *req-main - - ltac2: *req-main - - math-comp: *req-main - - sf: *req-main - - unimath: *req-main - - vst: *req-main + # - hott: *req-main + # - iris-lambda-rust: *req-main + # - ltac2: *req-main + # - math-comp: *req-main + # - pidetop: *req-main + # - sf: *req-main + # - unimath: *req-main + # - vst: *req-main |