diff options
Diffstat (limited to 'dev')
37 files changed, 120 insertions, 311 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index 4275e3d121..25545cf565 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -11,18 +11,6 @@ bench: - timing variables: GIT_DEPTH: "" - coq_pr_number: "" - coq_pr_comment_id: "" - new_ocaml_switch: "ocaml-base-compiler.4.07.1" - old_ocaml_switch: "ocaml-base-compiler.4.07.1" - new_coq_repository: "https://gitlab.com/coq/coq.git" - old_coq_repository: "https://gitlab.com/coq/coq.git" - new_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" - old_coq_opam_archive_git_uri: "https://github.com/coq/opam-coq-archive.git" - new_coq_opam_archive_git_branch: "master" - old_coq_opam_archive_git_branch: "master" - num_of_iterations: 1 - coq_opam_packages: "coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast" artifacts: name: "$CI_JOB_NAME" paths: diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 7625e4e7f7..d2e150be9a 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -40,18 +40,19 @@ echo $PWD #check_variable "JOB_NAME" #check_variable "JENKINS_URL" check_variable "CI_JOB_URL" -check_variable "coq_pr_number" -check_variable "coq_pr_comment_id" -check_variable "new_ocaml_switch" -check_variable "new_coq_repository" -check_variable "new_coq_opam_archive_git_uri" -check_variable "new_coq_opam_archive_git_branch" -check_variable "old_ocaml_switch" -check_variable "old_coq_repository" -check_variable "old_coq_opam_archive_git_uri" -check_variable "old_coq_opam_archive_git_branch" -check_variable "num_of_iterations" -check_variable "coq_opam_packages" + +: "${coq_pr_number:=}" +: "${coq_pr_comment_id:=}" +: "${new_ocaml_switch:=ocaml-base-compiler.4.07.1}" +: "${old_ocaml_switch:=ocaml-base-compiler.4.07.1}" +: "${new_coq_repository:=https://gitlab.com/coq/coq.git}" +: "${old_coq_repository:=https://gitlab.com/coq/coq.git}" +: "${new_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}" +: "${old_coq_opam_archive_git_uri:=https://github.com/coq/opam-coq-archive.git}" +: "${new_coq_opam_archive_git_branch:=master}" +: "${old_coq_opam_archive_git_branch:=master}" +: "${num_of_iterations:=1}" +: "${coq_opam_packages:=coq-performance-tests-lite coq-engine-bench-lite coq-hott coq-bignums coq-mathcomp-ssreflect coq-mathcomp-fingroup coq-mathcomp-algebra coq-mathcomp-solvable coq-mathcomp-field coq-mathcomp-character coq-mathcomp-odd-order coq-math-classes coq-corn coq-flocq coq-compcert coq-geocoq coq-color coq-coqprime coq-coqutil coq-bedrock2 coq-rewriter coq-fiat-core coq-fiat-parsers coq-fiat-crypto coq-unimath coq-sf-plf coq-coquelicot coq-lambda-rust coq-verdi coq-verdi-raft coq-fourcolor coq-rewriter-perf-SuperFast}" new_coq_commit=$(git rev-parse HEAD^2) old_coq_commit=$(git merge-base HEAD^1 $new_coq_commit) @@ -428,6 +429,9 @@ for coq_opam_package in $sorted_coq_opam_packages; do new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do + if [ -e $old_opam_root/$old_base_path/$vo ]; then + echo "$coq_opam_package/$vo $(stat -c%s $old_opam_root/$old_base_path/$vo) $(stat -c%s $new_opam_root/$new_base_path/$vo)" >> "$log_dir/vosize.log" + fi if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \ -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/ diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index fcc585117b..fc8921e63d 100755 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -1204,7 +1204,7 @@ function make_elpi { make_dune make_re - if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz 1 elpi; then + if build_prep https://github.com/LPCIC/elpi/archive v1.11.4 tar.gz 1 elpi; then log2 dune build -p elpi log2 dune install elpi diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index f9187d53a6..b85261d7fc 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -44,6 +44,18 @@ CI_BUILD_DIR="$PWD/_build_ci" ls -l "$CI_BUILD_DIR" || true +declare -A overlays + +overlay() +{ + local project=$1 + local ov_url=$2 + local ov_ref=$3 + + overlays[${project}_URL]=$ov_url + overlays[${project}_REF]=$ov_ref +} + set +x for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null @@ -62,32 +74,44 @@ set -x # (local build), it uses git clone to perform the download. git_download() { - local PROJECT=$1 - local DEST="$CI_BUILD_DIR/$PROJECT" - local GITURL_VAR="${PROJECT}_CI_GITURL" - local GITURL="${!GITURL_VAR}" - local REF_VAR="${PROJECT}_CI_REF" - local REF="${!REF_VAR}" - - if [ -d "$DEST" ]; then - echo "Warning: download and unpacking of $PROJECT skipped because $DEST already exists." - elif [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then - git clone "$GITURL" "$DEST" - cd "$DEST" - git checkout "$REF" + local project=$1 + local dest="$CI_BUILD_DIR/$project" + + local giturl_var="${project}_CI_GITURL" + local giturl="${!giturl_var}" + local ref_var="${project}_CI_REF" + local ref="${!ref_var}" + + local ov_url=${overlays[${project}_URL]} + local ov_ref=${overlays[${project}_REF]} + + if [ -d "$dest" ]; then + echo "Warning: download and unpacking of $project skipped because $dest already exists." + elif [[ $ov_url ]] || [ "$FORCE_GIT" = "1" ] || [ "$CI" = "" ]; then + git clone "$giturl" "$dest" + cd "$dest" + git checkout "$ref" + git log -n 1 + if [[ $ov_url ]]; then + git -c pull.rebase=false -c user.email=nobody@example.invalid -c user.name=Nobody \ + pull --no-ff "$ov_url" "$ov_ref" + git log -n 1 HEAD^2 + git log -n 1 + fi else # When possible, we download tarballs to reduce bandwidth and latency - local ARCHIVEURL_VAR="${PROJECT}_CI_ARCHIVEURL" - local ARCHIVEURL="${!ARCHIVEURL_VAR}" - mkdir -p "$DEST" - cd "$DEST" - local COMMIT=$(git ls-remote "$GITURL" "refs/heads/$REF" | cut -f 1) - if [[ "$COMMIT" == "" ]]; then - # $REF must have been a tag or hash, not a branch - COMMIT="$REF" + local archiveurl_var="${project}_CI_ARCHIVEURL" + local archiveurl="${!archiveurl_var}" + mkdir -p "$dest" + cd "$dest" + local commit + commit=$(git ls-remote "$giturl" "refs/heads/$ref" | cut -f 1) + if [[ "$commit" == "" ]]; then + # $ref must have been a tag or hash, not a branch + commit="$ref" fi - wget "$ARCHIVEURL/$COMMIT.tar.gz" - tar xfz "$COMMIT.tar.gz" --strip-components=1 - rm -f "$COMMIT.tar.gz" + wget "$archiveurl/$commit.tar.gz" + tar xfz "$commit.tar.gz" --strip-components=1 + rm -f "$commit.tar.gz" fi } diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh index 0256906112..9616f3ce00 100755 --- a/dev/ci/ci-iris.sh +++ b/dev/ci/ci-iris.sh @@ -9,13 +9,13 @@ git_download iris_string_ident git_download iris_examples # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris git_download iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f672ead807..c17ec502e7 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2020-09-17-V88" +# CACHEKEY: "bionic_coq-V2020-10-12-V89" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -43,7 +43,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages ENV BASE_OPAM="zarith.1.10 ocamlfind.1.8.1 ounit2.2.2.3 odoc.1.5.1" \ CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \ - BASE_ONLY_OPAM="elpi.1.11.0" + BASE_ONLY_OPAM="elpi.1.11.4" # BASE switch; CI_OPAM contains Coq's CI dependencies. ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0" diff --git a/dev/ci/user-overlays/08743-ejgallego-zarith.sh b/dev/ci/user-overlays/08743-ejgallego-zarith.sh deleted file mode 100644 index da1d30c1e9..0000000000 --- a/dev/ci/user-overlays/08743-ejgallego-zarith.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11742" ] || [ "$CI_BRANCH" = "zarith+core" ]; then - - bignums_CI_REF=zarith - bignums_CI_GITURL=https://github.com/ejgallego/bignums - -fi diff --git a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh deleted file mode 100644 index 80107ac9c5..0000000000 --- a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh +++ /dev/null @@ -1,30 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "10390" ] || [ "$CI_BRANCH" = "uip" ]; then - - unicoq_CI_REF=uip - unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq - - mtac2_CI_REF=uip - mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2 - - elpi_CI_REF=uip - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=uip - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - - paramcoq_CI_REF=uip - paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq - - relation_algebra_CI_REF=uip - relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra - - coq_dpdgraph_CI_REF=uip - coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph - - coqhammer_CI_REF=uip - coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer - - metacoq_CI_REF=uip - metacoq_CI_GITURL=https://github.com/SkySkimmer/metacoq - -fi diff --git a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh b/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh deleted file mode 100644 index 05192facbe..0000000000 --- a/dev/ci/user-overlays/11566-ejgallego-exninfo+coercion.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11566" ] || [ "$CI_BRANCH" = "exninfo+coercion" ]; then - - mtac2_CI_REF=exninfo+coercion - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/11604-persistent-arrays.sh b/dev/ci/user-overlays/11604-persistent-arrays.sh deleted file mode 100644 index aec5c4fa3d..0000000000 --- a/dev/ci/user-overlays/11604-persistent-arrays.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11604" ] || [ "$CI_BRANCH" = "persistent-arrays" ]; then - - unicoq_CI_REF=persistent-arrays - unicoq_CI_GITURL=https://github.com/maximedenes/unicoq - - elpi_CI_REF=persistent-arrays - elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi - - #relation_algebra_CI_REF=persistent-arrays - #relation_algebra_CI_GITURL=https://github.com/maximedenes/relation-algebra - - coqhammer_CI_REF=persistent-arrays - coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer - - metacoq_CI_REF=persistent-arrays - metacoq_CI_GITURL=https://github.com/maximedenes/metacoq - -fi diff --git a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh b/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh deleted file mode 100644 index 72ec55a37c..0000000000 --- a/dev/ci/user-overlays/11836-ejgallego-obligations+functional.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11836" ] || [ "$CI_BRANCH" = "obligations+functional" ]; then - - mtac2_CI_REF=obligations+functional - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - paramcoq_CI_REF=obligations+functional - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - equations_CI_REF=obligations+functional - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - metacoq_CI_REF=obligations+functional - metacoq_CI_GITURL=https://github.com/ejgallego/metacoq - - rewriter_CI_REF=obligations+functional - rewriter_CI_GITURL=https://github.com/ejgallego/rewriter - -fi diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh deleted file mode 100644 index c9ddb3fb9f..0000000000 --- a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then - - equations_CI_REF="rm-local-reductionops" - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - unicoq_CI_REF="rm-local-reductionops" - unicoq_CI_GITURL=https://github.com/ppedrot/unicoq - -fi diff --git a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh b/dev/ci/user-overlays/11948-proux01-hexadecimal.sh deleted file mode 100644 index 0b3133d1f1..0000000000 --- a/dev/ci/user-overlays/11948-proux01-hexadecimal.sh +++ /dev/null @@ -1,12 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "11948" ] || [ "$CI_BRANCH" = "hexadecimal" ]; then - - stdlib2_CI_REF=hexadecimal - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - - paramcoq_CI_REF=hexadecimal - paramcoq_CI_GITURL=https://github.com/proux01/paramcoq - - metacoq_CI_REF=hexadecimal - metacoq_CI_GITURL=https://github.com/proux01/metacoq - -fi diff --git a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh deleted file mode 100644 index ceb7afe3d1..0000000000 --- a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12267" ] || [ "$CI_BRANCH" = "elpi-1.11" ]; then - - elpi_CI_REF="coq-master+elpi-1.11" - elpi_hb_CI_REF="coq-master+elpi.11" - -fi diff --git a/dev/ci/user-overlays/12372-ejgallego-proof+info.sh b/dev/ci/user-overlays/12372-ejgallego-proof+info.sh deleted file mode 100644 index b9fdc338b5..0000000000 --- a/dev/ci/user-overlays/12372-ejgallego-proof+info.sh +++ /dev/null @@ -1,24 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12372" ] || [ "$CI_BRANCH" = "proof+info" ]; then - - rewriter_CI_REF=proof+info - rewriter_CI_GITURL=https://github.com/ejgallego/rewriter - - paramcoq_CI_REF=proof+info - paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq - - mtac2_CI_REF=proof+info - mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - - equations_CI_REF=proof+info - equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations - - elpi_CI_REF=proof+info - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - - aac_tactics_CI_REF=proof+info - aac_tactics_CI_GITURL=https://github.com/ejgallego/aac-tactics - - metacoq_CI_REF=proof+info - metacoq_CI_GITURL=https://github.com/ejgallego/metacoq - -fi diff --git a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh new file mode 100644 index 0000000000..fb5947d218 --- /dev/null +++ b/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12449" ] || [ "$CI_BRANCH" = "minim-prop-toset" ]; then + + mtac2_CI_REF=janno/coq-12449 + mtac2_CI_GITURL=https://github.com/mtac2/mtac2 + +fi diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh deleted file mode 100644 index ced0d95945..0000000000 --- a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then - - fiat_parsers_CI_REF="factor-hint-flags" - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -fi diff --git a/dev/ci/user-overlays/12523-term-notation-custom.sh b/dev/ci/user-overlays/12523-term-notation-custom.sh deleted file mode 100644 index 6217312a2a..0000000000 --- a/dev/ci/user-overlays/12523-term-notation-custom.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12523" ] || [ "$CI_BRANCH" = "fix-11121" ]; then - - equations_CI_REF=fix-11121 - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh b/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh deleted file mode 100644 index 7c04608403..0000000000 --- a/dev/ci/user-overlays/12565-ppedrot-fix-tc-search-opacity.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12565" ] || [ "$CI_BRANCH" = "fix-tc-search-opacity" ]; then - - coqhammer_CI_REF=fix-tc-search-opacity - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - -fi diff --git a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh b/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh deleted file mode 100644 index c8c5b3ed5a..0000000000 --- a/dev/ci/user-overlays/12599-ppedrot-rm-deprecated-refiner.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12599" ] || [ "$CI_BRANCH" = "rm-deprecated-refiner" ]; then - - equations_CI_REF=rm-deprecated-refiner - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh b/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh deleted file mode 100644 index d4c67b03b5..0000000000 --- a/dev/ci/user-overlays/12650-SkySkimmer-rebuild-record.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12650" ] || [ "$CI_BRANCH" = "rebuild-record" ]; then - - elpi_CI_REF=rebuild-record - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - -fi diff --git a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh b/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh deleted file mode 100644 index 56a69abbf7..0000000000 --- a/dev/ci/user-overlays/12709-ppedrot-hint-pattern-out.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12709" ] || [ "$CI_BRANCH" = "hint-pattern-out" ]; then - - coqhammer_CI_REF=hint-pattern-out - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - -fi diff --git a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh b/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh deleted file mode 100644 index e57f95ef19..0000000000 --- a/dev/ci/user-overlays/12720-ppedrot-factor-class-hint-clenv.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12720" ] || [ "$CI_BRANCH" = "factor-class-hint-clenv" ]; then - - coqhammer_CI_REF=factor-class-hint-clenv - coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer - -fi diff --git a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh b/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh deleted file mode 100644 index 54fdd87566..0000000000 --- a/dev/ci/user-overlays/12756-jashug-dont-refresh-argument-names.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12756" ] || [ "$CI_BRANCH" = "dont-refresh-argument-names" ]; then - - mathcomp_CI_REF=dont-refresh-argument-names-overlay - mathcomp_CI_GITURL=https://github.com/jashug/math-comp - - oddorder_CI_REF=dont-refresh-argument-names-overlay - oddorder_CI_GITURL=https://github.com/jashug/odd-order - -fi diff --git a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh b/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh deleted file mode 100644 index 6a9cf78687..0000000000 --- a/dev/ci/user-overlays/12801-VincentSe-CyclicSet.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12801" ] || [ "$CI_BRANCH" = "CyclicSet" ]; then - - bignums_CI_REF=CyclicSet - bignums_CI_GITURL=https://github.com/VincentSe/bignums - - coqprime_CI_REF=CyclicSet - coqprime_CI_GITURL=https://github.com/VincentSe/coqprime -fi diff --git a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh b/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh deleted file mode 100644 index bb08c13ef3..0000000000 --- a/dev/ci/user-overlays/12875-herbelin-master+about-print-all-arguments-names.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12875" ] || [ "$CI_BRANCH" = "master+about-print-all-arguments-names" ]; then - - elpi_CI_REF=coq-master+adapt-coq12875-arguments-pass-name-impargs - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh b/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh deleted file mode 100644 index f0878202d3..0000000000 --- a/dev/ci/user-overlays/12892-SkySkimmer-update-s-univs.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12892" ] || [ "$CI_BRANCH" = "update-s-univs" ]; then - - elpi_CI_REF=update-s-univs - elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi - - equations_CI_REF=update-s-univs - equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh b/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh deleted file mode 100644 index ee75944a52..0000000000 --- a/dev/ci/user-overlays/12968-maximedenes-delay-frozen-evarconv.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12968" ] || [ "$CI_BRANCH" = "delay-frozen-evarconv" ]; then - - equations_CI_REF=delay-frozen-evarconv - equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh b/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh deleted file mode 100644 index 7bed43afe1..0000000000 --- a/dev/ci/user-overlays/12977-ppedrot-static-hint-poly.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12977" ] || [ "$CI_BRANCH" = "static-hint-poly" ]; then - - equations_CI_REF=static-hint-poly - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - fiat_parsers_CI_REF=static-hint-poly - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -fi diff --git a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh b/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh deleted file mode 100644 index 3407c2db39..0000000000 --- a/dev/ci/user-overlays/13028-herbelin-master+fix-quotations-printing.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13028" ] || [ "$CI_BRANCH" = "master+fix-quotations-printing" ]; then - - equations_CI_REF=master+adapt-coq-pr13028-quotation-qualifier-printing - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh new file mode 100644 index 0000000000..f16cf1497e --- /dev/null +++ b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh @@ -0,0 +1,5 @@ +if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then + + overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance + +fi diff --git a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh new file mode 100644 index 0000000000..7d55cf6883 --- /dev/null +++ b/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "13166" ] || [ "$CI_BRANCH" = "master+fixes13165-missing-impargs-defined-fields" ]; then + + elpi_CI_REF=coq-master+adapt-coq-pr13166-impargs-record-fields + elpi_CI_GITURL=https://github.com/herbelin/coq-elpi + +fi diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh deleted file mode 100644 index 50eaf0b109..0000000000 --- a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then - - elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh b/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh deleted file mode 100644 index 3b3b20baf1..0000000000 --- a/dev/ci/user-overlays/8855-herbelin-master+more-search-options.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "8855" ] || [ "$CI_BRANCH" = "master+more-search-options" ]; then - - coqhammer_CI_REF=master+adapt-pr8855-search-api - coqhammer_CI_GITURL=https://github.com/herbelin/coqhammer - - coq_dpdgraph_CI_REF=coq-master+adapt-pr8855-search-api - coq_dpdgraph_CI_GITURL=https://github.com/herbelin/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 4c2f264a74..3f9ad5e878 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -4,15 +4,12 @@ When your pull request breaks an external project we test in our CI and you have prepared a branch with the fix, you can add an "overlay" to your pull request to test it with the adapted version of the external project. -An overlay is a file which defines where to look for the patched version so that -testing is possible. It redefines some variables from -[`ci-basic-overlay.sh`](../ci-basic-overlay.sh): -give the name of your branch / commit using a `_CI_REF` variable and the -location of your fork using a `_CI_GITURL` variable. -The `_CI_GITURL` variable should be the URL of the repository without a -trailing `.git`. -If the fork is not on the same platform (e.g. GitHub instead of GitLab), it is -necessary to redefine the `_CI_ARCHIVEURL` variable as well. +An overlay is a file which defines where to look for the patched +version so that testing is possible. This is done by calling the +`overlay` command for each project with the project name (as used in +the variables in [`ci-basic-overlay.sh`](../ci-basic-overlay.sh)), the +location of your fork and the branch containing the patch on your +fork. Moreover, the file contains very simple logic to test the pull request number or branch name and apply it only in this case. @@ -21,13 +18,12 @@ 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: `10185-SkySkimmer-instance-no-bang.sh` containing +Example: `13128-SkySkimmer-noinstance.sh` containing ``` -if [ "$CI_PULL_REQUEST" = "10185" ] || [ "$CI_BRANCH" = "instance-no-bang" ]; then +if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - quickchick_CI_REF=instance-no-bang - quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick + overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance fi ``` diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 59c1623a2d..6a6318f97a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,15 +1,35 @@ ## Changes between Coq 8.12 and Coq 8.13 -- Tactic language: TacGeneric now takes an argument to tell if it - comes from a notation. Use `None` if not and `Some foo` to tell to - print such TacGeneric surrounded with `foo:( )`. - ### Code formatting - The automatic code formatting tool `ocamlformat` has been disabled and its git hook removed. If desired, automatic formatting can be achieved by calling the `fmt` target of the dune build system. +### ML API + +Abstract syntax of tactic: + +- TacGeneric now takes an argument to tell if it comes from a + notation. Use `None` if not and `Some foo` to tell to print such + TacGeneric surrounded with `foo:( )`. + +Printing functions: + +- `Pp.h` does not take a `int` argument anymore (the argument was + not used). In general, where `h n` for `n` non zero was used, `hv n` + was instead intended. If cancelling the breaking role of cuts in the + box was intended, turn `h n c` into `h c`. + +Grammar entries: + +- `Prim.pattern_identref` is deprecated, use `Prim.pattern_ident` + which now returns a located identifier. + +Generic arguments: + +- Generic arguments: `wit_var` is deprecated, use `wit_hyp`. + ## Changes between Coq 8.11 and Coq 8.12 ### Code formatting diff --git a/dev/tools/create_overlays.sh b/dev/tools/create_overlays.sh index ad60b1115f..78ed27ba03 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -66,8 +66,7 @@ do make ci-$_CONTRIB_NAME || true setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL - echo " ${_CONTRIB_NAME}_CI_REF=$OVERLAY_BRANCH" >> $OVERLAY_FILE - echo " ${_CONTRIB_NAME}_CI_GITURL=$_CONTRIB_GITURL" >> $OVERLAY_FILE + echo " overlay ${_CONTRIB_NAME} $_CONTRIB_GITURL $OVERLAY_BRANCH" >> $OVERLAY_FILE echo "" >> $OVERLAY_FILE shift done |