From e5922809138d45fb29677577c7f8822875b5b67b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 8 Dec 2017 20:00:22 +0100
Subject: CI: poc Circleci configuration

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.

CI: poc Circleci configuration

Fixup

Try minimising build for faster testing

Various fixes

Fixup: yaml identation

Do not -j2: native compiler seems to take too much memory

Revert "Do not -j2: native compiler seems to take too much memory"

This reverts commit 4886151288a8d895c0fd23f9bded0970c59e1372.

Deactivate native compiler

Fixup (how did this happen?)

Do not call time (not install on docker images, will fix later)

Fixup

Fixup
---
 .circleci/config.yml | 143 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 143 insertions(+)
 create mode 100644 .circleci/config.yml

diff --git a/.circleci/config.yml b/.circleci/config.yml
new file mode 100644
index 0000000000..cb195f2128
--- /dev/null
+++ b/.circleci/config.yml
@@ -0,0 +1,143 @@
+defaults:
+  params:
+    # Following parameters are used in Coq CircleCI Job (using yaml
+    # reference syntax)
+    working_directory: &workdir ~/coq
+    base_image: &base ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda
+
+  # Job configuration
+  config: &coq
+    working_directory: *workdir
+    docker:
+      - image: *base
+    environment:
+      # required by some of the targets, e.g. compcert, passed for
+      # instance to opam to configure the number of parallel jobs
+      # allowed
+      - NJOBS: 2
+
+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
+      # 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:
+          name: Build opam dependencies
+          command: |
+            # workaround, ought to be fixed in recent opams. See
+            # https://github.com/ocaml/opam/issues/2978
+            export TERM=xterm
+            opam install -y camlp5 ocamlfind
+      - save_cache:
+          key: coq-opam-cache-{{ arch }}-v171208-static-deps
+          paths:
+            - ~/.opam
+      - run:
+          name: Configure
+          command: |
+            # XXX: all this .profile stuff is a shortcoming of the
+            # docker image. To be improved.
+            . ~/.profile
+            ./configure -local -native-compiler no
+      - run:
+          name: Build
+          command: |
+            . ~/.profile
+            make -j2
+      - run:
+          name: Validate
+          command: |
+            . ~/.profile
+            make -j2 validate
+      - persist_to_workspace:
+          root: &workspace ~/
+          paths:
+            - .opam
+            - coq/
+
+  bignums:
+    <<: *coq
+    steps:
+      # Restore workspace
+      - checkout
+      - attach_workspace:
+          at: *workspace
+      - run:
+          name: System dependencies
+          command: |
+            sudo apt-get update
+            sudo apt-get install -y python
+      - run:
+          name: Build
+          command: |
+            . ~/.profile
+            make -j2 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: System dependencies
+          command: |
+            sudo apt-get update
+            sudo apt-get install -y python
+      - run:
+          name: Build
+          command: |
+            . ~/.profile
+            make -j2 ci-color
+
+  compcert:
+    <<: *coq
+    steps:
+      # Restore workspace
+      - checkout
+      - attach_workspace:
+          at: *workspace
+      - run:
+          name: System dependencies
+          command: |
+            sudo apt-get update
+            sudo apt-get install -y python
+      - run:
+          name: Build
+          command: |
+            . ~/.profile
+            make -j2 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 8323ac57d63d3734c5f43b787c97644bf2fce32d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 11 Dec 2017 15:43:34 +0100
Subject: Near-full implementation of Circle CI.

VS gitlab:
+ fiat-crypto (Circle has 4GB RAM, gitlab 2GB)
- caching opam (TODO)
- publishing artefacts (TODO)
* tests with -local, not installed

VS travis:
+ reusing build products
- flambda validate job (TODO?)
- OSX jobs (TODO at least check if free OSX is possible)
- linter (TODO?)
---
 .circleci/config.yml | 475 ++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 354 insertions(+), 121 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index cb195f2128..42df67e711 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -1,143 +1,376 @@
 defaults:
-  params:
+  params: &params
     # Following parameters are used in Coq CircleCI Job (using yaml
     # reference syntax)
-    working_directory: &workdir ~/coq
-    base_image: &base ocaml/opam:ubuntu-16.04_ocaml-4.05.0_flambda
-
-  # Job configuration
-  config: &coq
-    working_directory: *workdir
+    working_directory: ~/coq
     docker:
