VST on Iris #991
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 | |
| on: | |
| push: | |
| branches: | |
| - master | |
| paths-ignore: | |
| - 'lib/**' | |
| pull_request: | |
| paths-ignore: | |
| - 'lib/**' | |
| jobs: | |
| build: | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| # ATTENTION: the "matrix" section must be identical for the "build" and "test" job | |
| # except for the "make_target" field and make_target related excludes | |
| coq_version: | |
| # See https://github.com/coq-community/docker-coq/wiki for supported images | |
| - '8.17' | |
| - '8.18' | |
| - '8.19' | |
| - 'dev' | |
| bit_size: | |
| - 32 | |
| - 64 | |
| make_target: | |
| - vst | |
| exclude: | |
| - coq_version: 8.17 | |
| bit_size: 32 | |
| - coq_version: 8.18 | |
| bit_size: 32 | |
| - coq_version: dev | |
| bit_size: 32 | |
| steps: | |
| - uses: actions/checkout@v2 | |
| with: | |
| submodules: true | |
| - uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.coq_version }} | |
| # See https://github.com/coq-community/docker-coq-action/tree/v1 for usage | |
| before_install: | | |
| startGroup "Opam config" | |
| opam repo add -y prerelease file://$(pwd)/opam-prerelease | |
| opam update -y | |
| opam config list; opam repo list; opam list | |
| endGroup | |
| install: | | |
| startGroup "Install dependencies" | |
| opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }} | |
| # Required by test2 | |
| opam install -y coq-ext-lib | |
| if [ ${{ github.ref_name }} = "755/merge" ] | |
| then | |
| opam repo add -y iris-dev https://gitlab.mpi-sws.org/iris/opam.git | |
| opam install -y coq-iris.dev.2024-02-04.0.0771fa71 | |
| fi | |
| endGroup | |
| # See https://github.com/coq-community/docker-coq-action/tree/v1#permissions | |
| before_script: | | |
| startGroup "Workaround permission issue" | |
| sudo chmod -R a=u . | |
| endGroup | |
| script: | | |
| startGroup "Build & Install" | |
| make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| endGroup | |
| after_script: | | |
| startGroup 'Copy Opam coq/user-contrib and coq-variant' | |
| cp -R -v "$(opam var lib)"/coq/user-contrib . | |
| mkdir -p "$(opam var lib)"/coq-variant/dummy | |
| cp -R -v "$(opam var lib)"/coq-variant . | |
| endGroup | |
| uninstall: | |
| - name: 'Create archive' | |
| run: tar -cpvzf archive.tgz * .depend | |
| - name: 'Upload archive' | |
| uses: actions/upload-artifact@v2 | |
| with: | |
| name: 'VST build artifacts ${{matrix.coq_version}} ${{matrix.bit_size}}' | |
| path: archive.tgz | |
| retention-days: 1 | |
| test: | |
| needs: build | |
| runs-on: ubuntu-latest | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| coq_version: | |
| - '8.17' | |
| - '8.18' | |
| - '8.19' | |
| - 'dev' | |
| make_target: | |
| - assumptions.txt | |
| - test | |
| - test2 | |
| - test3 | |
| - test4 | |
| - test5 | |
| bit_size: | |
| - 32 | |
| - 64 | |
| exclude: | |
| - coq_version: 8.17 | |
| bit_size: 32 | |
| - coq_version: 8.18 | |
| bit_size: 32 | |
| - coq_version: dev | |
| bit_size: 32 | |
| - bit_size: 64 | |
| make_target: test3 | |
| - bit_size: 32 | |
| make_target: test4 | |
| - bit_size: 64 | |
| make_target: test5 | |
| steps: | |
| - name: 'Download archive' | |
| uses: actions/download-artifact@v2 | |
| id: download | |
| with: | |
| name: 'VST build artifacts ${{matrix.coq_version}} ${{matrix.bit_size}}' | |
| - name: 'Extract archive' | |
| run: tar -xvpzf archive.tgz | |
| - uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.coq_version }} | |
| install: | | |
| startGroup "Copy downloaded Opam coq/user-contrib and coq-variant" | |
| cp -R -v user-contrib/* "$(opam var lib)"/coq/user-contrib | |
| mkdir -p "$(opam var lib)"/coq-variant | |
| cp -R -v coq-variant/* "$(opam var lib)"/coq-variant | |
| endGroup | |
| before_script: | | |
| startGroup "Workaround permission issue" | |
| sudo chmod -R a=u . | |
| endGroup | |
| script: | | |
| startGroup "Build & Install" | |
| make -f util/make-touch IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| endGroup | |
| uninstall: |