Skip to content

Add related_hetero_and_Proper #609

Add related_hetero_and_Proper

Add related_hetero_and_Proper #609

Workflow file for this run

name: CI (Coq)
on:
push:
pull_request:
schedule:
- cron: '0 0 1 * *'
jobs:
build:
strategy:
fail-fast: false
matrix:
os: [ ubuntu-latest ]
env:
- { COQ_VERSION: "8.17.1", COQ_PACKAGE: "coq-8.17.1 libcoq-8.17.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
# Ltac2 is broken in the 8.16 package
#- { COQ_VERSION: "8.16.1", COQ_PACKAGE: "coq-8.16.1 libcoq-8.16.1-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-11" }
- { COQ_VERSION: "8.15.2", COQ_PACKAGE: "coq-8.15.2 libcoq-8.15.2-ocaml-dev", SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" }
include:
- env: { COQ_VERSION: "v8.15" , COQ_PACKAGE: "coq libcoq-ocaml-dev" , SKIP_VALIDATE: "" , PPA: "ppa:jgross-h/coq-8.15-daily" }
os: ubuntu-20.04
env: ${{ matrix.env }}
runs-on: ${{ matrix.os }}
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::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: all
run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all
- name: perf-Sanity
run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 perf-Sanity
- name: display timing info
run: cat time-of-build-pretty.log
- name: display per-line timing info
run: etc/ci/github-actions-display-per-line-timing.sh
# - name: upload timing and .vo info
# uses: actions/upload-artifact@v1
# with:
# name: build-outputs-${{ matrix.env.COQ_VERSION }}
# path: .
# if: always ()
- name: validate
run: make TIMED=1 validate COQCHKFLAGS="-o"
if: matrix.env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'
check-all:
runs-on: ubuntu-latest
needs: build
if: always()
steps:
- run: echo 'The triggering workflow passed'
if: ${{ needs.build.result == 'success' }}
- run: echo 'The triggering workflow failed' && false
if: ${{ needs.build.result != 'success' }}