Skip to content

Adapt w.r.t. coq/coq#19228. #349

Adapt w.r.t. coq/coq#19228.

Adapt w.r.t. coq/coq#19228. #349

Workflow file for this run

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.17.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 (native)" , DOCKER_COQ_VERSION: "dev-native" , DOCKER_OCAML_VERSION: "default", OPAM_DEPS: "", LAPROOF: "", TGTS: "computed-lite" }
- 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 }}-${{ matrix.env.TGTS }}
concurrency:
group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-docker-build-native-${{ matrix.env.TGTS }}-${{ 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