path: root/.circleci/config.yml

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
    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: Install system packages
  command: |
    echo export TERM=xterm >> ~/.profile
    source ~/.profile
    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

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 ${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 "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} ${EXTRA_CONF}
    - 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: &build-variables
    <<: *envvars
    EXTRA_CONF: "-coqide opt"
    EXTRA_PACKAGES: *coqide-packages

.validate-template: &validate-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: *attach_workspace
    - run:
        name: Validate
        command: |
          source ~/.profile
          make validate
  environment: *envvars

.documentation-template: &documentation-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: *attach_workspace
    - run:
        name: Documentation
        command: |
          source ~/.profile
          make -j ${NJOBS} doc
  environment: &documentation-variables
    <<: *envvars
    EXTRA_PACKAGES: *coqdoc-packages

.test-suite-template: &test-suite-template
  <<: *params
  steps:
    - run: *before_script
    - attach_workspace: *attach_workspace
    - run:
        name: Test
        command: |
          source ~/.profile
          cd test-suite
          make clean
          make -j ${NJOBS} all
  environment: &test-suite-variables
    <<: *envvars
    EXTRA_PACKAGES: *timing-packages

.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:
  # 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

  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

  validate: *validate-template

  validate-32bit:
    <<: *validate-template
    environment:
      <<: *envvars
      COMPILER: *compiler-32bit
      EXTRA_PACKAGES: "gcc-multilib"

  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
      EXTRA_PACKAGES: *timing-packages

  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"

  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
      - opam-boot-32bit
      - opam-boot-be

      - build:
          requires:
            - opam-boot
      - validate: &req-main
          requires:
            - build
      - test-suite: *req-main
      - documentation: *req-main

      - bignums: *req-main
      - color:
          requires:
            - build
            - bignums
      - compcert: *req-main
      - coq-dpdgraph: *req-main
      - coquelicot: *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

      - build-32bit:
          requires:
            - opam-boot-32bit
      - validate-32bit: &req-32bit
          requires:
            - build-32bit
      - test-suite-32bit: *req-32bit

      - build-be:
          requires:
            - opam-boot-be
      - test-suite-be: &req-be
          requires:
            - build-be
      - documentation-be: *req-be