Adapt to Coq PR #17993 fixing Coq bug #12521 about simpl failing on mutual fixpoints with parameters #178
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 (Coq) | |
| on: | |
| push: | |
| 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 }} | |
| 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@v3 | |
| with: | |
| submodules: recursive | |
| - name: SCRIPT | |
| run: ./etc/coq-scripts/timing/make-pretty-timed.sh -j$NJOBS $TARGETS $FLAGS && make TIMED=1 -j$NJOBS $TARGETS |