diff options
46 files changed, 59 insertions, 414 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 68bb24ac77..5aa0fee16f 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -18,7 +18,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2019-03-01-V43" + CACHEKEY: "bionic_coq-V2019-03-14-V14" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 41392b4b8c..979b5917d4 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-V2019-03-14-V14" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -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" @@ -57,12 +57,11 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ # 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" # 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/11602-herbelin-master+support-only-parsing-where-clause.sh b/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh deleted file mode 100644 index 8b0f86d951..0000000000 --- a/dev/ci/user-overlays/11602-herbelin-master+support-only-parsing-where-clause.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11602" ] || [ "$CI_BRANCH" = "master+support-only-parsing-where-clause" ]; then - - equations_CI_REF=master+adapt-coq-pr11602-only-parsing-where-notation - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -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/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh deleted file mode 100644 index f8871ae158..0000000000 --- a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then - - elpi_CI_REF="simplify-template" - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - equations_CI_REF="simplify-template" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - paramcoq_CI_REF="simplify-template" - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - - mtac2_CI_REF="simplify-template" - mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2 - - rewriter_CI_REF="simplify-template" - rewriter_CI_GITURL=https://github.com/ppedrot/rewriter - -fi diff --git a/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst b/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst new file mode 100644 index 0000000000..c08ebb7f25 --- /dev/null +++ b/doc/changelog/01-kernel/11811-uncheck_positivity_bug.rst @@ -0,0 +1,4 @@ +- **Fixed:** + Allow more inductive types in `Unset Positivity Checking` mode + (`#11811 <https://github.com/coq/coq/pull/11811>`_, + by SimonBoulier). diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 51688e2d9e..0f05237036 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -595,6 +595,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/SeqSeries.v theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v + theories/Reals/Rregisternames.v (theories/Reals/Reals.v) theories/Reals/Runcountable.v </dd> diff --git a/kernel/constr.ml b/kernel/constr.ml index 84eacb196c..fde08743b6 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1297,7 +1297,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = fun t -> fst (sh_rec t) (* Exported hashing fonction on constr, used mainly in plugins. - Appears to have slight differences from [snd (hash_term t)] above ? *) + Slight differences from [snd (hash_term t)] above: it ignores binders + and doesn't do [land 0x3FFFFFFF]. *) let rec hash t = match kind t with @@ -1336,7 +1337,7 @@ let rec hash t = | Float f -> combinesmall 19 (Float64.hash f) and hash_term_array t = - Array.fold_left (fun acc t -> combine (hash t) acc) 0 t + Array.fold_left (fun acc t -> combine acc (hash t)) 0 t module CaseinfoHash = struct diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 58e5e76b61..c5a39262a4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -102,7 +102,7 @@ let failwith_non_pos_list n ntypes l = (* Check the inductive type is called with the expected parameters *) (* [n] is the index of the last inductive type in [env] *) -let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = +let check_correct_par ~chkpos (env,n,ntypes,_) paramdecls ind_index args = let nparams = Context.Rel.nhyps paramdecls in let args = Array.of_list args in if Array.length args < nparams then @@ -123,7 +123,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in raise (IllFormedInd err) in check (nparams-1) (n-nparamdecls) paramdecls; - if not (Array.for_all (noccur_between n ntypes) realargs) then + if chkpos && not (Array.for_all (noccur_between n ntypes) realargs) then failwith_non_pos_vect n ntypes realargs (* Computes the maximum number of recursive parameters: @@ -325,7 +325,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( if check_head then begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> - check_correct_par ienv paramsctxt (ntypes - i) largs + check_correct_par ~chkpos ienv paramsctxt (ntypes - i) largs | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs))) end else diff --git a/test-suite/bugs/closed/bug_11811.v b/test-suite/bugs/closed/bug_11811.v new file mode 100644 index 0000000000..a73494b630 --- /dev/null +++ b/test-suite/bugs/closed/bug_11811.v @@ -0,0 +1,13 @@ + +Unset Positivity Checking. + +Inductive foo : Type -> Type := +| bar : foo (foo unit) +| baz : foo nat. + +Definition toto : forall A, foo A -> {A = foo unit} + {A = nat}. +Proof. + intros A x. destruct x; intuition. +Defined. + +Check (eq_refl : toto _ baz = right eq_refl). diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v new file mode 100644 index 0000000000..7a0f354a53 --- /dev/null +++ b/theories/Reals/Rregisternames.v @@ -0,0 +1,30 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2020 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +Require Import Reals. + +(*****************************************************************) +(** Register names for use in plugins *) +(*****************************************************************) + +Register R as reals.R.type. +Register R0 as reals.R.R0. +Register R1 as reals.R.R1. +Register Rle as reals.R.Rle. +Register Rplus as reals.R.Rplus. +Register Ropp as reals.R.Ropp. +Register Rminus as reals.R.Rminus. +Register Rmult as reals.R.Rmult. +Register Rinv as reals.R.Rinv. +Register Rdiv as reals.R.Rdiv. +Register IZR as reals.R.IZR. +Register Rabs as reals.R.Rabs. +Register sqrt as reals.R.sqrt. +Register powerRZ as reals.R.powerRZ. |