-      - image: *base
-    environment:
-      # required by some of the targets, e.g. compcert, passed for
-      # instance to opam to configure the number of parallel jobs
-      # allowed
-      - NJOBS: 2
+      - image: ocaml/opam:ubuntu
+
+  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"
+
+    # some useful values
+    COMPILER_32BIT: &compiler-32bit "4.02.3+32bit"
+
+    COMPILER_BLEEDING_EDGE: &compiler-be "4.06.0"
+    CAMLP5_VER_BLEEDING_EDGE: &camlp5-ver-be "7.03"
+
+    TIMING_PACKAGES: &timing-packages "time python"
+
+    COQIDE_PACKAGES: &coqide-packages "libgtk2.0-dev libgtksourceview2.0-dev"
+    #COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
+    COQIDE_OPAM: &coqide-opam "lablgtk-extras"
+    COQIDE_OPAM_BE: &coqide-opam-be "num lablgtk.2.18.6 lablgtk-extras.1.6"
+    COQDOC_PACKAGES: &coqdoc-packages "texlive-latex-base texlive-latex-recommended texlive-latex-extra texlive-math-extra texlive-fonts-recommended texlive-fonts-extra latex-xcolor ghostscript transfig imagemagick tipa"
+    COQDOC_OPAM: &coqdoc-opam "hevea"
 
 version: 2
 
+before_script: &before_script
+  name: before_script
+  command: |
+    source ~/.profile
+    export TERM=xterm
+    ls # figure out if artifacts are around
+    printenv
+    #if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
+    if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi
+
+    # the default repo in this docker image is a local directory
+    # at the time of 4aaeb8abf it lagged behind the official
+    # repository such that camlp5 7.01 was not available
+    opam repository set-url default https://opam.ocaml.org
+    opam update
+    opam switch ${COMPILER}
+    eval $(opam config env)
+    opam config list
+    opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
+    rm -rf ~/.opam/log/
+    opam list
+
+.build-template: &build-template
+  <<: *params
+  steps:
+    - checkout
+    # - restore_cache:
+    #     key: coq-opam-cache-{{ arch }}-v171208-
+    - run: *before_script
+    # - save_cache:
+    #     key: coq-opam-cache-{{ arch }}-v171208-static-deps
+    #     paths:
+    #       - ~/.opam
+    - run: &build-configure
+        name: Configure
+        command: |
+          source ~/.profile
+
+          echo 'start:coq.config'
+          ./configure -local -native-compiler no ${EXTRA_CONF}
+          echo 'end:coq.config'
+    - run: &build-build
+        name: Build
+        command: |
+          source ~/.profile
+          echo 'start:coq.build'
+          make -j ${NJOBS} byte
+          make -j ${NJOBS}
+          make test-suite/misc/universes/all_stdlib.v
+          echo 'end:coq:build'
+    - persist_to_workspace:
+        root: &workspace ~/
+        paths:
+          - .opam
+          - coq/
+
+  environment: &build-variables
+    <<: *envvars
+    EXTRA_CONF: "-coqide opt"
+    EXTRA_PACKAGES: *coqide-packages
+    EXTRA_OPAM: *coqide-opam
+
+.validate-template: &validate-template
+  <<: *params
+  steps:
+    - checkout
+    - attach_workspace:
+        at: *workspace
+    - run: *before_script
+    - run:
+        name: Validate
+        command: |
+          source ~/.profile
+          make validate
+  environment: *envvars
+
+.documentation-template: &documentation-template
+  <<: *params
+  steps:
+    - checkout
+    - attach_workspace:
+        at: *workspace
+    - run: *before_script
+    - run:
+        name: Documentation
+        command: |
+          source ~/.profile
+          make -j ${NJOBS} doc
+  environment: &documentation-variables
+    <<: *envvars
+    EXTRA_PACKAGES: *coqdoc-packages
+    EXTRA_OPAM: *coqdoc-opam
+
+.test-suite-template: &test-suite-template
+  <<: *params
+  steps:
+    - checkout
+    - attach_workspace:
+        at: *workspace
+    - run: *before_script
+    - run:
+        name: Test
+        command: |
+          source ~/.profile
+          cd test-suite
+          make clean
+          make -j ${NJOBS} all
+  environment: &test-suite-variables
+    <<: *envvars
+    EXTRA_PACKAGES: *timing-packages
+
+.warnings-template: &warnings-template
+  <<: *params
+  steps:
+    - checkout
+    - run: *before_script
+    - run:
+        name: Configure
+        command: |
+          source ~/.profile
+          ./configure -local ${EXTRA_CONF}
+
+    - run:
+        name: Build
+        command: |
+          source ~/.profile
+          make -j ${NJOBS} coqocaml
+  environment: &warnings-variables
+    <<: *envvars
+    EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"
+    EXTRA_PACKAGES: *coqide-packages
+    EXTRA_OPAM: *coqide-opam
+
+.ci-template: &ci-template
+  <<: *params
+  steps:
+    - checkout
+    - attach_workspace:
+        at: *workspace
+    - run: *before_script
+    - run:
+        name: Test
+        command: |
+          source ~/.profile
+          echo 'start:coq.test'
+          make -f Makefile.ci -j ${NJOBS} ${CIRCLE_JOB}
+          echo 'end:coq.test'
+  environment: &ci-template-vars
+    <<: *envvars
+    EXTRA_PACKAGES: *timing-packages
+
 # Defines individual jobs, see the workflows section below for job orchestration
 jobs:
   # TODO: linter
 
   # Build and prepare test environment
