path: root/.circleci/config.yml

# This file used to contain configuration to also build documentation and CoqIDE,
# run the test-suite and the validate targets,
# including with 32-bits architecture or bleeding-edge compiler.

defaults:
  params: &params
    # Following parameters are used in Coq CircleCI Job (using yaml
    # reference syntax)
    working_directory: ~/coq
    docker:
      - 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"
    NATIVE_COMP: "yes"

    # some useful values
    TIMING_PACKAGES: &timing-packages "time python"

version: 2

before_script: &before_script
  name: Install system packages
  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}
    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-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
        paths:
          - coq/

  environment: *envvars

.ci-template: &ci-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: *attach_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

# 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

  bignums:
    <<: *ci-template

  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"

  elpi:
    <<: *ci-template

  equations:
    <<: *ci-template

  geocoq:
    <<: *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

  corn:
    <<: *ci-template

  formal-topology:
    <<: *ci-template

  hott:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python autoconf automake"

  iris-lambda-rust:
    <<: *ci-template

  ltac2:
    <<: *ci-template

  math-comp:
    <<: *ci-template

  sf:
    <<: *ci-template
    environment:
      <<: *ci-template-vars
      EXTRA_PACKAGES: "time python wget"

  unimath:
    <<: *ci-template

  vst:
    <<: *ci-template

workflows:
  version: 2
  # Run on each push
  main:
    jobs:
      - opam-boot

      - build:
          requires:
            - opam-boot

      - bignums: &req-main
          requires:
            - build
      - color:
          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
      - math-classes:
          requires:
            - build
            - bignums
      - corn:
          requires:
            - build
            - math-classes
      - formal-topology:
          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