diff options
Diffstat (limited to 'dev')
61 files changed, 165 insertions, 423 deletions
diff --git a/dev/build/osx/make-macos-dmg.sh b/dev/build/osx/make-macos-dmg.sh index 3a096fec06..35d0379008 100755 --- a/dev/build/osx/make-macos-dmg.sh +++ b/dev/build/osx/make-macos-dmg.sh @@ -24,4 +24,14 @@ mkdir -p _build # Temporary countermeasure to hdiutil error 5341 # head -c9703424 /dev/urandom > $DMGDIR/.padding -hdiutil create -imagekey zlib-level=9 -volname "coq-$VERSION-installer-macos" -srcfolder "$DMGDIR" -ov -format UDZO "_build/coq-$VERSION-installer-macos.dmg" +hdi_opts=(-volname "coq-$VERSION-installer-macos" + -srcfolder "$DMGDIR" + -ov # overwrite existing file + -format UDZO + -imagekey "zlib-level=9" + + # needed for backward compat since macOS 10.14 which uses APFS by default + # see discussion in #11803 + -fs hfs+ + ) +hdiutil create "${hdi_opts[@]}" "_build/coq-$VERSION-installer-macos.dmg" diff --git a/dev/ci/README-users.md b/dev/ci/README-users.md index 6649820f22..994ff87674 100644 --- a/dev/ci/README-users.md +++ b/dev/ci/README-users.md @@ -105,5 +105,10 @@ images for testing against Coq master. Using these images is highly recommended: - For Docker, see: https://github.com/coq-community/docker-coq + + The https://github.com/coq-community/docker-coq/wiki/CI-setup wiki + page contains additional information and templates to help setting + Docker-based CI up for your Coq project + - For Nix, see the setup at https://github.com/coq-community/manifesto/wiki/Continuous-Integration-with-Nix diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh index ee6c62673b..7b3e2703b8 100755 --- a/dev/ci/azure-opam.sh +++ b/dev/ci/azure-opam.sh @@ -2,7 +2,7 @@ set -e -x -OPAM_VARIANT=ocaml-variants.4.09.0+mingw64c +OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz tar -xf opam64.tar.xz diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 60c266699c..c18e556da8 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -200,6 +200,13 @@ : "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" ######################################################################## +# bbv +######################################################################## +: "${bbv_CI_REF:=master}" +: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}" +: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}" + +######################################################################## # bedrock2 ######################################################################## : "${bedrock2_CI_REF:=tested}" @@ -214,12 +221,16 @@ : "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" ######################################################################## -# Elpi +# Elpi + Hierarchy Builder ######################################################################## : "${elpi_CI_REF:=coq-master}" : "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" : "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" +: "${elpi_hb_CI_REF:=coq-master}" +: "${elpi_hb_CI_GITURL:=https://github.com/math-comp/hierarchy-builder}" +: "${elpi_hb_CI_ARCHIVEURL:=${elpi_hb_CI_GITURL}/archive}" + ######################################################################## # fcsl-pcm ######################################################################## @@ -326,3 +337,10 @@ : "${perennial_CI_REF:=master}" : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" + +######################################################################## +# metacoq +######################################################################## +: "${metacoq_CI_REF:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" +: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh new file mode 100755 index 0000000000..6892cea3e4 --- /dev/null +++ b/dev/ci/ci-bbv.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download bbv + +( cd "${CI_BUILD_DIR}/bbv" && make && make install ) diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 7aa265cf90..f0dbe485f7 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -19,7 +19,7 @@ then elif [ -d "$PWD/_build/install/default/" ]; then # Dune build - export OCAMLPATH="$PWD/_build/install/default/lib/" + export OCAMLPATH="$PWD/_build/install/default/lib/:$OCAMLPATH" export COQBIN="$PWD/_build/install/default/bin" export COQLIB="$PWD/_build/install/default/lib/coq" CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" diff --git a/dev/ci/ci-elpi.sh b/dev/ci/ci-elpi.sh index d60bf34ba2..4f185db813 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -6,3 +6,7 @@ ci_dir="$(dirname "$0")" git_download elpi ( cd "${CI_BUILD_DIR}/elpi" && make && make install ) + +git_download elpi_hb + +( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install ) diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh index 871d033f5b..30047e624b 100755 --- a/dev/ci/ci-equations.sh +++ b/dev/ci/ci-equations.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download equations -( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci) +( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh new file mode 100755 index 0000000000..1302065961 --- /dev/null +++ b/dev/ci/ci-metacoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download metacoq + +( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 41392b4b8c..e56e4d38ea 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2019-03-01-V43" +# CACHEKEY: "bionic_coq-V2020-03-19-V29" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -18,7 +18,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-science tipa # More dependencies of the sphinx doc -RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \ +RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \ antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0 # We need to install OPAM 2.0 manually for now. @@ -37,12 +37,12 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.0.8 odoc.1.4.2" \ +ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ BASE_ONLY_OPAM="elpi.1.10.2" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" +ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" # Must add this to COQIDE_OPAM{,_EDGE} when we update the opam # packages "lablgtk3-gtksourceview3" @@ -56,13 +56,12 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ opam install $BASE_OPAM # EDGE switch -ENV COMPILER_EDGE="4.09.0" \ - COQIDE_OPAM_EDGE="cairo2.0.6.1 lablgtk3-sourceview3.3.0.beta6" \ - BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12" +ENV COMPILER_EDGE="4.09.1" \ + BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0" # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch create "${COMPILER_EDGE}+flambda" && eval $(opam env) && \ - opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + opam install $BASE_OPAM $BASE_OPAM_EDGE $COQIDE_OPAM $CI_OPAM RUN opam clean -a -c diff --git a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh deleted file mode 100644 index 242b177d71..0000000000 --- a/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh +++ /dev/null @@ -1,23 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8726" ] || [ "$CI_BRANCH" = "master+more-stable-meaning-to-Discharge-flag" ]; then - - fiat_parsers_CI_BRANCH=master+change-for-coq-pr8726 - fiat_parsers_CI_REF=master+change-for-coq-pr8726 - fiat_parsers_CI_GITURL=https://github.com/herbelin/fiat - - elpi_CI_BRANCH=coq-master+fix-global-pr8726 - elpi_CI_REF=coq-master+fix-global-pr8726 - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - - equations_CI_BRANCH=master+fix-global-pr8726 - equations_CI_REF=master+fix-global-pr8726 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_BRANCH=master+fix-global-pr8726 - mtac2_CI_REF=master+fix-global-pr8726 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - - paramcoq_CI_BRANCH=master+fix-global-pr8726 - paramcoq_CI_REF=master+fix-global-pr8726 - paramcoq_CI_GITURL=https://github.com/herbelin/paramcoq - -fi diff --git a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh deleted file mode 100644 index e4cf74aa51..0000000000 --- a/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9566" ] || [ "$CI_BRANCH" = "proof_global+move_termination_routine_out" ]; then - - aac_tactics_CI_REF=proof_global+move_termination_routine_out - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - equations_CI_REF=proof_global+move_termination_routine_out - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - paramcoq_CI_REF=proof_global+move_termination_routine_out - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh deleted file mode 100644 index 3029f3019c..0000000000 --- a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then - - equations_CI_REF=proof+sayonara_baby - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+sayonara_baby - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+sayonara_baby - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09867-primitive-floats.sh b/dev/ci/user-overlays/09867-primitive-floats.sh deleted file mode 100644 index a0e9085afd..0000000000 --- a/dev/ci/user-overlays/09867-primitive-floats.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9867" ] || [ "$CI_BRANCH" = "primitive-floats" ]; then - - unicoq_CI_REF=primitive-floats - unicoq_CI_GITURL=https://github.com/validsdp/unicoq - - elpi_CI_REF=primitive-floats - elpi_CI_GITURL=https://github.com/validsdp/coq-elpi - - coqhammer_CI_REF=primitive-floats - coqhammer_CI_GITURL=https://github.com/validsdp/coqhammer - -fi diff --git a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh b/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh deleted file mode 100644 index 87dad61dbc..0000000000 --- a/dev/ci/user-overlays/10204-rm-unsafe-type-of-coercion.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10204" ] || [ "$CI_BRANCH" = "rm-unsafe-type-of-coercion" ]; then - - paramcoq_CI_REF=fix-papp - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - -fi diff --git a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh b/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh deleted file mode 100644 index c8cf85e73e..0000000000 --- a/dev/ci/user-overlays/10231-herbelin-master+locating-warning-different-implicit-term-type.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10231" ] || [ "$CI_BRANCH" = "master+locating-warning-different-implicit-term-type" ]; then - - equations_CI_REF=master+fix-manual-implicit-pr10231 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - mtac2_CI_REF=master+fix-manual-implicit-pr10231 - mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 - -fi diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh deleted file mode 100644 index d133bc9993..0000000000 --- a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then - - elpi_CI_REF=proof+recthms - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+recthms - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+recthms - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+recthms - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+recthms - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh b/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh deleted file mode 100644 index c5f1510357..0000000000 --- a/dev/ci/user-overlays/10319-SkySkimmer-vernac-when-sideff.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10319" ] || [ "$CI_BRANCH" = "vernac-when-sideff" ]; then - - mtac2_CI_REF=vernac-when-sideff - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - equations_CI_REF=vernac-when-sideff - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh deleted file mode 100644 index 2c3f490c03..0000000000 --- a/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10334" ] || [ "$CI_BRANCH" = "rm-kernel-sideeff-role" ]; then - - equations_CI_REF=rm-kernel-sideeff-role - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh b/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh deleted file mode 100644 index 288e14c866..0000000000 --- a/dev/ci/user-overlays/10337-ejgallego-vernac+qed_special_case_inject_proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10337" ] || [ "$CI_BRANCH" = "vernac+qed_special_case_inject_proof" ]; then - - paramcoq_CI_REF=vernac+qed_special_case_inject_proof - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=vernac+qed_special_case_inject_proof - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh b/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh deleted file mode 100644 index 735b2ebbc3..0000000000 --- a/dev/ci/user-overlays/10362-ppedrot-delay-poly-opaque.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10362" ] || [ "$CI_BRANCH" = "delay-poly-opaque" ]; then - - paramcoq_CI_REF=delay-poly-opaque - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - - elpi_CI_REF=delay-poly-opaque - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - coqhammer_CI_REF=delay-poly-opaque - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - coq_dpdgraph_CI_REF=delay-poly-opaque - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh b/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh deleted file mode 100644 index 3122f953de..0000000000 --- a/dev/ci/user-overlays/10406-ppedrot-desync-entry-proof.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10406" ] || [ "$CI_BRANCH" = "desync-entry-proof" ]; then - - equations_CI_REF=desync-entry-proof - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - quickchick_CI_REF=desync-entry-proof - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - -fi diff --git a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh b/dev/ci/user-overlays/10419-ejgallego-heads+test.sh deleted file mode 100644 index 0ec0c3673a..0000000000 --- a/dev/ci/user-overlays/10419-ejgallego-heads+test.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10419" ] || [ "$CI_BRANCH" = "heads+test" ]; then - - elpi_CI_REF=heads+test - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=heads+test - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=heads+test - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=heads+test - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=heads+test - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh b/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh deleted file mode 100644 index 3a2f4e1001..0000000000 --- a/dev/ci/user-overlays/10434-ejgallego-proof+hook_record.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10434" ] || [ "$CI_BRANCH" = "proof+hook_record" ]; then - - equations_CI_REF=proof+hook_record - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=proof+hook_record - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+hook_record - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh b/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh deleted file mode 100644 index 00f544f894..0000000000 --- a/dev/ci/user-overlays/10441-ppedrot-static-poly-section.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10441" ] || [ "$CI_BRANCH" = "static-poly-section" ]; then - - ext_lib_CI_REF=static-poly-section - ext_lib_CI_GITURL=https://github.com/ppedrot/coq-ext-lib - -fi diff --git a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh b/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh deleted file mode 100644 index 10526a9ffe..0000000000 --- a/dev/ci/user-overlays/10476-maximedenes-rm-library-optim.sh +++ /dev/null @@ -1,10 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10476" ] || [ "$CI_BRANCH" = "rm-library-optim" ]; then - - sf_lf_CI_TARURL=https://www.maximedenes.fr/download/lf.tgz - sf_plf_CI_TARURL=https://www.maximedenes.fr/download/plf.tgz - sf_vfa_CI_TARURL=https://www.maximedenes.fr/download/vfa.tgz - - vst_CI_REF=fix-export - vst_CI_GITURL=https://github.com/maximedenes/VST - -fi diff --git a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh b/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh deleted file mode 100644 index 7001c3d0c8..0000000000 --- a/dev/ci/user-overlays/10516-ejgallego-proof+dup_save.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10516" ] || [ "$CI_BRANCH" = "proof+dup_save" ]; then - - elpi_CI_REF=proof+dup_save - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh deleted file mode 100644 index 413805e8e9..0000000000 --- a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then - - elpi_CI_REF=feedback-added-axiom - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh b/dev/ci/user-overlays/10660-ejgallego-errors+private.sh deleted file mode 100644 index 21ff60493b..0000000000 --- a/dev/ci/user-overlays/10660-ejgallego-errors+private.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10660" ] || [ "$CI_BRANCH" = "errors+private" ]; then - - coqhammer_CI_REF=errors+private - coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - -fi diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh deleted file mode 100644 index 0c47f6a60b..0000000000 --- a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then - - elpi_CI_REF=api+varkind - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=api+varkind - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh b/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh deleted file mode 100644 index 6dc44aa627..0000000000 --- a/dev/ci/user-overlays/10674-ejgallego-proofs+declare_unif.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10674" ] || [ "$CI_BRANCH" = "proofs+declare_unif" ]; then - - equations_CI_REF=proofs+declare_unif - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh b/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh deleted file mode 100644 index f4840c2a83..0000000000 --- a/dev/ci/user-overlays/10681-ejgallego-proof+private_entry.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10681" ] || [ "$CI_BRANCH" = "proof+private_entry" ]; then - - equations_CI_REF=proof+private_entry - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh b/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh deleted file mode 100644 index a5f6551474..0000000000 --- a/dev/ci/user-overlays/10727-ejgallego-library+to_vernac_step2.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10727" ] || [ "$CI_BRANCH" = "library+to_vernac_step2" ]; then - - elpi_CI_REF=library+to_vernac_step2 - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh b/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh deleted file mode 100644 index d7af6b7a36..0000000000 --- a/dev/ci/user-overlays/10811-SkySkimmer-sprop-default-on.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10811" ] || [ "$CI_BRANCH" = "sprop-default-on" ]; then - - elpi_CI_REF=sprop-default-on - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - coq_dpdgraph_CI_REF=sprop-default-on - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh b/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh deleted file mode 100644 index c17fe4fcba..0000000000 --- a/dev/ci/user-overlays/10832-herbelin-master+fix6082-7766-overriding-notation-format.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10832" ] || [ "$CI_BRANCH" = "master+fix6082-7766-overriding-notation-format" ]; then - - equations_CI_REF=master+fix-interpretation-notation-format-pr10832 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - - quickchick_CI_REF=master+fix-interpretation-notation-format-pr10832 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh b/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh deleted file mode 100644 index bb65beb043..0000000000 --- a/dev/ci/user-overlays/11027-SkySkimmer-expose-comind-univ.sh +++ /dev/null @@ -1,19 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11027" ] || [ "$CI_BRANCH" = "cleanup-comind-univ" ]; then - - elpi_CI_REF=expose-comind-univ - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=expose-comind-univ - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=expose-comind-univ - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - mtac2_CI_REF=expose-comind-univ - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - rewriter_CI_REF=cleanup-comind-univ - rewriter_CI_GITURL=https://github.com/SkySkimmer/rewriter - - -fi diff --git a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh b/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh deleted file mode 100644 index fb66217487..0000000000 --- a/dev/ci/user-overlays/11141-herbelin-master+labelled-pr_lconstr-and-co.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11141" ] || [ "$CI_BRANCH" = "master+labelled-pr_lconstr-and-co" ]; then - - quickchick_CI_REF=master+adapt-coq-pr11141 - quickchick_CI_GITURL=https://github.com/herbelin/QuickChick - -fi diff --git a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh b/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh deleted file mode 100644 index e0d9dc6469..0000000000 --- a/dev/ci/user-overlays/11172-herbelin-master+coercion-notation-interleaved-printing.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11172" ] || [ "$CI_BRANCH" = "master+coercion-notation-interleaved-printing" ]; then - - elpi_CI_REF=coq-master+mini-fix-mkGApp - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh deleted file mode 100644 index fd63980036..0000000000 --- a/dev/ci/user-overlays/11235-non-maximal-implicit.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]; then - - quickchick_CI_REF=non_maximal_implicit - quickchick_CI_GITURL=https://github.com/SimonBoulier/QuickChick - - elpi_CI_REF=non_maximal_implicit - elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh b/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh deleted file mode 100644 index a95170a455..0000000000 --- a/dev/ci/user-overlays/11293-ppedrot-rename-class-files.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11293" ] || [ "$CI_BRANCH" = "rename-class-files" ]; then - - elpi_CI_REF=rename-class-files - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - mtac2_CI_REF=rename-class-files - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - -fi diff --git a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh b/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh deleted file mode 100644 index f41271804a..0000000000 --- a/dev/ci/user-overlays/11338-ppedrot-rm-global-uses-evd.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11338" ] || [ "$CI_BRANCH" = "rm-global-uses-evd" ]; then - - unicoq_CI_REF=rm-global-uses-evd - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - - equations_CI_REF=rm-global-uses-evd - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/11368-trailing-implicit-error.sh b/dev/ci/user-overlays/11368-trailing-implicit-error.sh deleted file mode 100644 index a125337dd9..0000000000 --- a/dev/ci/user-overlays/11368-trailing-implicit-error.sh +++ /dev/null @@ -1,33 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11368" ] || [ "$CI_BRANCH" = "trailing_implicit_error" ]; then - - mathcomp_CI_REF=non_maximal_implicit - mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp - - oddorder_CI_REF=non_maximal_implicit - oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order - - stdlib2_CI_REF=non_maximal_implicit - stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2 - - coq_dpdgraph_CI_REF=non_maximal_implicit - coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph - - vst_CI_REF=non_maximal_implicit - vst_CI_GITURL=https://github.com/SimonBoulier/VST - - equations_CI_REF=non_maximal_implicit - equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations - - mtac2_CI_REF=non_maximal_implicit - mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2 - - relation_algebra_CI_REF=non_maximal_implicit - relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra - - fiat_parsers_CI_REF=non_maximal_implicit - fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat - - Corn_CI_REF=non_maximal_implicit - Corn_CI_GITURL=https://github.com/SimonBoulier/corn - -fi diff --git a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh b/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh deleted file mode 100644 index 5fb29e1826..0000000000 --- a/dev/ci/user-overlays/11417-ppedrot-rm-kind-of-type.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11417" ] || [ "$CI_BRANCH" = "rm-kind-of-type" ]; then - - elpi_CI_REF=rm-kind-of-type - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - -fi diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh deleted file mode 100644 index f2a431978d..0000000000 --- a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then - - coqhammer_CI_REF=no-optname - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - equations_CI_REF=no-optname - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - unicoq_CI_REF=no-optname - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - paramcoq_CI_REF=no-optname - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - -fi diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh deleted file mode 100644 index 913b39c30c..0000000000 --- a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then - - equations_CI_REF=template-directify - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=template-directify - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - elpi_CI_REF=template-directify - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -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 new file mode 100644 index 0000000000..8a734feada --- /dev/null +++ b/dev/ci/user-overlays/11703-herbelin-master+turning-numTok-into-a-numeral-API.sh @@ -0,0 +1,6 @@ +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/11708-gares-elpi-1.10.sh b/dev/ci/user-overlays/11708-gares-elpi-1.10.sh deleted file mode 100644 index 121190e5f6..0000000000 --- a/dev/ci/user-overlays/11708-gares-elpi-1.10.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11708" ] || [ "$CI_BRANCH" = " elpi-1.10+coq-elpi-1.3" ]; then - - elpi_CI_REF="coq-master+coq-elpi-1.3" - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -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 new file mode 100644 index 0000000000..6928925e54 --- /dev/null +++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh @@ -0,0 +1,12 @@ +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 new file mode 100644 index 0000000000..8dae29adb6 --- /dev/null +++ b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh @@ -0,0 +1,9 @@ +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/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 777eec97c6..0506216541 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -125,10 +125,9 @@ dune exec -- dev/dune-dbg checker foo.vo (ocd) source dune_db ``` -Unfortunately, dependency handling here is not fully refined, so you -need to build enough of Coq once to use this target [it will then -correctly compute the deps and rebuild if you call the script again] -This will be fixed in the future. +Unfortunately, dependency handling is not fully refined / automated, +you may find the occasional hiccup due to libraries being renamed, +etc... Please report any issue. For running in emacs, use `coqdev-ocamldebug` from `coqdev.el`. diff --git a/dev/doc/changes.md b/dev/doc/changes.md index d5938713d6..eac8d86b0a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,13 +1,22 @@ ## Changes between Coq 8.11 and Coq 8.12 -### ML API +### Code formatting -Types `precedence`, `parenRelation`, `tolerability` in -`notgram_ops.ml` have been reworked. See `entry_level` and -`entry_relative_level` in `constrexpr.ml`. +- The automatic code formatting tool `ocamlformat` is enabled now for + the micromega codebase. Version 0.13.0 is required. See + `ocalmformat`'s documentation for more details on integration with + your editor. ### ML API +Notations: + +- Most operators on numerals have moved to file numTok.ml. + +- Types `precedence`, `parenRelation`, `tolerability` in + `notgram_ops.ml` have been reworked. See `entry_level` and + `entry_relative_level` in `constrexpr.ml`. + Exception handling: - Coq's custom `Backtrace` module has been removed in favor of OCaml's @@ -21,6 +30,11 @@ Exception handling: + printers are of type `exn -> Pp.t option` [`None` == not handled] + it is forbidden for exception printers to raise. +- Refiner.catchable_exception is deprecated, use instead + CErrors.noncritical in try-with block. Note that nothing is needed in + tclORELSE block since the exceptions there are supposed to be + non-critical by construction. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been @@ -9,12 +9,34 @@ (rule (targets dune-dbg) - (deps dune-dbg.in - ../checker/coqchk.bc - ../topbin/coqc_bin.bc - ../ide/coqide_main.bc - %{lib:coq.plugins.ltac:ltac_plugin.cma} - ; This is not enough, the call to `ocamlfind` may fail if the - ; META file is not yet in place :/ - top_printers.cma) + (deps + dune-dbg.in + ../checker/coqchk.bc + ../topbin/coqc_bin.bc + ../ide/coqide_main.bc + ; We require all the OCaml libs to be in place and searchable + ; by OCamlfind, this is a bit of a hack but until Dune gets + ; proper ocamldebug support we have to live with that. + %{lib:coq.config:config.cma} + %{lib:coq.clib:clib.cma} + %{lib:coq.lib:lib.cma} + %{lib:coq.kernel:kernel.cma} + %{lib:coq.vm:byterun.cma} + %{lib:coq.vm:../../stublibs/dllbyterun_stubs.so} + %{lib:coq.library:library.cma} + %{lib:coq.engine:engine.cma} + %{lib:coq.pretyping:pretyping.cma} + %{lib:coq.gramlib:gramlib.cma} + %{lib:coq.interp:interp.cma} + %{lib:coq.proofs:proofs.cma} + %{lib:coq.parsing:parsing.cma} + %{lib:coq.printing:printing.cma} + %{lib:coq.tactics:tactics.cma} + %{lib:coq.vernac:vernac.cma} + %{lib:coq.stm:stm.cma} + %{lib:coq.toplevel:toplevel.cma} + %{lib:coq.plugins.ltac:ltac_plugin.cma} + %{lib:coq.top_printers:top_printers.cmi} + %{lib:coq.top_printers:top_printers.cma} + %{lib:coq.top_printers:../META}) (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 49e338d0a5..556493ffad 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -3,5 +3,5 @@ ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) (context (opam (switch 4.05.0+32bit))) -(context (opam (switch 4.09.0))) -(context (opam (switch 4.09.0+flambda))) +(context (opam (switch 4.09.1))) +(context (opam (switch 4.09.1+flambda))) diff --git a/dev/header.c b/dev/header.c index 6201cb3b73..f31efcba47 100644 --- a/dev/header.c +++ b/dev/header.c @@ -1,7 +1,7 @@ /************************************************************************/ /* * The Coq Proof Assistant / The Coq Development Team */ -/* v * INRIA, CNRS and contributors - Copyright 1999-2019 */ -/* <O___,, * (see CREDITS file for the list of authors) */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ /* \VV/ **************************************************************/ /* // * This file is distributed under the terms of the */ /* * GNU Lesser General Public License Version 2.1 */ diff --git a/dev/header.ml b/dev/header.ml index 87553dcb56..b72d544151 100644 --- a/dev/header.ml +++ b/dev/header.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/dev/header.py b/dev/header.py index 86114503d4..2c39321f19 100644 --- a/dev/header.py +++ b/dev/header.py @@ -1,7 +1,7 @@ ########################################################################## ## # The Coq Proof Assistant / The Coq Development Team ## -## v # INRIA, CNRS and contributors - Copyright 1999-2019 ## -## <O___,, # (see CREDITS file for the list of authors) ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## ## \VV/ ############################################################### ## // # This file is distributed under the terms of the ## ## # GNU Lesser General Public License Version 2.1 ## diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 54baaee1fe..b8a696ef21 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/8da81465c19fca393a3b17004c743e4d82a98e4f.tar.gz"; - sha256 = "1f3s27nrssfk413pszjhbs70wpap43bbjx2pf4zq5x2c1kd72l6y"; + url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz"; + sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w"; }) diff --git a/dev/tools/change-header b/dev/tools/change-header index 59c6f43958..3b0a9d1ef9 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -43,6 +43,7 @@ for i in $(git grep --name-only --fixed-strings "$(head -1 $oldheader)"); do mv $i.tmp$$ $i modified=$(expr $modified + 1) else + echo "$i: header unchanged" kept=$(expr $kept + 1) fi rm $i.head.tmp$$ diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg index da224aa5ab..06db787488 100644 --- a/dev/top_printers.dbg +++ b/dev/top_printers.dbg @@ -24,6 +24,8 @@ install_printer Top_printers.ppglob_constr install_printer Top_printers.pppattern install_printer Top_printers.ppfconstr install_printer Top_printers.ppbigint +install_printer Top_printers.ppnumtokunsigned +install_printer Top_printers.ppnumtokunsignednat install_printer Top_printers.ppintset install_printer Top_printers.ppidset install_printer Top_printers.ppidmapgen diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e8129938a1..7002cbffac 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -82,10 +82,12 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x)) -let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e))) +let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e))) let ppfconstr c = ppconstr (CClosure.term_of_fconstr c) let ppbigint n = pp (str (Bigint.to_string n));; +let ppnumtokunsigned n = pp (NumTok.Unsigned.print n) +let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n) let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) diff --git a/dev/top_printers.mli b/dev/top_printers.mli index ac9b63f60a..c826391cac 100644 --- a/dev/top_printers.mli +++ b/dev/top_printers.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -54,6 +54,8 @@ val pppattern : Pattern.constr_pattern -> unit val ppfconstr : CClosure.fconstr -> unit val ppbigint : Bigint.bigint -> unit +val ppnumtokunsigned : NumTok.Unsigned.t -> unit +val ppnumtokunsignednat : NumTok.UnsignedNat.t -> unit val ppintset : Int.Set.t -> unit val ppidset : Names.Id.Set.t -> unit |