diff options
Diffstat (limited to 'dev')
40 files changed, 102 insertions, 346 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 95fceb773a..fa39b41565 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,7 +215,7 @@ ######################################################################## # simple-io ######################################################################## -: "${simple_io_CI_REF:=dev}" +: "${simple_io_CI_REF:=master}" : "${simple_io_CI_GITURL:=https://github.com/Lysxia/coq-simple-io}" : "${simple_io_CI_ARCHIVEURL:=${simple_io_CI_GITURL}/archive}" diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index bba17314f7..e8c8d22678 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -11,7 +11,7 @@ git_download fiat_crypto # c.f. https://github.com/coq/coq/pull/8313#issuecomment-416650241 fiat_crypto_CI_TARGETS1="c-files printlite lite" -fiat_crypto_CI_TARGETS2="print-nobigmem nobigmem" +fiat_crypto_CI_TARGETS2="coq" ( cd "${CI_BUILD_DIR}/fiat_crypto" && git submodule update --init --recursive && \ ulimit -s 32768 && \ diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh deleted file mode 100644 index 2b4c1489ad..0000000000 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ /dev/null @@ -1,13 +0,0 @@ -_OVERLAY_BRANCH=ho-matching-occ-sel - -if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then - - unicoq_CI_REF="PR7819-overlay" - - mtac2_CI_REF="PR7819-overlay" - mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 - - equations_CI_GITURL=https://github.com/mattam82/Coq-Equations - equations_CI_REF="PR7819-overlay" - -fi 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 new file mode 100644 index 0000000000..242b177d71 --- /dev/null +++ b/dev/ci/user-overlays/08726-herbelin-master+more-stable-meaning-to-Discharge-flag.sh @@ -0,0 +1,23 @@ +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/08764-validsdp-master-parsing-decimal.sh b/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh deleted file mode 100644 index 67f6f8610a..0000000000 --- a/dev/ci/user-overlays/08764-validsdp-master-parsing-decimal.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8764" ] || [ "$CI_BRANCH" = "master-parsing-decimal" ]; then - - ltac2_CI_REF=master-parsing-decimal - ltac2_CI_GITURL=https://github.com/proux01/ltac2 - - quickchick_CI_REF=master-parsing-decimal - quickchick_CI_GITURL=https://github.com/proux01/QuickChick - - Corn_CI_REF=master-parsing-decimal - Corn_CI_GITURL=https://github.com/proux01/corn - - HoTT_CI_REF=master-parsing-decimal - HoTT_CI_GITURL=https://github.com/proux01/HoTT - - stdlib2_CI_REF=master-parsing-decimal - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - -fi diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh deleted file mode 100644 index 81e18226ed..0000000000 --- a/dev/ci/user-overlays/08817-sprop.sh +++ /dev/null @@ -1,34 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then - aac_tactics_CI_REF=sprop - aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics - - coq_dpdgraph_CI_REF=sprop - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - - coqhammer_CI_REF=sprop - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - elpi_CI_REF=sprop - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sprop - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - ltac2_CI_REF=sprop - ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 - - unicoq_CI_REF=sprop - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - mtac2_CI_REF=sprop - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sprop - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - quickchick_CI_REF=sprop - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - - relation_algebra_CI_REF=sprop - relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra -fi diff --git a/dev/ci/user-overlays/08829-proj-syntax-check.sh b/dev/ci/user-overlays/08829-proj-syntax-check.sh deleted file mode 100644 index c04621114f..0000000000 --- a/dev/ci/user-overlays/08829-proj-syntax-check.sh +++ /dev/null @@ -1,5 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8829" ] || [ "$CI_BRANCH" = "proj-syntax-check" ]; then - lambdaRust_CI_REF=proj-syntax-check - lambdaRust_CI_GITURL=https://github.com/SkySkimmer/lambda-rust - lambdaRust_CI_ARCHIVEURL=$lambdaRust_CI_GITURL/archive -fi diff --git a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh b/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh deleted file mode 100644 index dc39ea5ef0..0000000000 --- a/dev/ci/user-overlays/08893-herbelin-master+moving-evars-of-term-on-econstr.sh +++ /dev/null @@ -1,7 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8893" ] || [ "$CI_BRANCH" = "master+moving-evars-of-term-on-econstr" ]; then - - equations_CI_BRANCH=master+fix-evars_of_term-pr8893 - equations_CI_REF=master+fix-evars_of_term-pr8893 - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh b/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh deleted file mode 100644 index 12be1b676a..0000000000 --- a/dev/ci/user-overlays/08984-vbgl-rm-hardwired-hint-db.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8984" ] || [ "$CI_BRANCH" = "rm-hardwired-hint-db" ]; then - - HoTT_CI_REF=rm-hardwired-hint-db - HoTT_CI_GITURL=https://github.com/vbgl/HoTT - - ltac2_CI_REF=rm-hardwired-hint-db - ltac2_CI_GITURL=https://github.com/vbgl/ltac2 - - UniMath_CI_REF=rm-hardwired-hint-db - UniMath_CI_GITURL=https://github.com/vbgl/UniMath - -fi diff --git a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh b/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh deleted file mode 100644 index c09d1b8929..0000000000 --- a/dev/ci/user-overlays/09129-ejgallego-proof+no_global_partial.sh +++ /dev/null @@ -1,30 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9129" ] || [ "$CI_BRANCH" = "proof+no_global_partial" ]; then - - aac_tactics_CI_REF=proof+no_global_partial - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - # coqhammer_CI_REF=proof+no_global_partial - # coqhammer_CI_GITURL=https://github.com/ejgallego/coqhammer - - elpi_CI_REF=proof+no_global_partial - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - equations_CI_REF=proof+no_global_partial - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - ltac2_CI_REF=proof+no_global_partial - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - # unicoq_CI_REF=proof+no_global_partial - # unicoq_CI_GITURL=https://github.com/ejgallego/unicoq - - mtac2_CI_REF=proof+no_global_partial - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=proof+no_global_partial - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - quickchick_CI_REF=proof+no_global_partial - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh b/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh deleted file mode 100644 index 1e1d36d54a..0000000000 --- a/dev/ci/user-overlays/09165-ejgallego-recarg-cleanup.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9165" ] || [ "$CI_BRANCH" = "recarg-cleanup" ]; then - - elpi_CI_REF=recarg-cleanup - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - quickchick_CI_REF=recarg-cleanup - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh b/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh deleted file mode 100644 index 23eb24c304..0000000000 --- a/dev/ci/user-overlays/09173-ejgallego-proofview+proof_info.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9173" ] || [ "$CI_BRANCH" = "proofview+proof_info" ]; then - - ltac2_CI_REF=proofview+proof_info - ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 - - fiat_parsers_CI_REF=proofview+proof_info - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat - -fi diff --git a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh b/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh deleted file mode 100644 index 1110157069..0000000000 --- a/dev/ci/user-overlays/09389-SkySkimmer-set-implicits.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9389" ] || [ "$CI_BRANCH" = "set-implicits" ]; then - - equations_CI_REF=set-implicits - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=set-implicits - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09439-sep-variance.sh b/dev/ci/user-overlays/09439-sep-variance.sh deleted file mode 100644 index cca85a2f68..0000000000 --- a/dev/ci/user-overlays/09439-sep-variance.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then - elpi_CI_REF=sep-variance - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=sep-variance - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - mtac2_CI_REF=sep-variance - mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2 - - paramcoq_CI_REF=sep-variance - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq -fi diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh deleted file mode 100644 index 1af8b5430d..0000000000 --- a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then - - quickchick_CI_REF=context-constructor - quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick - - equations_CI_REF=context-constructor - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -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 new file mode 100644 index 0000000000..e4cf74aa51 --- /dev/null +++ b/dev/ci/user-overlays/09566-ejgallego-proof_global+move_termination_routine_out.sh @@ -0,0 +1,12 @@ +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/09567-ejgallego-hooks_unify.sh b/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh deleted file mode 100644 index 27ce9aca16..0000000000 --- a/dev/ci/user-overlays/09567-ejgallego-hooks_unify.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9567" ] || [ "$CI_BRANCH" = "hooks_unify" ]; then - - equations_CI_REF=hooks_unify - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - mtac2_CI_REF=hooks_unify - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=hooks_unify - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - -fi diff --git a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh b/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh deleted file mode 100644 index 18a295cdbb..0000000000 --- a/dev/ci/user-overlays/09602-gares-more-delta-in-termination-checking.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9602" ] || [ "$CI_BRANCH" = "more-delta-in-termination-checking" ]; then - - equations_CI_REF=more-delta-in-termination-checking - equations_CI_GITURL=https://github.com/gares/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/09678-printed-by-env.sh b/dev/ci/user-overlays/09678-printed-by-env.sh deleted file mode 100644 index ccb3498764..0000000000 --- a/dev/ci/user-overlays/09678-printed-by-env.sh +++ /dev/null @@ -1,14 +0,0 @@ - -if [ "$CI_PULL_REQUEST" = "9678" ] || [ "$CI_BRANCH" = "printed-by-env" ]; then - elpi_CI_REF=printed-by-env - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - equations_CI_REF=printed-by-env - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=printed-by-env - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - quickchick_CI_REF=printed-by-env - quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick -fi diff --git a/dev/ci/user-overlays/09733-gares-quotations.sh b/dev/ci/user-overlays/09733-gares-quotations.sh deleted file mode 100644 index b17454fc4c..0000000000 --- a/dev/ci/user-overlays/09733-gares-quotations.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9733" ] || [ "$CI_BRANCH" = "quotations" ]; then - - ltac2_CI_REF=quotations - ltac2_CI_GITURL=https://github.com/gares/ltac2 - -fi diff --git a/dev/ci/user-overlays/09815-token-type.sh b/dev/ci/user-overlays/09815-token-type.sh deleted file mode 100644 index 4b49011de3..0000000000 --- a/dev/ci/user-overlays/09815-token-type.sh +++ /dev/null @@ -1,4 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9815" ] || [ "$CI_BRANCH" = "token-type" ]; then - ltac2_CI_REF=token-type - ltac2_CI_GITURL=https://github.com/proux01/ltac2 -fi diff --git a/dev/ci/user-overlays/09870-vbgl-recordops.sh b/dev/ci/user-overlays/09870-vbgl-recordops.sh deleted file mode 100644 index bb14a8c204..0000000000 --- a/dev/ci/user-overlays/09870-vbgl-recordops.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9870" ] || [ "$CI_BRANCH" = "doc-canonical" ]; then - - elpi_CI_REF=pr-9870 - elpi_CI_GITURL=https://github.com/vbgl/coq-elpi - -fi diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh deleted file mode 100644 index 9a42c829ce..0000000000 --- a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then - - quickchick_CI_REF=require+upper - quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick - -fi diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh deleted file mode 100644 index 01d3068591..0000000000 --- a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh +++ /dev/null @@ -1,21 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then - - elpi_CI_REF=pretyping-rm-global - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - coqhammer_CI_REF=pretyping-rm-global - coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer - - equations_CI_REF=pretyping-rm-global - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - - ltac2_CI_REF=pretyping-rm-global - ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 - - paramcoq_CI_REF=pretyping-rm-global - paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq - - mtac2_CI_REF=pretyping-rm-global - mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 - -fi diff --git a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh b/dev/ci/user-overlays/09973-gares-elpi-2.1.sh deleted file mode 100644 index 9a6e25d893..0000000000 --- a/dev/ci/user-overlays/09973-gares-elpi-2.1.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "9973" ] || [ "$CI_BRANCH" = "elpi-1.2" ]; then - - elpi_CI_REF=overlay-elpi1.2-coq-master - elpi_CI_GITURL=https://github.com/LPCIC/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh b/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh deleted file mode 100644 index 9f9cc19e83..0000000000 --- a/dev/ci/user-overlays/10052-ppedrot-cleanup-logic-convert-hyp.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10052" ] || [ "$CI_BRANCH" = "cleanup-logic-convert-hyp" ]; then - - relation_algebra_CI_REF=cleanup-logic-convert-hyp - relation_algebra_CI_GITURL=https://github.com/ppedrot/relation-algebra - -fi diff --git a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh b/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh deleted file mode 100644 index 0e1449f36c..0000000000 --- a/dev/ci/user-overlays/10069-ppedrot-whd-for-evar-conv-no-stack.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10069" ] || [ "$CI_BRANCH" = "whd-for-evar-conv-no-stack" ]; then - - unicoq_CI_REF=whd-for-evar-conv-no-stack - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - -fi diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh deleted file mode 100644 index 2015935dd9..0000000000 --- a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then - - elpi_CI_REF=canonical-disable-hint - elpi_CI_GITURL=https://github.com/vbgl/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh b/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh deleted file mode 100644 index 4032b1c6b5..0000000000 --- a/dev/ci/user-overlays/10125-SkySkimmer-run_tactic_gen.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10125" ] || [ "$CI_BRANCH" = "run_tactic_gen" ]; then - - paramcoq_CI_REF=run_tactic_gen - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - -fi diff --git a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh b/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh deleted file mode 100644 index 3658e96a3a..0000000000 --- a/dev/ci/user-overlays/10133-SkySkimmer-kelim.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10133" ] || [ "$CI_BRANCH" = "kelim" ]; then - - equations_CI_REF=kelim - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh b/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh deleted file mode 100644 index bc8aa33565..0000000000 --- a/dev/ci/user-overlays/10135-maximedenes-detype-anonymous.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10135" ] || [ "$CI_BRANCH" = "detype-anonymous" ]; then - - unicoq_CI_REF=detype-anonymous - unicoq_CI_GITURL=https://github.com/maximedenes/unicoq - -fi diff --git a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh b/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh deleted file mode 100644 index fcbeb32a58..0000000000 --- a/dev/ci/user-overlays/10157-SkySkimmer-def-not-visible-generic-warning.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10188" ] || [ "$CI_BRANCH" = "def-not-visible-remove-warning" ]; then - - elpi_CI_REF=def-not-visible-generic-warning - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh b/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh deleted file mode 100644 index a89f6aca1b..0000000000 --- a/dev/ci/user-overlays/10177-SkySkimmer-generalize.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10177" ] || [ "$CI_BRANCH" = "generalize" ]; then - - quickchick_CI_REF=generalize - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick - -fi diff --git a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh deleted file mode 100644 index e3bbb84bcb..0000000000 --- a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10201" ] || [ "$CI_BRANCH" = "opaque-future-cleanup" ]; then - - coq_dpdgraph_CI_REF=opaque-future-cleanup - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - - coqhammer_CI_REF=opaque-future-cleanup - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - - elpi_CI_REF=opaque-future-cleanup - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - paramcoq_CI_REF=opaque-future-cleanup - paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq - -fi diff --git a/dev/ci/user-overlays/10215-gares-less-ontop.sh b/dev/ci/user-overlays/10215-gares-less-ontop.sh deleted file mode 100644 index bceb5ad0e8..0000000000 --- a/dev/ci/user-overlays/10215-gares-less-ontop.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10215" ] || [ "$CI_BRANCH" = "custom-typing" ]; then - - equations_CI_REF=pass-less-ontop - equations_CI_GITURL=https://github.com/gares/Coq-Equations - - mtac2_CI_REF=pass-less-ontop - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - paramcoq_CI_REF=pass-less-ontop - paramcoq_CI_GITURL=https://github.com/gares/paramcoq - - quickchick_CI_REF=pass-less-ontop - quickchick_CI_GITURL=https://github.com/gares/QuickChick - -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 new file mode 100644 index 0000000000..2c3f490c03 --- /dev/null +++ b/dev/ci/user-overlays/10334-ppedrot-rm-kernel-sideeff-role.sh @@ -0,0 +1,6 @@ +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/README.md b/dev/ci/user-overlays/README.md index 7fb73e447d..4c2f264a74 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -21,14 +21,14 @@ The name of your overlay file should start with a five-digit pull request number, followed by a dash, anything (for instance your GitHub nickname and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). -Example: `00669-maximedenes-ssr-merge.sh` containing +Example: `10185-SkySkimmer-instance-no-bang.sh` containing ``` -#!/bin/sh +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 -if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then - mathcomp_CI_REF=ssr-merge - mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp fi ``` diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 339ac2d9b7..51d90df89f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -5,6 +5,21 @@ - Functions and types deprecated in 8.10 have been removed in Coq 8.11. +- Type Decl_kinds.locality has been restructured, see commit + message. Main change to do generally is to change the flag "Global" + to "Global ImportDefaultBehavior". + +Proof state: + + Proofs that are attached to a top-level constant (such as lemmas) + are represented by `Lemmas.t`, as they do contain additional + information related to the constant declaration. + + Plugins that require access to the information about currently + opened lemmas can add one of the `![proof]` attributes to their + `mlg` entry, which will refine the type accordingly. See + documentation in `vernacentries` for more information. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing @@ -59,6 +74,19 @@ Coqlib: command then enables to locate the registered constant through its name. The name resolution is dynamic. +Proof state: + +- Handling of proof state has been fully functionalized, thus it is + not possible to call global functions such as `get_current_context ()`. + + The main type for functions that need to handle proof state is + `Proof_global.t`. + + Unfortunately, this change was not possible to do in a + backwards-compatible way, but in most case the api changes are + straightforward, with functions taking and returning an extra + argument. + Macros: - The RAW_TYPED AS and GLOB_TYPED AS stanzas of the ARGUMENT EXTEND macro are diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh index 96c92e3162..539bb5f1f9 100755 --- a/dev/lint-commits.sh +++ b/dev/lint-commits.sh @@ -19,21 +19,40 @@ fi BASE_COMMIT="$1" HEAD_COMMIT="$2" -bad=() +bad_ws=() +bad_compile=() while IFS= read -r commit; do echo Checking "$commit" # git diff --check # uses .gitattributes to know what to check if ! git diff --check "${commit}^" "$commit"; - then - bad+=("$commit") + then bad_ws+=("$commit") + fi + + if ! make -f Makefile.dune check + then bad_compile+=("$commit") fi done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --) -if [ "${#bad[@]}" != 0 ] +# report errors + +CODE=0 + +if [ "${#bad_ws[@]}" != 0 ] then >&2 echo "Whitespace errors!" - >&2 echo "In commits ${bad[*]}" + >&2 echo "In commits ${bad_ws[*]}" >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces." - exit 1 + >&2 echo + CODE=1 fi + +if [ "${#bad_compile[@]}" != 0 ] +then + >&2 echo "Compilation errors!" + >&2 echo "In commits ${bad_compile[*]}" + >&2 echo + CODE=1 +fi + +exit $CODE diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index b89ae67a82..5f9f326750 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -78,11 +78,7 @@ Specifically `camldebug-command-name' and `ocamldebug-command-name'." Note that this function is executed before _Coqproject is read if it exists." (let ((dir (coqdev-default-directory))) (when dir - (unless coq-prog-args - (setq coq-prog-args - `("-coqlib" ,dir - "-topfile" ,buffer-file-name))) - (setq-local coq-prog-name (concat dir "bin/coqtop"))))) + (setq-local coq-prog-name (concat dir "_build/default/dev/shim/coqtop-prelude"))))) (add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) (defvar coqdev-ocamldebug-command "dune exec dev/dune-dbg" |