ci.yml

name: CI

on:
  push:
    branches:
    - v8.8
    - v8.9
    - v8.10
    - v8.11
    - v8.12
    - v8.13
    - v8.14
    - v8.15
    - v8.16
    - v8.17
    - main
  pull_request:
    branches:
    - v8.8
    - v8.9
    - v8.10
    - v8.11
    - v8.12
    - v8.13
    - v8.14
    - v8.15
    - v8.16
    - v8.17
    - main
  # Allows you to run this workflow manually from the Actions tab
  workflow_dispatch:

jobs:
  build:
    strategy:
      fail-fast: false
      matrix:
        ocaml-compiler: [4.09.x, 4.10.x, 4.11.x, 4.12.x, 4.13.x, 4.14.x, 5.0.x]
        test-target: [test]
        extra-opam: [coq.8.17.dev coq-mathcomp-ssreflect.dev]
        include:
        - ocaml-compiler: ocaml-variants.4.12.1+options,ocaml-option-32bit
          test-target: js-dune
          extra-opam: coq.8.17.dev js_of_ocaml js_of_ocaml-lwt zarith_stubs_js
        - ocaml-compiler: 4.13.1
          test-target: test
          extra-opam:
          coq-from-git: true
    env:
      OPAMJOBS: "2"
      OPAMROOTISOK: "true"
      OPAMYES: "true"
      NJOBS: "2"
      COQ_REPOS: "https://github.com/coq/coq.git"
      COQ_BRANCH: "v8.17"
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v2
      - name: Install apt dependencies
        run: |
          sudo dpkg --add-architecture i386
          sudo apt-get -o Acquire::Retries=30 update -q
          sudo apt-get -o Acquire::Retries=30 install gcc-multilib libgmp-dev:i386 -y --allow-unauthenticated
      - name: Set up OCaml ${{ matrix.ocaml-compiler }}
        uses: avsm/setup-ocaml@v2
        with:
          ocaml-compiler: ${{ matrix.ocaml-compiler }}
          dune-cache: true
      - name: Basic OPAM setup for SerAPI
        run: |
          eval $(opam env)
          opam repos add coq-released http://coq.inria.fr/opam/released
          opam repos add coq-core-dev http://coq.inria.fr/opam/core-dev
          # Only for mathcomp.dev which is needed for 8.16, remove when math-comp is fixed
          opam repos add coq-extra-dev http://coq.inria.fr/opam/extra-dev
          # coq-serapi already pinned by the setup-ocaml@v2 action
          opam install --deps-only coq-serapi
      - name: Display OPAM Setup
        run: |
          eval $(opam env)
          opam list
      - name: Install Coq via git
        if: ${{ matrix.coq-from-git }}
        run: |
          eval $(opam env)
          opam pin add -k version dune 3.3.1
          # First we update SERAPI_COQ_HOME for future steps as per https://docs.github.com/en/actions/reference/workflow-commands-for-github-actions#setting-an-environment-variable
          echo "SERAPI_COQ_HOME=$HOME/coq-$COQ_BRANCH/_build/install/default/lib/" >> $GITHUB_ENV
          # Update to coq-core some day
          # opam install --deps-only coq-core
          opam install --deps-only coq-core
          git clone --depth=3 -b "$COQ_BRANCH" "$COQ_REPOS" "$HOME/coq-$COQ_BRANCH"
          # Upstream 'make -C "$HOME/coq-$COQ_BRANCH" world' target now builds coqide
          cd "$HOME/coq-$COQ_BRANCH"
          ./configure -prefix "$HOME/coq-$COQ_BRANCH/_build/install/default/"
          make dunestrap
          dune build -p coq-core,coq-stdlib,coq
          cd "$HOME"
          # Install math-comp using Coq from git
          PATH="$HOME/coq-$COQ_BRANCH/_build/install/default/bin:$PATH"
          git clone --depth=3 -b master https://github.com/math-comp/math-comp.git
          make -C math-comp/mathcomp/ssreflect
          make -C math-comp/mathcomp/ssreflect install
      - name: Extra OPAM Setup (Coq, js_of_ocaml)
        if: ${{ matrix.extra-opam != '' }}
        run: |
          eval $(opam env)
          opam install ${{ matrix.extra-opam }}
      - name: Build and Test SerAPI
        run: |
          eval $(opam env)
          make -j "$NJOBS" SERAPI_COQ_HOME="$SERAPI_COQ_HOME" "${{ matrix.test-target }}"
          ls -lR _build/install/default/ || true
          ls -lR _build/default/sertop/*.js || true