Adapt to Coq/Coq#18164 (#103) #212
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 ] | |
| pull_request: | |
| workflow_dispatch: | |
| jobs: | |
| build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| env: | |
| - { COQ_VERSION: "v8.15" , TARGETS: "fiat-core parsers querystructures", FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-8.15-daily" } | |
| - { COQ_VERSION: "v8.14" , TARGETS: "fiat-core parsers querystructures", FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-8.14-daily" } | |
| - { COQ_VERSION: "v8.13" , TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-8.13-daily" } | |
| - { COQ_VERSION: "v8.12" , TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-8.12-daily" } | |
| - { COQ_VERSION: "v8.11" , TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-8.11-daily" } | |
| - { COQ_VERSION: "8.15.0", TARGETS: "fiat-core parsers querystructures", FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq-8.15.0 libcoq-8.15.0-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" } | |
| - { COQ_VERSION: "8.14.1", TARGETS: "fiat-core parsers querystructures", FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq-8.14.1 libcoq-8.14.1-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" } | |
| - { COQ_VERSION: "8.13.2", TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq-8.13.2 libcoq-8.13.2-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" } | |
| - { COQ_VERSION: "8.12.2", TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq-8.12.2 libcoq-8.12.2-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" } | |
| - { COQ_VERSION: "8.11.2", TARGETS: "fiat-core parsers" , FLAGS: "PROFILE=1", NJOBS: "2", COQ_PACKAGE: "coq-8.11.2 libcoq-8.11.2-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" } | |
| env: ${{ matrix.env }} | |
| name: ${{ matrix.env.COQ_VERSION }} (${{ matrix.env.TARGETS }}) | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| runs-on: ubuntu-20.04 | |
| steps: | |
| - 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 | |
| - 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::ghc --version" | |
| ghc --version | |
| 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 | |
| with: | |
| submodules: recursive | |
| - name: SCRIPT | |
| run: ./etc/coq-scripts/timing/make-pretty-timed.sh -j$NJOBS $TARGETS $FLAGS && make TIMED=1 -j$NJOBS $TARGETS | |
| 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' }} |