-  build:
-    <<: *coq
-    steps:
-      - checkout
-      # 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:
-          name: Build opam dependencies
-          command: |
-            # workaround, ought to be fixed in recent opams. See
-            # https://github.com/ocaml/opam/issues/2978
-            export TERM=xterm
-            opam install -y camlp5 ocamlfind
-      - save_cache:
-          key: coq-opam-cache-{{ arch }}-v171208-static-deps
-          paths:
-            - ~/.opam
-      - run:
-          name: Configure
-          command: |
-            # XXX: all this .profile stuff is a shortcoming of the
-            # docker image. To be improved.
-            . ~/.profile
-            ./configure -local -native-compiler no
-      - run:
-          name: Build
-          command: |
-            . ~/.profile
-            make -j2
-      - run:
-          name: Validate
-          command: |
-            . ~/.profile
-            make -j2 validate
-      - persist_to_workspace:
-          root: &workspace ~/
-          paths:
-            - .opam
-            - coq/
-
-  bignums:
-    <<: *coq
-    steps:
-      # Restore workspace
-      - checkout
-      - attach_workspace:
-          at: *workspace
-      - run:
-          name: System dependencies
-          command: |
-            sudo apt-get update
-            sudo apt-get install -y python
-      - run:
-          name: Build
-          command: |
-            . ~/.profile
-            make -j2 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: System dependencies
-          command: |
-            sudo apt-get update
-            sudo apt-get install -y python
-      - run:
-          name: Build
-          command: |
-            . ~/.profile
-            make -j2 ci-color
-
-  compcert:
-    <<: *coq
-    steps:
-      # Restore workspace
-      - checkout
-      - attach_workspace:
-          at: *workspace
-      - run:
-          name: System dependencies
-          command: |
-            sudo apt-get update
-            sudo apt-get install -y python
-      - run:
-          name: Build
-          command: |
-            . ~/.profile
-            make -j2 ci-compcert
+  build: *build-template
+
+  build-32bit:
+    <<: *build-template
+    environment:
+      <<: *envvars # no coqide for 32bit
+      EXTRA_PACKAGES: "gcc-multilib"
+      COMPILER: *compiler-32bit
+
+  build-be:
+    <<: *build-template
+    environment:
+      <<: *build-variables
+      COMPILER: *compiler-be
+      CAMLP5_VER: *camlp5-ver-be
+      EXTRA_OPAM: *coqide-opam-be
+
+  validate: *validate-template
+
+  validate-32bit:
+    <<: *validate-template
+    environment:
+      <<: *envvars
+      COMPILER: *compiler-32bit
+      EXTRA_PACKAGES: "gcc-multilib"
+
+  warnings: *warnings-template
+
+  warnings-be:
+    <<: *warnings-template
+    environment:
+      <<: *warnings-variables
+      COMPILER: *compiler-be
+      CAMLP5_VER: *camlp5-ver-be
+      EXTRA_OPAM: *coqide-opam-be
+
+  documentation: *documentation-template
+
+  documentation-be:
+    <<: *documentation-template
+    environment:
+      <<: *documentation-variables
+      COMPILER: *compiler-be
+      CAMLP5_VER: *camlp5-ver-be
+
+  test-suite:
+    <<: *test-suite-template
+
+  test-suite-32bit:
+    <<: *test-suite-template
+    environment:
+      <<: *test-suite-variables
+      COMPILER: *compiler-32bit
+      EXTRA_PACKAGES: "gcc-multilib time python"
+
+  test-suite-be:
+    <<: *test-suite-template
+    environment:
+      <<: *test-suite-variables
+      COMPILER: *compiler-be
+      CAMLP5_VER: *camlp5-ver-be
+      EXTRA_PACKAGES: *timing-packages
+
+  ci-bignums:
+    <<: *ci-template
+
+  ci-color:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: *timing-packages
+
+  ci-compcert:
+    <<: *ci-template
+
+  ci-coq-dpdgraph:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_OPAM: "ocamlgraph"
+      EXTRA_PACKAGES: "time python autoconf automake"
+
+  ci-coquelicot:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: "time python autoconf automake"
+
+  ci-equations:
+    <<: *ci-template
+
+  ci-geocoq:
+    <<: *ci-template
+
+  ci-fiat-crypto:
+    <<: *ci-template
+
+  ci-fiat-parsers:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: *timing-packages
+
+  ci-flocq:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: "time python autoconf automake"
+
+  ci-formal-topology:
+    <<: *ci-template
+
+  ci-hott:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: "time python autoconf automake"
+
+  ci-iris-lambda-rust:
+    <<: *ci-template
+
+  ci-ltac2:
+    <<: *ci-template
+
+  ci-math-comp:
+    <<: *ci-template
+
+  ci-sf:
+    <<: *ci-template
+    environment:
+      <<: *ci-template-vars
+      EXTRA_PACKAGES: "time python wget"
+
+  ci-unimath:
+    <<: *ci-template
+
+  ci-vst:
+    <<: *ci-template
 
 workflows:
   version: 2
   # Run on each push
