coq.yml

# Based on a similar workflow for the mit-plv/rupicola repository, which in turn is based on mit-plv/fiat-crypto

name: Coq

on:
  push:
    branches:
      - master
  pull_request:
  workflow_dispatch:

jobs:
  build:

    runs-on: ubuntu-20.04

    strategy:
      matrix:
        env:
        - { COQ_VERSION: "8.18.0", COQ_PACKAGE: "coq-8.18.0 libcoq-8.18.0-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
        - { COQ_VERSION: "master", COQ_PACKAGE: "coq libcoq-core-ocaml-dev"         , PPA: "ppa:jgross-h/coq-master-daily" }
      fail-fast: false

    name: build (${{ matrix.env.COQ_VERSION }})

    env: ${{ matrix.env }}

    concurrency:
      group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
      cancel-in-progress: true

    steps:
    - name: install Coq
      run: |
        sudo sed -i 's/azure\.//' /etc/apt/sources.list
        if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
        sudo apt-get -o Acquire::Retries=30 update -q
        sudo apt-get -o Acquire::Retries=30 install ocaml-findlib $COQ_PACKAGE -y --allow-unauthenticated
    - name: echo build params
      run: |
        echo "::group::lscpu"
        lscpu
        echo "::endgroup::"
        echo "::group::uname -a"
        uname -a
        echo "::endgroup::"
        echo "::group::lsb_release -a"
        lsb_release -a
        echo "::endgroup::"
        echo "::group::gcc -v"
        gcc -v
        echo "::endgroup::"
        echo "::group::ocamlc -config"
        ocamlc -config
        echo "::endgroup::"
        echo "::group::coqc --config"
        coqc --config
        echo "::endgroup::"
        echo "::group::coqc --version"
        coqc --version
        echo "::endgroup::"
        echo "::group::echo | coqtop"
        echo | coqtop
        echo "::endgroup::"
    - uses: actions/checkout@v4
      with:
        submodules: recursive
    - name: make
      run: TIMED=1 make

  coq-check-all:
    runs-on: ubuntu-latest
    needs: build
    if: always()
    steps:
    - run: echo 'build passed'
      if: ${{ needs.build.result == 'success' }}
    - run: echo 'build failed' && false
      if: ${{ needs.build.result != 'success' }}