diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2017-12-08 20:00:22 +0100 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2017-12-08 21:32:56 +0100 |
| commit | d606a85d53fbd0227b15e18701e2ac4c9d911f34 (patch) | |
| tree | be82d4ceccc9adb31233ab3e5ce96ed4b7086a40 | |
| parent | 7b40908bfbc255d51384e88a73fa5d98380b237f (diff) | |
CI: poc Circleci configuration
| -rw-r--r-- | .circleci/config.yml | 125 |
1 files changed, 125 insertions, 0 deletions
diff --git a/.circleci/config.yml b/.circleci/config.yml new file mode 100644 index 000000000..0d797869f --- /dev/null +++ b/.circleci/config.yml @@ -0,0 +1,125 @@ +defaults: + params: + # Following parameters are used in Coq CircleCI Job (using yaml + # reference syntax) + working_directory: &workdir ~/coq + base_image: &base opam:ubuntu-16.04_ocaml-4.05.0_flambda + + # Job configuration + config: &coq + working_directory: *workdir + docker: + - image: *base + +version: 2 + +# Defines individual jobs, see the workflows section below for job orchestration +jobs: + # TODO: linter + + # Build and prepare test environment + build: + <<: *coq + steps: + - checkout + - run: + name: Install system dependencies for build + command: | + apt-get update && apt-get install -y + aspcud \ + libgtk2.0-dev \ + libgtksourceview2.0-dev \ + texlive-latex-base \ + texlive-latex-recommended \ + texlive-latex-extra \ + texlive-math-extra \ + texlive-fonts-recommended \ + texlive-fonts-extra \ + latex-xcolor \ + ghostscript \ + transfig \ + imagemagick \ + tipa + # Restore last version of the dependencies in cache When a new + # major version of caches has to be generated, please use + # vYYMMDD format to avoid collision. + - restore_cache: + key: coq-opam-cache-{{ arch }}-v171208- + - run: + - run: + name: Build opam dependencies + command: | + opam install -y camlp5 ocamlfind hevea lablgtk lablgtk-extras + - save_cache: + key: coq-opam-cache-{{ arch }}-v171208-static-deps + paths: + - ~/.opam + - run: + name: Configure + command: ./configure -local + - run: + name: Build -j2 + command: make + - run: + name: Validate + command: make -j2 validate + - persist_to_workspace: + root: &workspace ~/ + paths: + - .opam + - coq/ + + bignums: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: Build + command: make -j2 TIMED=1 ci-bignums + # bignums is a dependency + - persist_to_workspace: + root: &workspace ~/ + paths: + - coq/ + + color: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: Build + command: make -j2 TIMED=1 ci-color + + compcert: + <<: *coq + steps: + # Restore workspace + - checkout + - attach_workspace: + at: *workspace + - run: + name: Build + command: make -j2 TIMED=1 ci-compcert + +workflows: + version: 2 + # Run on each push + ci: + jobs: + - build + - bignums: + requires: + - build + - color: + requires: + - build + - bignums + - compcert: + requires: + - build |