-  ci:
+  main:
     jobs:
       - build
-      - bignums:
+      - warnings
+      - validate: &req-main
           requires:
             - build
-      - color:
+      - test-suite: *req-main
+      - documentation: *req-main
+
+      - ci-bignums: *req-main
+      - ci-color: *req-main
+      - ci-compcert: *req-main
+      - ci-coq-dpdgraph: *req-main
+      - ci-coquelicot: *req-main
+      - ci-equations: *req-main
+      - ci-geocoq: *req-main
+      - ci-fiat-crypto: *req-main
+      - ci-fiat-parsers: *req-main
+      - ci-flocq: *req-main
+      - ci-formal-topology: *req-main
+      - ci-hott: *req-main
+      - ci-iris-lambda-rust: *req-main
+      - ci-ltac2: *req-main
+      - ci-math-comp: *req-main
+      - ci-sf: *req-main
+      - ci-unimath: *req-main
+      - ci-vst: *req-main
+
+  # 32bit:
+  #   jobs:
+      - build-32bit
+      - validate-32bit: &req-32bit
           requires:
-            - build
-            - bignums
-      - compcert:
+            - build-32bit
+      - test-suite-32bit: *req-32bit
+
+  # bleeding-edge:
+  #   jobs:
+      - build-be
+      - warnings-be
+      - test-suite-be: &req-be
           requires:
-            - build
+            - build-be
+      - documentation-be: *req-be
-- 
cgit v1.2.3


From c2b7b15526f0c8b87b9442567ddfa0e133cfebcf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 13:26:59 +0100
Subject: Circle CI: enable native compiler.

---
 .circleci/config.yml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 42df67e711..fecabd7bc9 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -13,6 +13,7 @@ defaults:
     NJOBS: 2
     COMPILER: "system"
     CAMLP5_VER: "6.14"
+    NATIVE_COMP: "yes"
 
     # some useful values
     COMPILER_32BIT: &compiler-32bit "4.02.3+32bit"
@@ -70,7 +71,7 @@ before_script: &before_script
           source ~/.profile
 
           echo 'start:coq.config'
-          ./configure -local -native-compiler no ${EXTRA_CONF}
+          ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
           echo 'end:coq.config'
     - run: &build-build
         name: Build
@@ -151,7 +152,7 @@ before_script: &before_script
         name: Configure
         command: |
           source ~/.profile
-          ./configure -local ${EXTRA_CONF}
+          ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
 
     - run:
         name: Build
@@ -160,7 +161,7 @@ before_script: &before_script
           make -j ${NJOBS} coqocaml
   environment: &warnings-variables
     <<: *envvars
-    EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only"
+    EXTRA_CONF: "-coqide byte -byte-only"
     EXTRA_PACKAGES: *coqide-packages
     EXTRA_OPAM: *coqide-opam
 
-- 
cgit v1.2.3


From 4d11d6dc3bfcef3ecdf3f905dcf2fdbca259677e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 13:42:59 +0100
Subject: Circle CI: use cache for opam

---
 .circleci/config.yml | 55 +++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 48 insertions(+), 7 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index fecabd7bc9..7b68a0711e 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -58,13 +58,15 @@ before_script: &before_script
   <<: *params
   steps:
     - checkout
-    # - restore_cache:
-    #     key: coq-opam-cache-{{ arch }}-v171208-
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
-    # - save_cache:
-    #     key: coq-opam-cache-{{ arch }}-v171208-static-deps
-    #     paths:
-    #       - ~/.opam
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run: &build-configure
         name: Configure
         command: |
@@ -85,7 +87,6 @@ before_script: &before_script
     - persist_to_workspace:
         root: &workspace ~/
         paths:
-          - .opam
           - coq/
 
   environment: &build-variables
@@ -100,7 +101,15 @@ before_script: &before_script
     - checkout
     - attach_workspace:
         at: *workspace
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run:
         name: Validate
         command: |
@@ -114,7 +123,15 @@ before_script: &before_script
     - checkout
     - attach_workspace:
         at: *workspace
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run:
         name: Documentation
         command: |
@@ -131,7 +148,15 @@ before_script: &before_script
     - checkout
     - attach_workspace:
         at: *workspace
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run:
         name: Test
         command: |
@@ -147,7 +172,15 @@ before_script: &before_script
   <<: *params
   steps:
     - checkout
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run:
         name: Configure
         command: |
@@ -171,7 +204,15 @@ before_script: &before_script
     - checkout
     - attach_workspace:
         at: *workspace
+    - restore_cache:
+        keys:
+          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
+    - save_cache:
+        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        paths:
+          - ~/.opam
     - run:
         name: Test
         command: |
-- 
cgit v1.2.3


