diff options
Diffstat (limited to 'dev')
13 files changed, 10 insertions, 109 deletions
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 9ee6496ee5..51a602303a 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-05-06-V70" +# CACHEKEY: "bionic_coq-V2020-05-18-V3" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -14,12 +14,13 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # Dependencies of stdlib and sphinx doc texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ xindy python3-pip python3-setuptools python3-pexpect python3-bs4 \ + fonts-freefont-otf \ # Dependencies of source-doc and coq-makefile texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 +RUN pip3 install sphinx==2.3.1 sphinx_rtd_theme==0.4.3 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.2 # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh b/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh deleted file mode 100644 index c584438b21..0000000000 --- a/dev/ci/user-overlays/10185-SkySkimmer-instance-no-bang.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then - - quickchick_CI_REF=instance-no-bang - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - -fi diff --git a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh deleted file mode 100644 index 8a734feada..0000000000 --- a/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11703" ] || [ "$CI_BRANCH" = "master+turning-numTok-into-a-numeral-API" ]; then - - quickchick_CI_REF=master+adapting-numTok-new-api-pr11703 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh deleted file mode 100644 index 6928925e54..0000000000 --- a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then - - equations_CI_REF=proof+more_naming_unif - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - rewriter_CI_REF=proof+more_naming_unif - rewriter_CI_GITURL=https://github.com/ejgallego/rewriter - - elpi_CI_REF=proof+more_naming_unif - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh deleted file mode 100644 index 8dae29adb6..0000000000 --- a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then - - equations_CI_REF="export-hint-globality" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - fiat_parsers_CI_REF="export-hint-globality" - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -fi diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh deleted file mode 100644 index e3a8eb07f3..0000000000 --- a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then - - metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual - metacoq_CI_GITURL=https://github.com/ejgallego/metacoq - - elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh deleted file mode 100644 index 4170799be7..0000000000 --- a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then - - elpi_CI_REF=partial-import - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh deleted file mode 100644 index cd6b408813..0000000000 --- a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh +++ /dev/null @@ -1,24 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then - - coqhammer_CI_REF="evar-inst-list" - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - elpi_CI_REF="evar-inst-list" - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - equations_CI_REF="evar-inst-list" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - metacoq_CI_REF="evar-inst-list" - metacoq_CI_GITURL=https://github.com/ppedrot/metacoq - - mtac2_CI_REF="evar-inst-list" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - - quickchick_CI_REF="evar-inst-list" - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - - unicoq_CI_REF="evar-inst-list" - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - -fi diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh deleted file mode 100644 index 6bee3c7bb6..0000000000 --- a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then - - fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto - - mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - - metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - metacoq_CI_GITURL=https://github.com/herbelin/template-coq - - unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file - unimath_CI_GITURL=https://github.com/herbelin/UniMath - -fi diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh deleted file mode 100644 index b5faabcfe1..0000000000 --- a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then - - elpi_CI_REF=no-mod-univs - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh deleted file mode 100644 index 0f8daf418c..0000000000 --- a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then - - equations_CI_REF="refiner-rm-v82" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9498ab8bbb..ae4c6328b5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,5 @@ +## Changes between Coq 8.12 and Coq 8.13 + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index af8a4737be..da9f37f666 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -25,7 +25,10 @@ in time. the next branch point with the `--release` flag (see next section). - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the - branch of the previous version. + branch of the previous version. Note that this commit is the first commit + in the first PR merged in master, not the merge commit for that PR. + After tagging double check that `git describe` picks up + the tag you just made (if not, you tagged the wrong commit). - [ ] Create the `X.X+beta1` milestone if it did not already exist. - [ ] Decide the release calendar with the team (freeze date, beta date, final release date) and put this information in the milestone (using the |