From d606a85d53fbd0227b15e18701e2ac4c9d911f34 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 8 Dec 2017 20:00:22 +0100 Subject: CI: poc Circleci configuration --- .circleci/config.yml | 125 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 .circleci/config.yml diff --git a/.circleci/config.yml b/.circleci/config.yml new file mode 100644 index 0000000000..0d797869f9 --- /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 -- cgit v1.2.3 From 319a3c230e9f9ec5a8a5bea9e07b6b8d17444ac9 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 8 Dec 2017 21:43:12 +0100 Subject: Revert "CI: poc Circleci configuration" Committed on master by mistake. Clearly I'm too clumsy to be trusted with push rights. This reverts commit d606a85d53fbd0227b15e18701e2ac4c9d911f34. --- .circleci/config.yml | 125 --------------------------------------------------- 1 file changed, 125 deletions(-) delete mode 100644 .circleci/config.yml diff --git a/.circleci/config.yml b/.circleci/config.yml deleted file mode 100644 index 0d797869f9..0000000000 --- a/.circleci/config.yml +++ /dev/null @@ -1,125 +0,0 @@ -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 -- cgit v1.2.3 From 5d4cf69a3d7d472b54b5decc8400164b87e9a73f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 18:21:38 +0100 Subject: [ci] Temporal workaround for checker non-backwards compatible change. --- dev/ci/ci-compcert.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef3426..7bf2c7427d 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -8,4 +8,5 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +#( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) -- cgit v1.2.3