From cef0430e14c370e6cbfe72db75e61cb4b8c8a8b9 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 15:05:10 +0100
Subject: Circle CI: enable TIMED for external developments

---
 .circleci/config.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 7b68a0711e..718bd6b5e7 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -218,7 +218,7 @@ before_script: &before_script
         command: |
           source ~/.profile
           echo 'start:coq.test'
-          make -f Makefile.ci -j ${NJOBS} ${CIRCLE_JOB}
+          make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB}
           echo 'end:coq.test'
   environment: &ci-template-vars
     <<: *envvars
-- 
cgit v1.2.3


From f10d9fefdaf694253495c1ecf2e57ce5099b9375 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 15:13:17 +0100
Subject: Put bignums, math-classes and corn dependencies in Makefile

---
 Makefile.ci                  | 20 ++++++++++++++++++--
 dev/ci/ci-color.sh           |  3 ---
 dev/ci/ci-corn.sh            | 10 ++++++++++
 dev/ci/ci-formal-topology.sh | 22 ----------------------
 dev/ci/ci-math-classes.sh    | 14 --------------
 dev/ci/ci-wrapper.sh         |  5 ++++-
 6 files changed, 32 insertions(+), 42 deletions(-)
 create mode 100755 dev/ci/ci-corn.sh

diff --git a/Makefile.ci b/Makefile.ci
index a17d4ddf75..2a6222e222 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -4,6 +4,7 @@ CI_TARGETS=ci-all \
     ci-compcert \
     ci-coq-dpdgraph \
     ci-coquelicot \
+    ci-corn \
     ci-cpdt \
     ci-equations \
     ci-fiat-crypto \
@@ -24,6 +25,21 @@ CI_TARGETS=ci-all \
 
 .PHONY: $(CI_TARGETS)
 
+_build_ci/.ci-%.done:
+	+./dev/ci/ci-wrapper.sh $*
+
+ci-color: ci-bignums
+
+ci-math-classes: ci-bignums
+
+ci-corn: ci-math-classes
+
+ci-formal-topology: ci-corn
+
 # Generic rule, we use make to ease travis integration with mixed rules
-$(CI_TARGETS): ci-%:
-	+./dev/ci/ci-wrapper.sh ci-$*.sh
+$(CI_TARGETS): ci-%: _build_ci/.ci-%.done
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End:
diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh
index c3ae7552a9..558e8cbb8c 100755
--- a/dev/ci/ci-color.sh
+++ b/dev/ci/ci-color.sh
@@ -5,9 +5,6 @@ source ${ci_dir}/ci-common.sh
 
 CoLoR_CI_DIR=${CI_BUILD_DIR}/color
 
-# Setup Bignums
-source ${ci_dir}/ci-bignums.sh
-
 # Compile CoLoR
 git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR}
 ( cd ${CoLoR_CI_DIR} && make )
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
new file mode 100755
index 0000000000..54cad5df4c
--- /dev/null
+++ b/dev/ci/ci-corn.sh
@@ -0,0 +1,10 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+source ${ci_dir}/ci-common.sh
+
+Corn_CI_DIR=${CI_BUILD_DIR}/corn
+
+git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
+
+( cd ${Corn_CI_DIR} && make && make install )
diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh
index 2556f84a55..53eb55fc45 100755
--- a/dev/ci/ci-formal-topology.sh
+++ b/dev/ci/ci-formal-topology.sh
@@ -3,30 +3,8 @@
 ci_dir="$(dirname "$0")"
 source ${ci_dir}/ci-common.sh
 
-math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
-
-Corn_CI_DIR=${CI_BUILD_DIR}/corn
-
 formal_topology_CI_DIR=${CI_BUILD_DIR}/formal-topology
 
-# Setup Bignums
-
-source ${ci_dir}/ci-bignums.sh
-
-# Setup Math-Classes
-
-git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
-
-( cd ${math_classes_CI_DIR} && make && make install )
-
-# Setup Corn
-
-git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-
-( cd ${Corn_CI_DIR} && make && make install )
-
-# Setup formal-topology
-
 git_checkout ${formal_topology_CI_BRANCH} ${formal_topology_CI_GITURL} ${formal_topology_CI_DIR}
 
 ( cd ${formal_topology_CI_DIR} && make )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh
index 2837dee963..db4a31e549 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math-classes.sh
@@ -5,20 +5,6 @@ source ${ci_dir}/ci-common.sh
 
 math_classes_CI_DIR=${CI_BUILD_DIR}/math-classes
 
-Corn_CI_DIR=${CI_BUILD_DIR}/corn
-
-# Setup Bignums
-
-source ${ci_dir}/ci-bignums.sh
-
-# Setup Math-Classes
-
 git_checkout ${math_classes_CI_BRANCH} ${math_classes_CI_GITURL} ${math_classes_CI_DIR}
 
 ( cd ${math_classes_CI_DIR} && make && make install )
