CI Build UniMath #16
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI Build UniMath | |
| on: | |
| push: | |
| branches: [master] | |
| pull_request: | |
| branches: [master] | |
| # Allows you to run this workflow manually from the Actions tab | |
| workflow_dispatch: | |
| schedule: | |
| # Based on https://github.com/marketplace/actions/set-up-ocaml | |
| # Prime the caches every Monday | |
| - cron: '0 1 * * MON' | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| # This workflow contains four kinds of jobs: | |
| # - sanity-checks | |
| # - build-Unimath-ubuntu: (Linux, docker-coq, latest Coq >= 8.16, manual cache) | |
| # - build-macos: (MacOS, Opam, Coq 8.16.0, cache using actions/setup-ocaml) | |
| # - build-satellites: (Linux, docker-coq, Coq 8.16.x, manual cache) | |
| sanity-checks: | |
| name: Sanity Checks | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install build dependencies | |
| run: | | |
| sudo apt-get update | |
| sudo apt-get install coq | |
| type coqc | |
| coqc --version | |
| - name: Run sanity checks | |
| run: | | |
| cd $GITHUB_WORKSPACE | |
| time make -k sanity-checks || time make sanity-checks | |
| # Build the current PR/branch with the latest stable release of Coq. | |
| build-Unimath-ubuntu: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| os: [ubuntu-22.04] | |
| # https://github.com/coq-community/docker-coq/wiki#ocaml-versions-policy | |
| coq-version: [latest, dev] | |
| # (the following is obsolete:) coq-version: [8.16] or [latest, 8.16] (when 8.17 is released) | |
| ocaml-version: [default] | |
| name: Build on Linux (Coq ${{ matrix.coq-version }}) | |
| runs-on: ${{ matrix.os }} | |
| steps: | |
| - uses: actions/checkout@v4 | |
| # Grab the cache if available and extract it to dune-cache/. We tell dune | |
| # to use $(pwd)/dune-cache/ in the custom_script when initiating the | |
| # docker run. | |
| - uses: actions/cache/restore@v4 | |
| id: cache | |
| with: | |
| path: dune-cache | |
| # Example key: UniMath-Linux-coq-8.16-123456789-10 | |
| key: UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }} | |
| restore-keys: | | |
| UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }} | |
| UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}- | |
| - name: Build UniMath | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.coq-version }} | |
| ocaml_version: ${{ matrix.ocaml-version }} | |
| custom_script: | | |
| startGroup "Workaround permission issue" | |
| sudo chown -R coq:coq . | |
| endGroup | |
| startGroup "Print versions" | |
| opam --version | |
| opam exec -- dune --version | |
| opam exec -- coqc --version | |
| endGroup | |
| startGroup "Build UniMath" | |
| export DUNE_CACHE_ROOT=$(pwd)/dune-cache/ | |
| opam exec -- dune build -j 2 --display=short \ | |
| --cache=enabled --error-reporting=twice | |
| endGroup | |
| - name: Revert permissions | |
| if: ${{ always() }} | |
| run: sudo chown -R 1001:116 . | |
| - uses: actions/cache/save@v4 | |
| if: always() | |
| with: | |
| path: dune-cache | |
| key: UniMath-${{ runner.os }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }} | |
| # Build UniMath on MacOS using latest stable release of Coq installed with | |
| # Homebrew (8.18.0 still on March 18, 2024). Build files are cached. | |
| build-macos: | |
| name: Build on macOS (latest Coq on Homebrew) | |
| runs-on: macos-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| - name: Install Coq | |
| run: | | |
| brew install coq ocaml-findlib dune | |
| coqc --version | |
| dune --version | |
| - uses: actions/cache/restore@v4 | |
| id: cache | |
| with: | |
| path: dune-cache | |
| key: UniMath-MacOS-${{ github.run_id }}-${{ github.run_number }} | |
| restore-keys: | | |
| UniMath-MacOS-${{ github.run_id }} | |
| UniMath-MacOS | |
| - name: Build UniMath | |
| run: | | |
| export DUNE_CACHE_ROOT=$(pwd)/dune-cache/ | |
| dune build --display=short --error-reporting=twice --cache=enabled UniMath/ | |
| - uses: actions/cache/save@v4 | |
| if: always () | |
| with: | |
| path: dune-cache | |
| key: UniMath-MacOS-${{ github.run_id }}-${{ github.run_number }} | |
| # Build the satellites in parallel using docker-coq images with the latest | |
| # stable patch-release of Coq 8.19 as of March 20, 2024 | |
| # (outdated comment:) except for TypeTheory, which is built | |
| # using the latest stable 8.15 release. | |
| build-satellites: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| satellite: [SetHITs, largecatmodules, GrpdHITs, TypeTheory] | |
| coq-version: [latest, dev] | |
| ocaml-version: [4.14-flambda] | |
| # (outdated exception:) exclude: | |
| # - satellite: GrpdHITs | |
| # coq-version: dev | |
| name: Build ${{ matrix.satellite }} (Coq ${{ matrix.coq-version }}) | |
| runs-on: ubuntu-22.04 | |
| steps: | |
| # Check out the current branch of UniMath in the current directory. | |
| - uses: actions/checkout@v4 | |
| # Check out the satellite we want to build in Satellite/. | |
| - name: Clone ${{ matrix.satellite }} | |
| uses: actions/checkout@v4 | |
| with: | |
| repository: UniMath/${{ matrix.satellite }} | |
| path: Satellite | |
| # Grab the cache if available. We tell dune to use $(pwd)/dune-cache/ in | |
| # the custom_script below. | |
| - uses: actions/cache/restore@v4 | |
| id: cache | |
| with: | |
| path: dune-cache | |
| # Example key: SetHITs-coq-8.15-123456789-10 | |
| key: ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }} | |
| restore-keys: | | |
| ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }} | |
| ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}- | |
| - name: Build ${{ matrix.satellite }} | |
| uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.coq-version }} | |
| ocaml_version: ${{ matrix.ocaml-version }} | |
| custom_script: | | |
| startGroup "Workaround permission issue" | |
| sudo chown -R coq:coq . | |
| endGroup | |
| startGroup "Print versions" | |
| opam --version | |
| opam exec -- dune --version | |
| opam exec -- coqc --version | |
| endGroup | |
| startGroup "Build Satellite" | |
| export DUNE_CACHE_ROOT=$(pwd)/dune-cache/ | |
| opam exec -- dune build -j 2 Satellite --display=short \ | |
| --cache=enabled --error-reporting=twice | |
| endGroup | |
| - name: Revert permissions | |
| if: ${{ always() }} | |
| run: sudo chown -R 1001:116 . | |
| - uses: actions/cache/save@v4 | |
| if: always () | |
| with: | |
| path: dune-cache | |
| key: ${{ matrix.satellite }}-coq-${{ matrix.coq-version }}-${{ github.run_id }}-${{ github.run_number }} |