From 65ab4f07afd48ccad264b386c1f28d3b2c97e96d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 1 Jul 2022 12:57:22 -0400 Subject: [PATCH] Use docker-coq action for running Coq This will hopefully make it easier to maintain moving forwards, and make it easier to work around the native compiler issue by moving to the dev versions of older Coq versions with https://github.com/coq-community/docker-coq/issues/49 --- .github/workflows/coq.yml | 76 ++++++++---------- PerformanceExperiments/gen-listing.sh | 2 +- README.md | 108 +++++++++++++------------- 3 files changed, 86 insertions(+), 100 deletions(-) diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml index 0b50fb01d6..de87722942 100644 --- a/.github/workflows/coq.yml +++ b/.github/workflows/coq.yml @@ -15,31 +15,17 @@ jobs: fail-fast: false matrix: # N.B. The update-README makefile target pulls information - # about Coq versions from this file, so be careful about - # ordering of the env and about the presence of COQ_VERSION - # immediately followed by : in this file - env: - - { COQ_VERSION: "master", COQ_PACKAGE: "coq libcoq-ocaml-dev" , PPA: "ppa:jgross-h/coq-master-daily" , TIMED: "1" } - - { COQ_VERSION: "8.15.0", COQ_PACKAGE: "coq-8.15.0 libcoq-8.15.0-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" , TIMED: "1" } - - { COQ_VERSION: "8.14.1", COQ_PACKAGE: "coq-8.14.1 libcoq-8.14.1-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-08" , TIMED: "1" } - - { COQ_VERSION: "8.13.2", COQ_PACKAGE: "coq-8.13.2 libcoq-8.13.2-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" , TIMED: "1" } - - { COQ_VERSION: "8.12.2", COQ_PACKAGE: "coq-8.12.2 libcoq-8.12.2-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" , TIMED: "1" } - - { COQ_VERSION: "8.11.2", COQ_PACKAGE: "coq-8.11.2 libcoq-8.11.2-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" , TIMED: "1" } - - { COQ_VERSION: "8.10.2", COQ_PACKAGE: "coq-8.10.2 libcoq-8.10.2-ocaml-dev", PPA: "ppa:jgross-h/many-coq-versions-ocaml-4-05" , TIMED: "1" } - - { COQ_VERSION: "8.9.1" , COQ_PACKAGE: "coq-8.9.1 libcoq-8.9.1-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions" , TIMED: "1" } - - { COQ_VERSION: "8.8.2" , COQ_PACKAGE: "coq-8.8.2 libcoq-8.8.2-ocaml-dev" , PPA: "ppa:jgross-h/many-coq-versions" , TIMED: "1" } - - env: ${{ matrix.env }} + # about Coq versions from this file, so be careful about the + # presence of COQ_VERSION immediately followed by : in this + # file and about the ordering of the list + COQ_VERSION: ["dev", "8.15", "8.14", "8.13", "8.12", "8.11", "8.10", "8.9", "8.8"] steps: - - name: install Coq and deps + - uses: actions/checkout@v3 + - name: install deps 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 -y --allow-unauthenticated \ - ocaml-findlib \ - $COQ_PACKAGE \ - apt-show-versions \ texlive \ texlive-latex-extra \ texlive-bibtex-extra \ @@ -56,8 +42,7 @@ jobs: pdf2svg \ python \ python-pygments - - uses: actions/checkout@v3 - - name: echo build params + - name: echo build params (Coq: ${{ matrix.COQ_VERSION }}) run: | echo "::group::lscpu" lscpu @@ -71,34 +56,35 @@ jobs: echo "::group::etc/machine.sh" etc/machine.sh 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" - true | coqtop - echo "::endgroup::" - echo "::group::apt-show-versions $COQ_PACKAGE" - apt-show-versions $COQ_PACKAGE - echo "::endgroup::" - - run: make -j2 TiMED=1 - - run: make perf - - run: make validate -j2 - - run: sudo make install install-perf + - uses: coq-community/docker-coq-action@v1 + with: + coq_version: ${{ matrix.COQ_VERSION }} + ocaml_version: default + custom_script: | + sudo chmod -R a+rw . + echo '::group::make -j2 TIMED=1' + make -j2 TIMED=1 + echo '::endgroup::' + echo '::group::make perf TIMED=1' + make perf TIMED=1 + echo '::endgroup::' + echo '::group::make validate -j2' + make validate -j2 + echo '::endgroup::' + echo '::group::sudo make install install-perf' + sudo make install install-perf + echo '::endgroup::' + echo '::group::make copy-perf OUTPUT="doc-build/${{ matrix.COQ_VERSION }}"' + make copy-perf OUTPUT="doc-build/${{ matrix.COQ_VERSION }}" + echo '::endgroup::' - run: make pdf - run: make doc - - run: make copy-pdf copy-doc copy-perf OUTPUT="doc-build/${COQ_VERSION}" - - run: apt-show-versions $COQ_PACKAGE > doc-build/${COQ_VERSION}/.apt-show-versions + - run: make copy-pdf copy-doc OUTPUT="doc-build/${{ matrix.COQ_VERSION }}" - name: Upload artifact uses: actions/upload-artifact@v2 with: - name: ${{ matrix.env.COQ_VERSION }} - path: doc-build/${{ matrix.env.COQ_VERSION }} + name: ${{ matrix.COQ_VERSION }} + path: doc-build/${{ matrix.COQ_VERSION }} deploy: diff --git a/PerformanceExperiments/gen-listing.sh b/PerformanceExperiments/gen-listing.sh index 882200e59f..ccf3a4467e 100755 --- a/PerformanceExperiments/gen-listing.sh +++ b/PerformanceExperiments/gen-listing.sh @@ -10,7 +10,7 @@ stems="$@" stems="$(echo "$stems" | tr ' ' '\n' | sed 's/\.v$//g' | tr '\n' ' ')" extra_bar="" extra_bar_space="" -coq_versions="$(grep -o 'COQ_VERSION:\s*[^, ]*' .github/workflows/coq.yml | sed 's/COQ_VERSION://g; s/[ "]//g')" +coq_versions="$(grep -o 'COQ_VERSION:.*$' .github/workflows/coq.yml | sed 's/COQ_VERSION://g; s/\[//g; s/\]//g; s/[ "'"'"']//g; s/,/ /g')" for stem in $stems; do stem_dash="$(echo "$stem" | sed 's,[_/],-,g')" echo diff --git a/README.md b/README.md index ac917b7241..2dba602e78 100644 --- a/README.md +++ b/README.md @@ -22,162 +22,162 @@ You can use `make update-README` to regenerate the tables for this README. - [`Reify/BaselineStats`](./PerformanceExperiments/Reify/BaselineStats.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/CanonicalStructures`](./PerformanceExperiments/Reify/CanonicalStructures.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/Ltac2`](./PerformanceExperiments/Reify/Ltac2.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/LtacVariants`](./PerformanceExperiments/Reify/LtacVariants.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/OCaml`](./PerformanceExperiments/Reify/OCaml.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/Parametricity`](./PerformanceExperiments/Reify/Parametricity.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/QuoteFlat`](./PerformanceExperiments/Reify/QuoteFlat.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`Reify/TypeClasses`](./PerformanceExperiments/Reify/TypeClasses.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`n_polymorphic_universes`](./PerformanceExperiments/n_polymorphic_universes.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`pattern`](./PerformanceExperiments/pattern.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`repeat_setoid_rewrite_under_binders`](./PerformanceExperiments/repeat_setoid_rewrite_under_binders.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`repeat_setoid_rewrite_under_binders_noop`](./PerformanceExperiments/repeat_setoid_rewrite_under_binders_noop.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_lift_lets_map`](./PerformanceExperiments/rewrite_lift_lets_map.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_plus_0_tree`](./PerformanceExperiments/rewrite_plus_0_tree.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_autorewrite`](./PerformanceExperiments/rewrite_repeated_app_autorewrite.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_autorewrite_noop`](./PerformanceExperiments/rewrite_repeated_app_autorewrite_noop.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_fast_rewrite`](./PerformanceExperiments/rewrite_repeated_app_fast_rewrite.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_fast_rewrite_ltac2`](./PerformanceExperiments/rewrite_repeated_app_fast_rewrite_ltac2.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_fast_rewrite_no_abstract`](./PerformanceExperiments/rewrite_repeated_app_fast_rewrite_no_abstract.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_rewrite_strat`](./PerformanceExperiments/rewrite_repeated_app_rewrite_strat.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_ssrrewrite`](./PerformanceExperiments/rewrite_repeated_app_ssrrewrite.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_repeated_app_ssrrewrite_noop`](./PerformanceExperiments/rewrite_repeated_app_ssrrewrite_noop.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_strat_under_binders`](./PerformanceExperiments/rewrite_strat_under_binders.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`rewrite_under_lets_plus_0`](./PerformanceExperiments/rewrite_under_lets_plus_0.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`sieve_of_eratosthenes`](./PerformanceExperiments/sieve_of_eratosthenes.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`typeclass_reification_let_in_HOAS`](./PerformanceExperiments/typeclass_reification_let_in_HOAS.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | | - [`typeclass_reification_let_in_PHOAS`](./PerformanceExperiments/typeclass_reification_let_in_PHOAS.v) - master | 8.15.0 | 8.14.1 | 8.13.2 | 8.12.2 | 8.11.2 | 8.10.2 | 8.9.1 | 8.8.2 + dev | 8.15 | 8.14 | 8.13 | 8.12 | 8.11 | 8.10 | 8.9 | 8.8 --|--|--|--|--|--|--|--|-- - | | | | | | | | + | | | | | | | |