-
-# Setup Corn
-
-git_checkout ${Corn_CI_BRANCH} ${Corn_CI_GITURL} ${Corn_CI_DIR}
-
-( cd ${Corn_CI_DIR} && make )
diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 96acc5a11c..a21bf9f38c 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -13,7 +13,8 @@ function travis_fold {
     fi
 }
 
-CI_SCRIPT="$1"
+CI_NAME="$1"
+CI_SCRIPT="ci-${CI_NAME}.sh"
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 # assume this script is in dev/ci/, cd to the root Coq directory
 cd "${DIR}/../.."
@@ -22,3 +23,5 @@ cd "${DIR}/../.."
 travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
 travis_fold 'end' 'coq.test.timing'
+
+touch "_build_ci/.ci-${CI_NAME}.done"
-- 
cgit v1.2.3


From eced3ec17e156a6cf5c96822bc675b353a9b0168 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 15:16:04 +0100
Subject: Circle CI: uses dependencies between external developments.

---
 .circleci/config.yml | 30 +++++++++++++++++++++++++++---
 1 file changed, 27 insertions(+), 3 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 718bd6b5e7..437f5cd2e9 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -220,7 +220,11 @@ before_script: &before_script
           echo 'start:coq.test'
           make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB}
           echo 'end:coq.test'
-  environment: &ci-template-vars
+    - persist_to_workspace:
+        root: &workspace ~/
+        paths:
+          - coq/
+environment: &ci-template-vars
     <<: *envvars
     EXTRA_PACKAGES: *timing-packages
 
@@ -338,6 +342,12 @@ jobs:
       <<: *ci-template-vars
       EXTRA_PACKAGES: "time python autoconf automake"
 
+  ci-math-classes:
+    <<: *ci-template
+
+  ci-corn:
+    <<: *ci-template
+
   ci-formal-topology:
     <<: *ci-template
 
@@ -382,7 +392,10 @@ workflows:
       - documentation: *req-main
 
       - ci-bignums: *req-main
-      - ci-color: *req-main
+      - ci-color:
+          requires:
+            - build
+            - ci-bignums
       - ci-compcert: *req-main
       - ci-coq-dpdgraph: *req-main
       - ci-coquelicot: *req-main
@@ -391,7 +404,18 @@ workflows:
       - ci-fiat-crypto: *req-main
       - ci-fiat-parsers: *req-main
       - ci-flocq: *req-main
-      - ci-formal-topology: *req-main
+      - ci-math-classes:
+          requires:
+            - build
+            - ci-bignums
+      - ci-corn:
+          requires:
+            - build
+            - ci-math-classes
+      - ci-formal-topology:
+          requires:
+            - build
+            - ci-corn
       - ci-hott: *req-main
       - ci-iris-lambda-rust: *req-main
       - ci-ltac2: *req-main
-- 
cgit v1.2.3


From f5adde067368cd6d0b3470be1253cb3629bad2c1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 16:49:26 +0100
Subject: Circle CI: cat failed test suite logs

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6865dcc768..dbd63a57b8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -177,7 +177,7 @@ summary.log:
 report: summary.log
 	$(HIDE)bash save-logs.sh
 	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi
