Work around coq-dev not supporting Mathcomp 1 #271
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: | |
| paths: | |
| - theories/** | |
| - _CoqProject | |
| - Makefile | |
| - Makefile.coq.local | |
| - .github/workflows/coq.yml | |
| branches: | |
| - main | |
| pull_request: | |
| workflow_dispatch: | |
| permissions: | |
| contents: write | |
| jobs: | |
| docker-build: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - env: { COQ_VERSION: "master", DOCKER_COQ_VERSION: "dev" , DOCKER_MATHCOMP_VERSION: "latest", DOCKER_OCAML_VERSION: "default", OPAM_DEPS: "coq-record-update coq-flocq", LAPROOF: "", TGTS: "computed", INSTALL_TGTS: "" } | |
| - env: { COQ_VERSION: "8.17" , DOCKER_COQ_VERSION: "8.17", DOCKER_MATHCOMP_VERSION: "1.18.0", DOCKER_OCAML_VERSION: "default", OPAM_DEPS: "coq-record-update coq-flocq coq-interval coq-vcfloat coq-mathcomp-zify coq-mathcomp-analysis coq-mathcomp-algebra-tactics coq-mathcomp-finmap coq-vst coq-vst-lib", LAPROOF: "1", TGTS: "", INSTALL_TGTS: "install" } | |
| runs-on: ubuntu-latest | |
| env: ${{ matrix.env }} | |
| name: ${{ matrix.env.COQ_VERSION }} | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-docker-build-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Runner Info for ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-docker-build-${{ github.head_ref || github.run_id }} | |
| run: true | |
| - uses: coq-community/docker-coq-action@v1 | |
| with: | |
| custom_image: mathcomp/mathcomp:${{ matrix.env.DOCKER_MATHCOMP_VERSION }}-coq-${{ matrix.env.DOCKER_COQ_VERSION }} | |
| #coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| #ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI | |
| custom_script: | | |
| eval $(opam env) | |
| sudo chmod -R a=u . | |
| # Work around https://github.com/actions/checkout/issues/766 | |
| git config --global --add safe.directory "*" | |
| startGroup 'install dependencies' | |
| opam install -y -v ${{ matrix.env.OPAM_DEPS }} | |
| endGroup | |
| startGroup 'install LAProof' | |
| if [ ! -z "${{ matrix.env.LAPROOF }}" ]; then | |
| git clone https://github.com/VeriNum/LAProof.git | |
| pushd LAProof | |
| git remote add JasonGross https://github.com/JasonGross/LAProof.git | |
| git remote update | |
| git checkout 7e5c81dcfafde501e87a2c2db4021f5190dff960 # waiting on https://github.com/VeriNum/LAProof/pull/10/ | |
| make -j2 TIMED=1 | |
| make install | |
| popd | |
| fi | |
| endGroup | |
| startGroup 'make' | |
| make pretty-timed -j2 TGTS="${{ matrix.env.TGTS }}" | |
| if [ ! -z "${{ matrix.env.INSTALL_TGTS }}" ]; then | |
| make ${{ matrix.env.INSTALL_TGTS }} | |
| fi | |
| endGroup | |
| make print-pretty-timed | |
| docker-build-native: | |
| strategy: | |
| fail-fast: false | |
| matrix: | |
| include: | |
| - env: { COQ_VERSION: "master (native)", DOCKER_COQ_VERSION: "dev-native" , DOCKER_OCAML_VERSION: "default", OPAM_DEPS: "", LAPROOF: "", TGTS: "computed" } | |
| - env: { COQ_VERSION: "master (for Coq CI, native)", DOCKER_COQ_VERSION: "dev-native" , DOCKER_OCAML_VERSION: "default", OPAM_DEPS: "", LAPROOF: "", TGTS: "coq-ci-target" } | |
| runs-on: ubuntu-latest | |
| env: ${{ matrix.env }} | |
| name: ${{ matrix.env.COQ_VERSION }} | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-docker-build-native-${{ github.head_ref || github.run_id }} | |
| cancel-in-progress: true | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| submodules: recursive | |
| - name: Runner Info for ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-docker-build-native-${{ github.head_ref || github.run_id }} | |
| run: true | |
| - uses: coq-community/docker-coq-action@v1 | |
| with: | |
| coq_version: ${{ matrix.env.DOCKER_COQ_VERSION }} | |
| ocaml_version: ${{ matrix.env.DOCKER_OCAML_VERSION }} | |
| export: CI | |
| custom_script: | | |
| eval $(opam env) | |
| sudo chmod -R a=u . | |
| # Work around https://github.com/actions/checkout/issues/766 | |
| git config --global --add safe.directory "*" | |
| startGroup 'install dependencies' | |
| if [ ! -z "${{ matrix.env.OPAM_DEPS }}" ]; then | |
| opam install -y -v ${{ matrix.env.OPAM_DEPS }} | |
| fi | |
| endGroup | |
| startGroup 'install LAProof' | |
| if [ ! -z "${{ matrix.env.LAPROOF }}" ]; then | |
| git clone https://github.com/VeriNum/LAProof.git | |
| pushd LAProof | |
| git remote add JasonGross https://github.com/JasonGross/LAProof.git | |
| git remote update | |
| git checkout 7e5c81dcfafde501e87a2c2db4021f5190dff960 # waiting on https://github.com/VeriNum/LAProof/pull/10/ | |
| make -j2 TIMED=1 | |
| make install | |
| popd | |
| fi | |
| endGroup | |
| startGroup 'make' | |
| make pretty-timed -j2 TGTS="${{ matrix.env.TGTS }}" | |
| endGroup | |
| make print-pretty-timed | |
| check-all: | |
| runs-on: ubuntu-latest | |
| needs: [docker-build, docker-build-native] | |
| if: always() | |
| steps: | |
| - run: echo 'docker-build passed' | |
| if: ${{ needs.docker-build.result == 'success' }} | |
| - run: echo 'docker-build-native passed' | |
| if: ${{ needs.docker-build-native.result == 'success' }} | |
| - run: echo 'docker-build failed' && false | |
| if: ${{ needs.docker-build.result != 'success' }} | |
| - run: echo 'docker-build-native failed' && false | |
| if: ${{ needs.docker-build-native.result != 'success' }} | |
| update-tested: | |
| name: Update tested | |
| if: github.ref == 'refs/heads/main' | |
| needs: [docker-build, docker-build-native] | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - run: pwd | |
| - run: git fetch origin tested | |
| - run: git log --oneline --max-count=10 | |
| - run: git log origin/tested --oneline --max-count=10 | |
| - run: git log origin/main --oneline --max-count=10 | |
| - run: git push origin HEAD:tested |