coq.yml

# Based on a similar workflow for the mit-plv/fiat-crypto repository

name: Coq

on:
  push:
  pull_request:
  schedule:
    - cron: '0 0 1 * *'
  workflow_dispatch:

jobs:
  build:

    runs-on: ubuntu-latest

    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

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

    env: ${{ matrix.env }}

    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
    - name: submodules-init
      run: git submodule update --init --recursive
    - name: make dependencies
      run: make -j2 deps
    - name: make all
      run: make -j2 all

  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' }}