-	$(HIDE)if [ -n "${APPVEYOR}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi
+	$(HIDE)if [ "(" -n "${APPVEYOR}" ")" -o "(" -n "${CIRCLECI}" ")" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
 
 #######################################################################
-- 
cgit v1.2.3


From 7fc585a30ee5aaeb3463eb0c5dc317ffcee3ce53 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 17:07:17 +0100
Subject: Circle CI: remove warning jobs

---
 .circleci/config.yml | 46 ----------------------------------------------
 1 file changed, 46 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 437f5cd2e9..96e9358766 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -168,36 +168,6 @@ before_script: &before_script
     <<: *envvars
     EXTRA_PACKAGES: *timing-packages
 
-.warnings-template: &warnings-template
-  <<: *params
-  steps:
-    - checkout
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
-    - run: *before_script
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
-    - run:
-        name: Configure
-        command: |
-          source ~/.profile
-          ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
-
-    - run:
-        name: Build
-        command: |
-          source ~/.profile
-          make -j ${NJOBS} coqocaml
-  environment: &warnings-variables
-    <<: *envvars
-    EXTRA_CONF: "-coqide byte -byte-only"
-    EXTRA_PACKAGES: *coqide-packages
-    EXTRA_OPAM: *coqide-opam
-
 .ci-template: &ci-template
   <<: *params
   steps:
@@ -259,16 +229,6 @@ jobs:
       COMPILER: *compiler-32bit
       EXTRA_PACKAGES: "gcc-multilib"
 
-  warnings: *warnings-template
-
-  warnings-be:
-    <<: *warnings-template
-    environment:
-      <<: *warnings-variables
-      COMPILER: *compiler-be
-      CAMLP5_VER: *camlp5-ver-be
-      EXTRA_OPAM: *coqide-opam-be
-
   documentation: *documentation-template
 
   documentation-be:
@@ -384,7 +344,6 @@ workflows:
   main:
     jobs:
       - build
-      - warnings
       - validate: &req-main
           requires:
             - build
@@ -424,18 +383,13 @@ workflows:
       - ci-unimath: *req-main
       - ci-vst: *req-main
 
-  # 32bit:
-  #   jobs:
       - build-32bit
       - validate-32bit: &req-32bit
           requires:
             - build-32bit
       - test-suite-32bit: *req-32bit
 
-  # bleeding-edge:
-  #   jobs:
       - build-be
-      - warnings-be
       - test-suite-be: &req-be
           requires:
             - build-be
-- 
cgit v1.2.3


From 81e0ef590172c8eeed7b3c5e5b4290010557dc48 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 13 Dec 2017 17:38:56 +0100
Subject: Circle CI: separate job to boot opam with all used packages.

---
 .circleci/config.yml | 164 +++++++++++++++++++++++++++------------------------
 1 file changed, 86 insertions(+), 78 deletions(-)

diff --git a/.circleci/config.yml b/.circleci/config.yml
index 96e9358766..7c250c667e 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -33,59 +33,80 @@ defaults:
 version: 2
 
 before_script: &before_script
-  name: before_script
+  name: Install system packages
   command: |
+    echo export TERM=xterm >> ~/.profile
     source ~/.profile
-    export TERM=xterm
-    ls # figure out if artifacts are around
     printenv
     #if [ "$COMPILER" = "$COMPILER_32BIT" ]; then sudo dpkg --add-architecture i386; fi
     if [ -n "${EXTRA_PACKAGES}" ]; then sudo apt-get update -yq && sudo apt-get install -yq --no-install-recommends ${EXTRA_PACKAGES}; fi
 
-    # the default repo in this docker image is a local directory
-    # at the time of 4aaeb8abf it lagged behind the official
-    # repository such that camlp5 7.01 was not available
-    opam repository set-url default https://opam.ocaml.org
-    opam update
+opam-switch: &opam-switch
+  name: Select opam switch
+  command: |
+    source ~/.profile
     opam switch ${COMPILER}
-    eval $(opam config env)
     opam config list
-    opam install -j ${NJOBS} -y camlp5.${CAMLP5_VER} ocamlfind ${EXTRA_OPAM}
-    rm -rf ~/.opam/log/
     opam list
 
-.build-template: &build-template
+.opam-boot-template: &opam-boot-template
   <<: *params
   steps:
     - checkout
+    - run: *before_script
     - restore_cache:
         keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
-    - run: *before_script
+          - coq-opam-cache-v1-{{ arch }}-{{ .Environment.COMPILER }}-{{ checksum ".circleci/config.yml" }}-
+          - coq-opam-cache-v1-{{ arch }}-{{ .Environment.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 ${COQIDE_OPAM} ${COQDOC_OPAM} ${EXTRA_OPAM}
+    - run:
+        name: Clean cache
+        command: |
+          source ~/.profile
+          rm -rf ~/.opam/log/
     - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
+        key: coq-opam-cache-v1-{{ arch }}-{{ .Environment.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-configure
         name: Configure
         command: |
           source ~/.profile
 
-          echo 'start:coq.config'
           ./configure -local -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
-          echo 'end:coq.config'
     - run: &build-build
         name: Build
         command: |
           source ~/.profile
-          echo 'start:coq.build'
           make -j ${NJOBS} byte
           make -j ${NJOBS}
           make test-suite/misc/universes/all_stdlib.v
-          echo 'end:coq:build'
     - persist_to_workspace:
-        root: &workspace ~/
+        root: *workspace
         paths:
           - coq/
 
@@ -93,23 +114,12 @@ before_script: &before_script
     <<: *envvars
     EXTRA_CONF: "-coqide opt"
     EXTRA_PACKAGES: *coqide-packages
-    EXTRA_OPAM: *coqide-opam
 
 .validate-template: &validate-template
   <<: *params
   steps:
-    - checkout
-    - attach_workspace:
-        at: *workspace
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
+    - attach_workspace: *attach_workspace
     - run:
         name: Validate
         command: |
@@ -120,18 +130,8 @@ before_script: &before_script
 .documentation-template: &documentation-template
   <<: *params
   steps:
-    - checkout
-    - attach_workspace:
-        at: *workspace
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
+    - attach_workspace: *attach_workspace
     - run:
         name: Documentation
         command: |
@@ -140,23 +140,12 @@ before_script: &before_script
   environment: &documentation-variables
     <<: *envvars
     EXTRA_PACKAGES: *coqdoc-packages
-    EXTRA_OPAM: *coqdoc-opam
 
 .test-suite-template: &test-suite-template
   <<: *params
   steps:
-    - checkout
-    - attach_workspace:
-        at: *workspace
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
+    - attach_workspace: *attach_workspace
     - run:
         name: Test
         command: |
@@ -171,30 +160,18 @@ before_script: &before_script
 .ci-template: &ci-template
   <<: *params
   steps:
-    - checkout
-    - attach_workspace:
-        at: *workspace
-    - restore_cache:
-        keys:
-          - coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-          - coq-opam-cache-v1-{{ arch }}- # this grabs old cache if checksum doesn't match
     - run: *before_script
-    - save_cache:
-        key: coq-opam-cache-v1-{{ arch }}-{{ checksum ".circleci/config.yml" }}-
-        paths:
-          - ~/.opam
+    - attach_workspace: *attach_workspace
     - run:
         name: Test
         command: |
           source ~/.profile
-          echo 'start:coq.test'
           make -f Makefile.ci -j ${NJOBS} TIMED=1 ${CIRCLE_JOB}
-          echo 'end:coq.test'
     - persist_to_workspace:
-        root: &workspace ~/
+        root: *workspace
         paths:
           - coq/
-environment: &ci-template-vars
+  environment: &ci-template-vars
     <<: *envvars
     EXTRA_PACKAGES: *timing-packages
 
@@ -202,6 +179,31 @@ environment: &ci-template-vars
 jobs:
   # TODO: linter
 
+  opam-boot:
+    <<: *opam-boot-template
+    environment:
+      <<: *envvars
+      EXTRA_PACKAGES: *coqide-packages
+      EXTRA_OPAM: "ocamlgraph"
+
+  opam-boot-32bit:
+    <<: *opam-boot-template
+    environment:
+      <<: *envvars
+      EXTRA_PACKAGES: "gcc-multilib"
+      COMPILER: *compiler-32bit
+      COQIDE_OPAM: ""
+      COQDOC_OPAM: ""
+
+  opam-boot-be:
+    <<: *opam-boot-template
+    environment:
+      <<: *envvars
+      EXTRA_PACKAGES: *coqide-packages
+      COMPILER: *compiler-be
+      CAMLP5_VER: *camlp5-ver-be
+      COQIDE_OPAM: *coqide-opam-be
+
   # Build and prepare test environment
   build: *build-template
 
@@ -217,8 +219,6 @@ jobs:
     environment:
       <<: *build-variables
       COMPILER: *compiler-be
-      CAMLP5_VER: *camlp5-ver-be
-      EXTRA_OPAM: *coqide-opam-be
 
   validate: *validate-template
 
@@ -253,7 +253,6 @@ jobs:
     environment:
       <<: *test-suite-variables
       COMPILER: *compiler-be
-      CAMLP5_VER: *camlp5-ver-be
       EXTRA_PACKAGES: *timing-packages
 
   ci-bignums:
@@ -272,7 +271,6 @@ jobs:
     <<: *ci-template
     environment:
       <<: *ci-template-vars
-      EXTRA_OPAM: "ocamlgraph"
       EXTRA_PACKAGES: "time python autoconf automake"
 
   ci-coquelicot:
@@ -343,7 +341,13 @@ workflows:
   # Run on each push
   main:
     jobs:
-      - build
+      - opam-boot
+      - opam-boot-32bit
+      - opam-boot-be
+
+      - build:
+          requires:
+            - opam-boot
       - validate: &req-main
           requires:
             - build
@@ -383,13 +387,17 @@ workflows:
       - ci-unimath: *req-main
       - ci-vst: *req-main
 
-      - build-32bit
+      - build-32bit:
+          requires:
+            - opam-boot-32bit
       - validate-32bit: &req-32bit
           requires:
             - build-32bit
       - test-suite-32bit: *req-32bit
 
-      - build-be
+      - build-be:
+          requires:
+            - opam-boot-be
       - test-suite-be: &req-be
           requires:
             - build-be
-- 
cgit v1.2.3


From 653df5afeafab4c08c2fd436636e549d31a2fa9f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 14 Dec 2017 12:56:54 +0100
Subject: Circle CI: add badge to README.

---
 README.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 490c619cb6..30911e78e8 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,10 @@
 # Coq
 
-[![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) [![Build status](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master) [![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
+- [![Travis](https://travis-ci.org/coq/coq.svg?branch=master)](https://travis-ci.org/coq/coq/builds) Travis CI
+- [![Appveyor](https://ci.appveyor.com/api/projects/status/eln43k05pa2vm908/branch/master?svg=true)](https://ci.appveyor.com/project/coq/coq/branch/master) Appveyor CI (Windows)
+- [![Circle CI](https://circleci.com/gh/SkySkimmer/coq/tree/circle-ci.svg?style=shield&circle-token=70b9a75b750778d8b252afe18a81de7c4cd0299b)](https://circleci.com/gh/SkySkimmer/workflows/coq) Circle CI
+
+[![Gitter](https://badges.gitter.im/coq/coq.svg)](https://gitter.im/coq/coq)
 
 Coq is a formal proof management system. It provides a formal language to write
 mathematical definitions, executable algorithms and theorems together with an
-- 
cgit v1.2.3