CI (Coq) #4153
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 (Coq) | |
| on: | |
| push: | |
| branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ] | |
| pull_request: | |
| workflow_dispatch: | |
| schedule: | |
| - cron: '0 0 1 * *' | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - env: { COQ_VERSION: "Ubuntu LTS", COQ_PACKAGE: "coq libcoq-ocaml-dev" , SKIP_VALIDATE: "1", COQCHKEXTRAFLAGS: "" , PPA: "" } | |
| os: 'ubuntu-22.04' | |
| runs-on: ${{ matrix.os }} | |
| env: ${{ matrix.env }} | |
| name: ${{ matrix.env.COQ_VERSION }} | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| steps: | |
| - uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: install Coq | |
| run: | | |
| 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 | |
| - uses: haskell/actions/setup@v2 | |
| with: | |
| ghc-version: 'latest' | |
| cabal-version: 'latest' | |
| - name: echo build params | |
| run: etc/ci/describe-system-config.sh | |
| - name: deps | |
| run: etc/ci/github-actions-make.sh -j2 deps | |
| - name: all-except-generated | |
| run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated | |
| - name: generated-files | |
| run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 generated-files | |
| if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master' | |
| - run: tar -czvf generated-files.tgz fiat-*/ | |
| if: ${{ failure() }} | |
| - name: upload generated files | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: generated-files-${{ matrix.env.COQ_VERSION }} | |
| path: generated-files.tgz | |
| if: ${{ failure() }} | |
| - name: upload OCaml files | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }} | |
| path: src/ExtractionOCaml | |
| if: always () | |
| - name: standalone-haskell | |
| run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS' | |
| - name: upload Haskell files | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: ExtractionHaskell-${{ matrix.env.COQ_VERSION }} | |
| path: src/ExtractionHaskell | |
| if: always () | |
| - name: display timing info | |
| run: cat time-of-build-pretty.log | |
| - name: display per-line timing info | |
| run: etc/ci/github-actions-display-per-line-timing.sh | |
| # - name: upload timing and .vo info | |
| # uses: actions/upload-artifact@v3 | |
| # with: | |
| # name: build-outputs-${{ matrix.env.COQ_VERSION }} | |
| # path: . | |
| # if: always () | |
| - name: validate | |
| run: make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}" | |
| if: matrix.env.SKIP_VALIDATE == '' && github.event_name != 'pull_request' | |
| test-amd64: | |
| runs-on: ubuntu-latest | |
| concurrency: | |
| group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| needs: build | |
| steps: | |
| - name: checkout repo | |
| uses: actions/checkout@v3 | |
| with: | |
| submodules: recursive | |
| - name: Download a Build Artifact | |
| uses: actions/download-artifact@v3 | |
| with: | |
| name: "ExtractionOCaml-Ubuntu LTS" | |
| path: src/ExtractionOCaml | |
| - name: make binaries executable | |
| run: chmod +x src/ExtractionOCaml/* | |
| - name: make only-test-amd64-files | |
| run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files SLOWEST_FIRST=1 | |
| env: | |
| ALLOW_DIFF: 1 |