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
--|--|--|--|--|--|--|--|--
- 
| 
| 
| 
| 
| 
| 
| 
| 
+ 
| 
| 
| 
| 
| 
| 
| 
| 