Port VST 2.x to CompCert master #1086
Workflow file for this run
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 | |
| 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" | |
| # put the first version back once CompCert 3.15 is in the Coq Platform | |
| # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled 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: 32 | |
| 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 | |
| # put the first version back once CompCert 3.15 is in the Coq Platform | |
| # make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=${{ matrix.coq_version=='dev' && 'bundled' || 'platform' }} IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| make ${{matrix.make_target}} BITSIZE=${{matrix.bit_size}} COMPCERT=bundled IGNORECOQVERSION=true IGNORECOMPCERTVERSION=true | |
| endGroup | |
| uninstall: |