diff options
35 files changed, 380 insertions, 356 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 18fdd83218..be819616e2 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -1,54 +1,72 @@ #!/usr/bin/env bash -# This is the basic overlay set for repositories in the CI. - -# Maybe we should just use Ruby to have real objects... - -# : "${foo:=bar}" sets foo to "bar" if it is unset or null +# This is the list of repositories used by the CI scripts, unless overridden +# by a call to the "overlay" function in ci-common + +declare -a projects # the list of project repos that can be be overlayed + +# checks if the given argument is a known project +function is_in_projects { + local rc=1 + for x in ${!projects[@]}; do + if [ "$1" = "$x" ]; then rc=0; fi; + done + return rc +} + +# project <name> <giturl> <ref> [<archiveurl>] +# [<archiveurl>] defaults to <giturl>/archive on github.com +# and <giturl>/-/archive on gitlab +function project { + + local var_ref=${1}_CI_REF + local var_giturl=${1}_CI_GITURL + local var_archiveurl=${1}_CI_ARCHIVEURL + local giturl=$2 + local ref=$3 + local archiveurl=$4 + case $giturl in + *github.com*) archiveurl=${archiveurl:-$giturl/archive} ;; + *gitlab*) archiveurl=${archiveurl:-$giturl/-/archive} ;; + esac + + # register the project in the list of projects + projects[${#projects[*]}]=$1 + + # bash idiom for setting a variable if not already set + : "${!var_ref:=$ref}" + : "${!var_giturl:=$giturl}" + : "${!var_archiveurl:=$archiveurl}" + +} ######################################################################## # MathComp ######################################################################## -: "${mathcomp_CI_REF:=master}" -: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp}" -: "${mathcomp_CI_ARCHIVEURL:=${mathcomp_CI_GITURL}/archive}" +project mathcomp "https://github.com/math-comp/math-comp" "master" -: "${fourcolor_CI_REF:=master}" -: "${fourcolor_CI_GITURL:=https://github.com/math-comp/fourcolor}" -: "${fourcolor_CI_ARCHIVEURL:=${fourcolor_CI_GITURL}/archive}" +project fourcolor "https://github.com/math-comp/fourcolor" "master" -: "${oddorder_CI_REF:=master}" -: "${oddorder_CI_GITURL:=https://github.com/math-comp/odd-order}" -: "${oddorder_CI_ARCHIVEURL:=${oddorder_CI_GITURL}/archive}" +project oddorder "https://github.com/math-comp/odd-order" "master" ######################################################################## # UniMath ######################################################################## -: "${unimath_CI_REF:=master}" -: "${unimath_CI_GITURL:=https://github.com/UniMath/UniMath}" -: "${unimath_CI_ARCHIVEURL:=${unimath_CI_GITURL}/archive}" +project unimath "https://github.com/UniMath/UniMath" "master" ######################################################################## # Unicoq + Mtac2 ######################################################################## -: "${unicoq_CI_REF:=master}" -: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq}" -: "${unicoq_CI_ARCHIVEURL:=${unicoq_CI_GITURL}/archive}" +project unicoq "https://github.com/unicoq/unicoq" "master" -: "${mtac2_CI_REF:=master}" -: "${mtac2_CI_GITURL:=https://github.com/Mtac2/Mtac2}" -: "${mtac2_CI_ARCHIVEURL:=${mtac2_CI_GITURL}/archive}" +project mtac2 "https://github.com/Mtac2/Mtac2" "master" ######################################################################## # Mathclasses + Corn ######################################################################## -: "${math_classes_CI_REF:=master}" -: "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}" -: "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}" +project math_classes "https://github.com/coq-community/math-classes" "master" -: "${corn_CI_REF:=master}" -: "${corn_CI_GITURL:=https://github.com/coq-community/corn}" -: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}" +project corn "https://github.com/coq-community/corn" "master" ######################################################################## # Iris @@ -56,342 +74,238 @@ # NB: stdpp and Iris refs are gotten from the opam files in the Iris # and lambdaRust repos respectively. -: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}" -: "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}" +project stdpp "https://gitlab.mpi-sws.org/iris/stdpp" "" -: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}" -: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}" +project iris "https://gitlab.mpi-sws.org/iris/iris" "" -: "${autosubst_CI_REF:=coq86-devel}" -: "${autosubst_CI_GITURL:=https://github.com/RalfJung/autosubst}" -: "${autosubst_CI_ARCHIVEURL:=${autosubst_CI_GITURL}/archive}" +project autosubst "https://github.com/coq-community/autosubst" "master" -: "${iris_string_ident_CI_REF:=master}" -: "${iris_string_ident_CI_GITURL:=https://gitlab.mpi-sws.org/iris/string-ident}" -: "${iris_string_ident_CI_ARCHIVEURL:=${iris_string_ident_CI_GITURL}/-/archive}" +project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master" -: "${iris_examples_CI_REF:=master}" -: "${iris_examples_CI_GITURL:=https://gitlab.mpi-sws.org/iris/examples}" -: "${iris_examples_CI_ARCHIVEURL:=${iris_examples_CI_GITURL}/-/archive}" +project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master" ######################################################################## # HoTT ######################################################################## -: "${hott_CI_REF:=master}" -: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}" -: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}" +project hott "https://github.com/HoTT/HoTT" "master" ######################################################################## # CoqHammer ######################################################################## -: "${coqhammer_CI_REF:=master}" -: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}" -: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" +project coqhammer "https://github.com/lukaszcz/coqhammer" "master" ######################################################################## # GeoCoq ######################################################################## -: "${geocoq_CI_REF:=master}" -: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}" -: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}" +project geocoq "https://github.com/GeoCoq/GeoCoq" "master" ######################################################################## # Flocq ######################################################################## -: "${flocq_CI_REF:=master}" -: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}" -: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}" +project flocq "https://gitlab.inria.fr/flocq/flocq" "master" ######################################################################## # coq-performance-tests ######################################################################## -: "${coq_performance_tests_CI_REF:=master}" -: "${coq_performance_tests_CI_GITURL:=https://github.com/coq-community/coq-performance-tests}" -: "${coq_performance_tests_CI_ARCHIVEURL:=${coq_performance_tests_CI_GITURL}/archive}" +project coq_performance_tests "https://github.com/coq-community/coq-performance-tests" "master" ######################################################################## # coq-tools ######################################################################## -: "${coq_tools_CI_REF:=master}" -: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}" -: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}" +project coq_tools "https://github.com/JasonGross/coq-tools" "master" ######################################################################## # Coquelicot ######################################################################## -: "${coquelicot_CI_REF:=master}" -: "${coquelicot_CI_GITURL:=https://gitlab.inria.fr/coquelicot/coquelicot}" -: "${coquelicot_CI_ARCHIVEURL:=${coquelicot_CI_GITURL}/-/archive}" +project coquelicot "https://gitlab.inria.fr/coquelicot/coquelicot" "master" ######################################################################## # Coq-interval ######################################################################## -: "${interval_CI_REF:=master}" -: "${interval_CI_GITURL:=https://gitlab.inria.fr/coqinterval/interval}" -: "${interval_CI_ARCHIVEURL:=${interval_CI_GITURL}/-/archive}" +project interval "https://gitlab.inria.fr/coqinterval/interval" "master" ######################################################################## # Gappa stand alone tool ######################################################################## -: "${gappa_tool_CI_REF:=master}" -: "${gappa_tool_CI_GITURL:=https://gitlab.inria.fr/gappa/gappa}" -: "${gappa_tool_CI_ARCHIVEURL:=${gappa_tool_CI_GITURL}/-/archive}" +project gappa_tool "https://gitlab.inria.fr/gappa/gappa" "master" ######################################################################## # Gappa plugin ######################################################################## -: "${gappa_plugin_CI_REF:=master}" -: "${gappa_plugin_CI_GITURL:=https://gitlab.inria.fr/gappa/coq}" -: "${gappa_plugin_CI_ARCHIVEURL:=${gappa_plugin_CI_GITURL}/-/archive}" +project gappa_plugin "https://gitlab.inria.fr/gappa/coq" "master" ######################################################################## # CompCert ######################################################################## -: "${compcert_CI_REF:=master}" -: "${compcert_CI_GITURL:=https://github.com/AbsInt/CompCert}" -: "${compcert_CI_ARCHIVEURL:=${compcert_CI_GITURL}/archive}" +project compcert "https://github.com/AbsInt/CompCert" "master" ######################################################################## # VST ######################################################################## -: "${vst_CI_REF:=master}" -: "${vst_CI_GITURL:=https://github.com/PrincetonUniversity/VST}" -: "${vst_CI_ARCHIVEURL:=${vst_CI_GITURL}/archive}" +project vst "https://github.com/PrincetonUniversity/VST" "master" ######################################################################## # cross-crypto ######################################################################## -: "${cross_crypto_CI_REF:=master}" -: "${cross_crypto_CI_GITURL:=https://github.com/mit-plv/cross-crypto}" -: "${cross_crypto_CI_ARCHIVEURL:=${cross_crypto_CI_GITURL}/archive}" +project cross_crypto "https://github.com/mit-plv/cross-crypto" "master" ######################################################################## # rewriter ######################################################################## -: "${rewriter_CI_REF:=master}" -: "${rewriter_CI_GITURL:=https://github.com/mit-plv/rewriter}" -: "${rewriter_CI_ARCHIVEURL:=${rewriter_CI_GITURL}/archive}" +project rewriter "https://github.com/mit-plv/rewriter" "master" ######################################################################## # fiat_parsers ######################################################################## -: "${fiat_parsers_CI_REF:=master}" -: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat}" -: "${fiat_parsers_CI_ARCHIVEURL:=${fiat_parsers_CI_GITURL}/archive}" +project fiat_parsers "https://github.com/mit-plv/fiat" "master" ######################################################################## # fiat_crypto ######################################################################## -: "${fiat_crypto_CI_REF:=master}" -: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" +project fiat_crypto "https://github.com/mit-plv/fiat-crypto" "master" ######################################################################## # fiat_crypto_legacy ######################################################################## -: "${fiat_crypto_legacy_CI_REF:=sp2019latest}" -: "${fiat_crypto_legacy_CI_GITURL:=https://github.com/mit-plv/fiat-crypto}" -: "${fiat_crypto_legacy_CI_ARCHIVEURL:=${fiat_crypto_legacy_CI_GITURL}/archive}" +project fiat_crypto_legacy "https://github.com/mit-plv/fiat-crypto" "sp2019latest" ######################################################################## # coq_dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_REF:=coq-master}" -: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph}" -: "${coq_dpdgraph_CI_ARCHIVEURL:=${coq_dpdgraph_CI_GITURL}/archive}" +project coq_dpdgraph "https://github.com/Karmaki/coq-dpdgraph" "coq-master" ######################################################################## # CoLoR ######################################################################## -: "${color_CI_REF:=master}" -: "${color_CI_GITURL:=https://github.com/fblanqui/color}" -: "${color_CI_ARCHIVEURL:=${color_CI_GITURL}/archive}" +project color "https://github.com/fblanqui/color" "master" ######################################################################## # TLC ######################################################################## -: "${tlc_CI_REF:=master-for-coq-ci}" -: "${tlc_CI_GITURL:=https://github.com/charguer/tlc}" -: "${tlc_CI_ARCHIVEURL:=${tlc_CI_GITURL}/archive}" +project tlc "https://github.com/charguer/tlc" "master-for-coq-ci" ######################################################################## # Bignums ######################################################################## -: "${bignums_CI_REF:=master}" -: "${bignums_CI_GITURL:=https://github.com/coq/bignums}" -: "${bignums_CI_ARCHIVEURL:=${bignums_CI_GITURL}/archive}" +project bignums "https://github.com/coq/bignums" "master" ######################################################################## # coqprime ######################################################################## -: "${coqprime_CI_REF:=master}" -: "${coqprime_CI_GITURL:=https://github.com/thery/coqprime}" -: "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" +project coqprime "https://github.com/thery/coqprime" "master" ######################################################################## # bbv ######################################################################## -: "${bbv_CI_REF:=master}" -: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}" -: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}" +project bbv "https://github.com/mit-plv/bbv" "master" ######################################################################## # bedrock2 ######################################################################## -: "${bedrock2_CI_REF:=tested}" -: "${bedrock2_CI_GITURL:=https://github.com/mit-plv/bedrock2}" -: "${bedrock2_CI_ARCHIVEURL:=${bedrock2_CI_GITURL}/archive}" +project bedrock2 "https://github.com/mit-plv/bedrock2" "tested" ######################################################################## # Equations ######################################################################## -: "${equations_CI_REF:=master}" -: "${equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations}" -: "${equations_CI_ARCHIVEURL:=${equations_CI_GITURL}/archive}" +project equations "https://github.com/mattam82/Coq-Equations" "master" ######################################################################## # Elpi + Hierarchy Builder ######################################################################## -: "${elpi_CI_REF:=coq-master}" -: "${elpi_CI_GITURL:=https://github.com/LPCIC/coq-elpi}" -: "${elpi_CI_ARCHIVEURL:=${elpi_CI_GITURL}/archive}" +project elpi "https://github.com/LPCIC/coq-elpi" "coq-master" -: "${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}" +project elpi_hb "https://github.com/math-comp/hierarchy-builder" "coq-master" ######################################################################## # Engine-Bench ######################################################################## -: "${engine_bench_CI_REF:=master}" -: "${engine_bench_CI_GITURL:=https://github.com/mit-plv/engine-bench}" -: "${engine_bench_CI_ARCHIVEURL:=${engine_bench_CI_GITURL}/archive}" +project engine_bench "https://github.com/mit-plv/engine-bench" "master" ######################################################################## # fcsl-pcm ######################################################################## -: "${fcsl_pcm_CI_REF:=master}" -: "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}" -: "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" +project fcsl_pcm "https://github.com/imdea-software/fcsl-pcm" "master" ######################################################################## # ext-lib ######################################################################## -: "${ext_lib_CI_REF:=master}" -: "${ext_lib_CI_GITURL:=https://github.com/coq-community/coq-ext-lib}" -: "${ext_lib_CI_ARCHIVEURL:=${ext_lib_CI_GITURL}/archive}" +project ext_lib "https://github.com/coq-community/coq-ext-lib" "master" ######################################################################## # simple-io ######################################################################## -: "${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}" +project simple_io "https://github.com/Lysxia/coq-simple-io" "master" ######################################################################## # quickchick ######################################################################## -: "${quickchick_CI_REF:=master}" -: "${quickchick_CI_GITURL:=https://github.com/QuickChick/QuickChick}" -: "${quickchick_CI_ARCHIVEURL:=${quickchick_CI_GITURL}/archive}" +project quickchick "https://github.com/QuickChick/QuickChick" "master" ######################################################################## # reduction-effects ######################################################################## -: "${reduction_effects_CI_REF:=master}" -: "${reduction_effects_CI_GITURL:=https://github.com/coq-community/reduction-effects}" -: "${reduction_effects_CI_ARCHIVEURL:=${reduction_effects_CI_GITURL}/archive}" +project reduction_effects "https://github.com/coq-community/reduction-effects" "master" ######################################################################## # menhirlib ######################################################################## # Note: menhirlib is now in subfolder coq-menhirlib of menhir -: "${menhirlib_CI_REF:=20201122}" -: "${menhirlib_CI_GITURL:=https://gitlab.inria.fr/fpottier/menhir}" -: "${menhirlib_CI_ARCHIVEURL:=${menhirlib_CI_GITURL}/-/archive}" +project menhirlib "https://gitlab.inria.fr/fpottier/menhir" "20201122" ######################################################################## # aac_tactics ######################################################################## -: "${aac_tactics_CI_REF:=master}" -: "${aac_tactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" -: "${aac_tactics_CI_ARCHIVEURL:=${aac_tactics_CI_GITURL}/archive}" +project aac_tactics "https://github.com/coq-community/aac-tactics" "master" ######################################################################## # paramcoq ######################################################################## -: "${paramcoq_CI_REF:=master}" -: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" -: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" +project paramcoq "https://github.com/coq-community/paramcoq" "master" ######################################################################## # relation_algebra ######################################################################## -: "${relation_algebra_CI_REF:=master}" -: "${relation_algebra_CI_GITURL:=https://github.com/damien-pous/relation-algebra}" -: "${relation_algebra_CI_ARCHIVEURL:=${relation_algebra_CI_GITURL}/archive}" +project relation_algebra "https://github.com/damien-pous/relation-algebra" "master" ######################################################################## # StructTact + InfSeqExt + Cheerios + Verdi + Verdi Raft ######################################################################## -: "${struct_tact_CI_REF:=master}" -: "${struct_tact_CI_GITURL:=https://github.com/uwplse/StructTact}" -: "${struct_tact_CI_ARCHIVEURL:=${struct_tact_CI_GITURL}/archive}" +project struct_tact "https://github.com/uwplse/StructTact" "master" -: "${inf_seq_ext_CI_REF:=master}" -: "${inf_seq_ext_CI_GITURL:=https://github.com/DistributedComponents/InfSeqExt}" -: "${inf_seq_ext_CI_ARCHIVEURL:=${inf_seq_ext_CI_GITURL}/archive}" +project inf_seq_ext "https://github.com/DistributedComponents/InfSeqExt" "master" -: "${cheerios_CI_REF:=master}" -: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" -: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" +project cheerios "https://github.com/uwplse/cheerios" "master" -: "${verdi_CI_REF:=master}" -: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" -: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" +project verdi "https://github.com/uwplse/verdi" "master" -: "${verdi_raft_CI_REF:=master}" -: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" -: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" +project verdi_raft "https://github.com/uwplse/verdi-raft" "master" ######################################################################## # stdlib2 ######################################################################## -: "${stdlib2_CI_REF:=master}" -: "${stdlib2_CI_GITURL:=https://github.com/coq/stdlib2}" -: "${stdlib2_CI_ARCHIVEURL:=${stdlib2_CI_GITURL}/archive}" +project stdlib2 "https://github.com/coq/stdlib2" "master" ######################################################################## # argosy ######################################################################## -: "${argosy_CI_REF:=master}" -: "${argosy_CI_GITURL:=https://github.com/mit-pdos/argosy}" -: "${argosy_CI_ARCHIVEURL:=${argosy_CI_GITURL}/archive}" +project argosy "https://github.com/mit-pdos/argosy" "master" ######################################################################## # perennial ######################################################################## -: "${perennial_CI_REF:=coq/tested}" -: "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}" -: "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}" +project perennial "https://github.com/mit-pdos/perennial" "coq/tested" ######################################################################## # metacoq ######################################################################## -: "${metacoq_CI_REF:=master}" -: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}" -: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}" +project metacoq "https://github.com/MetaCoq/metacoq" "master" ######################################################################## # SF suite ######################################################################## -: "${sf_CI_REF:=master}" -: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}" -: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}" +project sf "https://github.com/DeepSpec/sf" "master" ######################################################################## # Coqtail ######################################################################## -: "${coqtail_CI_REF:=master}" -: "${coqtail_CI_GITURL:=https://github.com/whonore/Coqtail}" -: "${coqtail_CI_ARCHIVEURL:=${coqtail_CI_GITURL}/archive}" +project coqtail "https://github.com/whonore/Coqtail" "master" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 1a4ebc0e90..fdba690155 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -49,20 +49,34 @@ ls -l "$CI_BUILD_DIR" || true declare -A overlays -overlay() +# overlay <project> <giturl> <ref> <prnumber> [<prbranch>] +# creates an overlay for project using a given url and branch which is +# active for prnumber or prbranch. prbranch defaults to ref. +function overlay() { local project=$1 local ov_url=$2 local ov_ref=$3 - - overlays[${project}_URL]=$ov_url - overlays[${project}_REF]=$ov_ref + local ov_prnumber=$4 + local ov_prbranch=$5 + : "${ov_prbranch:=$ov_ref}" + + if [ "$CI_PULL_REQUEST" = "$ov_prnumber" ] || [ "$CI_BRANCH" = "$ov_prbranch" ]; then + if ! is_in_projects "$project"; then + echo "Error: $1 is not a known project which can be overlayed" + exit 1 + fi + + overlays[${project}_URL]=$ov_url + overlays[${project}_REF]=$ov_ref + fi } set +x for overlay in "${ci_dir}"/user-overlays/*.sh; do # shellcheck source=/dev/null - . "${overlay}" + # the directoy can be empty + if [ -e "${overlay}" ]; then . "${overlay}"; fi done # shellcheck source=ci-basic-overlay.sh diff --git a/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh b/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh deleted file mode 100644 index d9b49ad0d1..0000000000 --- a/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh +++ /dev/null @@ -1,18 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12218" ] || [ "$CI_BRANCH" = "numeral-notations-non-inductive" ]; then - - stdlib2_CI_REF=numeral-notations-non-inductive - stdlib2_CI_GITURL=https://github.com/proux01/stdlib2 - - hott_CI_REF=numeral-notations-non-inductive - hott_CI_GITURL=https://github.com/proux01/HoTT - - paramcoq_CI_REF=numeral-notations-non-inductive - paramcoq_CI_GITURL=https://github.com/proux01/paramcoq - - quickchick_CI_REF=numeral-notations-non-inductive - quickchick_CI_GITURL=https://github.com/proux01/QuickChick - - metacoq_CI_REF=numeral-notations-non-inductive - metacoq_CI_GITURL=https://github.com/proux01/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 deleted file mode 100644 index fb5947d218..0000000000 --- a/dev/ci/user-overlays/12449-SkySkimmer-minim-prop-toset.sh +++ /dev/null @@ -1,6 +0,0 @@ -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/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh deleted file mode 100644 index b7d21ed59c..0000000000 --- a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then - - elpi_CI_REF=record+refactor - elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi - -# mtac2_CI_REF=record+refactor -# mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2 - -fi diff --git a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh deleted file mode 100644 index 1473f6df8b..0000000000 --- a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh +++ /dev/null @@ -1,15 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12653" ] || [ "$CI_BRANCH" = "cumul-syntax" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi cumul-syntax - - overlay equations https://github.com/SkySkimmer/Coq-Equations cumul-syntax - - overlay mtac2 https://github.com/SkySkimmer/Mtac2 cumul-syntax - - overlay paramcoq https://github.com/SkySkimmer/paramcoq cumul-syntax - - overlay rewriter https://github.com/SkySkimmer/rewriter cumul-syntax - - overlay metacoq https://github.com/SkySkimmer/metacoq cumul-syntax - -fi diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh deleted file mode 100644 index 7680e8da78..0000000000 --- a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then - - equations_CI_REF=master+fix12873-better-unification - equations_CI_GITURL=https://github.com/herbelin/Coq-Equations - -fi diff --git a/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh b/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh deleted file mode 100644 index 8b223719ea..0000000000 --- a/dev/ci/user-overlays/13075-ppedrot-explicit-names-quotient.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13075" ] || [ "$CI_BRANCH" = "explicit-names-quotient" ]; then - - elpi_CI_REF=explicit-names-quotient - elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi - - coq_dpdgraph_CI_REF=explicit-names-quotient - coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph - -fi diff --git a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh b/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh deleted file mode 100644 index f16cf1497e..0000000000 --- a/dev/ci/user-overlays/13128-SkySkimmer-noinstance.sh +++ /dev/null @@ -1,5 +0,0 @@ -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/13139-ppedrot-clean-hint-constr.sh b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh deleted file mode 100644 index 2f70f43a2b..0000000000 --- a/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13139" ] || [ "$CI_BRANCH" = "clean-hint-constr" ]; then - - equations_CI_REF=clean-hint-constr - equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations - - fiat_parsers_CI_REF=clean-hint-constr - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat - -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 deleted file mode 100644 index 7d55cf6883..0000000000 --- a/dev/ci/user-overlays/13166-herbelin-master+fixes13165-missing-impargs-defined-fields.sh +++ /dev/null @@ -1,6 +0,0 @@ -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/13312-ejgallego-attributes+bool_single.sh b/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh deleted file mode 100644 index 3bdbcf7d6e..0000000000 --- a/dev/ci/user-overlays/13312-ejgallego-attributes+bool_single.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13312" ] || [ "$CI_BRANCH" = "attributes+bool_single" ]; then - - overlay unicoq https://github.com/ejgallego/unicoq attributes+bool_single - overlay elpi https://github.com/ejgallego/coq-elpi attributes+bool_single - -fi diff --git a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh b/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh deleted file mode 100644 index 95f0de2bd3..0000000000 --- a/dev/ci/user-overlays/13386-master+fix9971-primproj-canonical-structure-on-evar-type.sh +++ /dev/null @@ -1,9 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13386" ] || [ "$CI_BRANCH" = "master+fix9971-primproj-canonical-structure-on-evar-type" ]; then - - unicoq_CI_REF=master+adapting-coq-pr13386 - unicoq_CI_GITURL=https://github.com/herbelin/unicoq - - elpi_CI_REF=coq-master+adapting-coq-pr13386 - elpi_CI_GITURL=https://github.com/herbelin/coq-elpi - -fi diff --git a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh b/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh deleted file mode 100644 index 0bf806085e..0000000000 --- a/dev/ci/user-overlays/13415-SkySkimmer-intern-univs.sh +++ /dev/null @@ -1,8 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13415" ] || [ "$CI_BRANCH" = "intern-univs" ]; then - - overlay equations https://github.com/SkySkimmer/Coq-Equations intern-univs - - overlay paramcoq https://github.com/SkySkimmer/paramcoq intern-univs - - overlay elpi https://github.com/SkySkimmer/coq-elpi intern-univs -fi diff --git a/dev/ci/user-overlays/13481-elpi-1.12.sh b/dev/ci/user-overlays/13481-elpi-1.12.sh deleted file mode 100644 index a6be2e3a1a..0000000000 --- a/dev/ci/user-overlays/13481-elpi-1.12.sh +++ /dev/null @@ -1,6 +0,0 @@ -if [ "$CI_PULL_REQUEST" = "13481" ] || [ "$CI_BRANCH" = "elpi-1.12" ]; then - - elpi_CI_REF=coq-master+elpi.1.12 - elpi_hb_CI_REF=coq-master+coq-elpi-1.7.0+elpi-1.12 - -fi diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md index 3f9ad5e878..14ee5e4199 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -21,14 +21,11 @@ and the branch name), then a `.sh` extension (`[0-9]{5}-[a-zA-Z0-9-_]+.sh`). Example: `13128-SkySkimmer-noinstance.sh` containing ``` -if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance - -fi +overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance 13128 ``` -(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh)) +See [`ci-common.sh`](../ci-common.sh) for the detailed documentation of +the `overlay` function. ### Branching conventions diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5adeafaa38..26c4b01c9f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -37,6 +37,11 @@ Dumpglob: plugins to temporarily change/pause the output of Dumpglob, and then restore it to the original setting. +Glob_term: + +- Removing useless `binding_kind` argument of `GLocalDef` in + `extended_glob_local_binder`. + ## 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 78ed27ba03..ac8fd1676d 100755 --- a/dev/tools/create_overlays.sh +++ b/dev/tools/create_overlays.sh @@ -42,7 +42,7 @@ OVERLAY_BRANCH=$(git rev-parse --abbrev-ref HEAD) OVERLAY_FILE=$(mktemp overlay-XXXX) # Create the overlay file -printf 'if [ "$CI_PULL_REQUEST" = "%s" ] || [ "$CI_BRANCH" = "%s" ]; then\n\n' "$PR_NUMBER" "$OVERLAY_BRANCH" > "$OVERLAY_FILE" +> "$OVERLAY_FILE" # We first try to build the contribs while test $# -gt 0 @@ -66,12 +66,11 @@ do make ci-$_CONTRIB_NAME || true setup_contrib_git $_CONTRIB_DIR $_CONTRIB_GITPUSHURL - echo " overlay ${_CONTRIB_NAME} $_CONTRIB_GITURL $OVERLAY_BRANCH" >> $OVERLAY_FILE + echo "overlay ${_CONTRIB_NAME} $_CONTRIB_GITURL $OVERLAY_BRANCH $PR_NUMBER" >> $OVERLAY_FILE echo "" >> $OVERLAY_FILE shift done -# End the file; copy to overlays folder. -echo "fi" >> $OVERLAY_FILE +# Copy to overlays folder. PR_NUMBER=$(printf '%05d' "$PR_NUMBER") mv $OVERLAY_FILE dev/ci/user-overlays/$PR_NUMBER-$DEVELOPER_NAME-${OVERLAY_BRANCH///}.sh diff --git a/dev/tools/notify-upstream-pins.sh b/dev/tools/notify-upstream-pins.sh index 37fe0cbcbf..ebf920b0f7 100755 --- a/dev/tools/notify-upstream-pins.sh +++ b/dev/tools/notify-upstream-pins.sh @@ -14,24 +14,6 @@ REASON="bundled in the Windows installer" git show master:dev/ci/ci-basic-overlay.sh > /tmp/master-ci-basic-overlay.sh git show v${VERSION}:dev/ci/ci-basic-overlay.sh > /tmp/branch-ci-basic-overlay.sh -# caveats: -# - dev/ci/gitlab.bat has \r (windows) -# - aactactics, gappa, HB, extlib have different names in ci -# - menhir is not pinned but figures as an addon -# - unicoq is not an addon -WINDOWS_ADDONS=$(grep addon= dev/ci/gitlab.bat \ - | cut -d = -f 2 \ - | cut -d ' ' -f 1 \ - | tr -d '\r' \ - | sed -e 's/^aactactics$/aac_tactics/' \ - -e 's/^gappa$/gappa_plugin/' \ - -e 's/^HB$/elpi_hb/' \ - -e 's/^extlib$/ext_lib/' \ - \ - -e '/^menhir$/d' \ - ) \ -WINDOWS_ADDONS="$WINDOWS_ADDONS unicoq" - # reads a variable value from a ci-basic-overlay.sh file function read_from() { ( . $1; varname="$2"; echo ${!varname} ) @@ -99,7 +81,10 @@ $CC esac } -for addon in $WINDOWS_ADDONS; do +# TODO: filter w.r.t. what is in the platform +PROJECTS=`read_from /tmp/branch-ci-basic-overlay.sh "projects[@]"` + +for addon in $PROJECTS; do URL=`read_from /tmp/master-ci-basic-overlay.sh "${addon}_CI_GITURL"` REF=`read_from /tmp/master-ci-basic-overlay.sh "${addon}_CI_REF"` PIN=`read_from /tmp/branch-ci-basic-overlay.sh "${addon}_CI_REF"` diff --git a/doc/changelog/03-notations/13519-primitiveArrayNotations.rst b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst new file mode 100644 index 0000000000..fb2545652c --- /dev/null +++ b/doc/changelog/03-notations/13519-primitiveArrayNotations.rst @@ -0,0 +1,8 @@ +- **Added:** + :cmd:`Number Notation` and :cmd:`String Notation` now support + parsing and printing of primitive floats, primitive arrays + and type constants of primitive types. + (`#13519 <https://github.com/coq/coq/pull/13519>`_, + fixes `#13484 <https://github.com/coq/coq/issues/13484>`_ + and `#13517 <https://github.com/coq/coq/issues/13517>`_, + by Fabian Kunze, with help of Jason Gross) diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 73f90b0056..259f5e0546 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1740,7 +1740,8 @@ Number notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. .. _number-string-via: @@ -1904,7 +1905,8 @@ String notations Note that only fully-reduced ground terms (terms containing only function application, constructors, inductive type families, - sorts, and primitive integers) will be considered for printing. + sorts, primitive integers, primitive floats, primitive arrays and type + constants for primitive types) will be considered for printing. :n:`via @qualid__ind mapping [ {+, @qualid__constant => @qualid__constructor } ]` works as for :ref:`number notations above <number-string-via>`. diff --git a/engine/evd.ml b/engine/evd.ml index 59eea97ce9..706e51d4b3 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -983,6 +983,9 @@ let fresh_inductive_instance ?loc ?(rigid=univ_flexible) env evd i = let fresh_constructor_instance ?loc ?(rigid=univ_flexible) env evd c = with_context_set ?loc rigid evd (UnivGen.fresh_constructor_instance env c) +let fresh_array_instance ?loc ?(rigid=univ_flexible) env evd = + with_context_set ?loc rigid evd (UnivGen.fresh_array_instance env) + let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) diff --git a/engine/evd.mli b/engine/evd.mli index 911e00c23a..a6d55c2615 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -698,6 +698,8 @@ val fresh_inductive_instance : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> constructor -> evar_map * pconstructor +val fresh_array_instance : ?loc:Loc.t -> ?rigid:rigid + -> env -> evar_map -> evar_map * Univ.Instance.t val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> GlobRef.t -> evar_map * econstr diff --git a/engine/univGen.ml b/engine/univGen.ml index 6f27ccb7dc..278ca6bf34 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -65,6 +65,11 @@ let fresh_constructor_instance env c = let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in (c, u), ctx +let fresh_array_instance env = + let auctx = CPrimitives.typ_univs CPrimitives.PT_array in + let u, ctx = fresh_instance_from auctx None in + u, ctx + let fresh_global_instance ?loc ?names env gr = let u, ctx = fresh_global_instance ?loc ?names env gr in mkRef (gr, u), ctx diff --git a/engine/univGen.mli b/engine/univGen.mli index 81bdac17ce..05737411f5 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -42,6 +42,8 @@ val fresh_inductive_instance : env -> inductive -> pinductive in_universe_context_set val fresh_constructor_instance : env -> constructor -> pconstructor in_universe_context_set +val fresh_array_instance : env -> + Instance.t in_universe_context_set val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3969c7ea1f..f3ba884856 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -886,9 +886,10 @@ let extern_prim_token_delimiter_if_required n key_n scope_n scopes = let extended_glob_local_binder_of_decl loc = function | (p,bk,None,t) -> GLocalAssum (p,bk,t) | (p,bk,Some x, t) -> + assert (bk = Explicit); match DAst.get t with - | GHole (_, IntroAnonymous, None) -> GLocalDef (p,bk,x,None) - | _ -> GLocalDef (p,bk,x,Some t) + | GHole (_, IntroAnonymous, None) -> GLocalDef (p,x,None) + | _ -> GLocalDef (p,x,Some t) let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_local_binder_of_decl loc u) @@ -1217,7 +1218,7 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | b :: l -> match DAst.get b with - | GLocalDef (na,bk,bd,ty) -> + | GLocalDef (na,bd,ty) -> let (assums,ids,l) = extern_local_binder scopes (on_fst (Name.fold_right Id.Set.add na) vars) l in (assums,na::ids, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e3a4d1b169..70a4ea35e9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -560,10 +560,10 @@ let intern_assumption intern ntnvars env nal bk ty = let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function | GLocalAssum (na,bk,t) -> (na,bk,None,t) - | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t) - | GLocalDef (na,bk,c,None) -> + | GLocalDef (na,c,Some t) -> (na,Explicit,Some c,t) + | GLocalDef (na,c,None) -> let t = DAst.make ?loc @@ GHole(Evar_kinds.BinderType na,IntroAnonymous,None) in - (na,bk,Some c,t) + (na,Explicit,Some c,t) | GLocalPattern (_,_,_,_) -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here") ) @@ -575,7 +575,7 @@ let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = let ty = Option.map (intern (set_type_scope (restart_prod_binders env))) ty in let impls = impls_term_list 1 term in (push_name_env ntnvars impls env locna, - (na,Explicit,term,ty)) + (na,term,ty)) let intern_cases_pattern_as_binder intern test_kind ntnvars env bk (CAst.{v=p;loc} as pv) = let p,t = match p with @@ -606,8 +606,8 @@ let intern_local_binder_aux intern ntnvars (env,bl) = function let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl | CLocalDef( {loc; v=na} as locna,def,ty) -> - let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in - env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl + let env,(na,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in + env, (DAst.make ?loc @@ GLocalDef (na,def,ty)) :: bl | CLocalPattern p -> let env, ((disjpat,il),id),na,bk,t = intern_cases_pattern_as_binder intern test_kind_tolerant ntnvars env Explicit p in (env, (DAst.make ?loc:p.CAst.loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) @@ -650,7 +650,7 @@ let rec expand_binders ?loc mk bl c = | [] -> c | b :: bl -> match DAst.get b with - | GLocalDef (n, bk, b, oty) -> + | GLocalDef (n, b, oty) -> expand_binders ?loc mk bl (DAst.make ?loc @@ GLetIn (n, b, oty, c)) | GLocalAssum (n, bk, t) -> expand_binders ?loc mk bl (mk ?loc (n,bk,t) c) @@ -794,8 +794,8 @@ let terms_of_binders bl = let loc = bnd.loc in begin match DAst.get bnd with | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l - | GLocalDef (Name id,_,_,_) -> extract_variables l - | GLocalDef (Anonymous,_,_,_) + | GLocalDef (Name id,_,_) -> extract_variables l + | GLocalDef (Anonymous,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") | GLocalPattern (([u],_),_,_,_) -> term_of_pat u :: extract_variables l | GLocalPattern ((_,_),_,_,_) -> error_cannot_coerce_disjunctive_pattern_term ?loc () @@ -847,7 +847,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | AddTermIter nterms::rest,terminator,iter -> aux (nterms,None,Some (rest,terminator,iter)) (renaming,env) iter | AddLetIn (na,c,t)::rest,terminator,iter -> - let env,(na,_,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in + let env,(na,c,t) = intern_letin_binder intern ntnvars (adjust_env env iter) (na,c,t) in DAst.make ?loc (GLetIn (na,c,t,aux_letin env (rest,terminator,iter))) in aux_letin env (Option.get iteropt) | NVar id -> subst_var subst' (renaming, env) id diff --git a/interp/notation.ml b/interp/notation.ml index 912e52cec8..f2d113954b 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -640,7 +640,7 @@ let constr_of_globref allow_constant env sigma = function | GlobRef.IndRef c -> let sigma,c = Evd.fresh_inductive_instance env sigma c in sigma,mkIndU c - | GlobRef.ConstRef c when allow_constant -> + | GlobRef.ConstRef c when allow_constant || Environ.is_primitive_type env c -> let sigma,c = Evd.fresh_constant_instance env sigma c in sigma,mkConstU c | _ -> raise NotAValidPrimToken @@ -692,6 +692,13 @@ let rec constr_of_glob allow_constant to_post post env sigma g = match DAst.get sigma,mkApp (c, Array.of_list cl) end | Glob_term.GInt i -> sigma, mkInt i + | Glob_term.GFloat f -> sigma, mkFloat f + | Glob_term.GArray (_,t,def,ty) -> + let sigma, u' = Evd.fresh_array_instance env sigma in + let sigma, def' = constr_of_glob allow_constant to_post post env sigma def in + let sigma, t' = Array.fold_left_map (constr_of_glob allow_constant to_post post env) sigma t in + let sigma, ty' = constr_of_glob allow_constant to_post post env sigma ty in + sigma, mkArray (u',t',def',ty') | Glob_term.GSort gs -> let sigma,c = Evd.fresh_sort_in_family sigma (Glob_ops.glob_sort_family gs) in sigma,mkSort c @@ -712,6 +719,12 @@ let rec glob_of_constr token_kind ?loc env sigma c = match Constr.kind c with | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (GlobRef.IndRef ind, None)) | Var id -> DAst.make ?loc (Glob_term.GRef (GlobRef.VarRef id, None)) | Int i -> DAst.make ?loc (Glob_term.GInt i) + | Float f -> DAst.make ?loc (Glob_term.GFloat f) + | Array (u,t,def,ty) -> + let def' = glob_of_constr token_kind ?loc env sigma def + and t' = Array.map (glob_of_constr token_kind ?loc env sigma) t + and ty' = glob_of_constr token_kind ?loc env sigma ty in + DAst.make ?loc (Glob_term.GArray (None,t',def',ty')) | Sort Sorts.SProp -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSProp, 0])) | Sort Sorts.Prop -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GProp, 0])) | Sort Sorts.Set -> DAst.make ?loc (Glob_term.GSort (Glob_term.UNamed [Glob_term.GSet, 0])) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 036970ce37..0e7f085bde 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -863,7 +863,7 @@ let rec push_context_binders vars = function let vars = match DAst.get b with | GLocalAssum (na,_,_) -> Termops.add_vname vars na | GLocalPattern ((disjpat,ids),p,bk,t) -> List.fold_right Id.Set.add ids vars - | GLocalDef (na,_,_,_) -> Termops.add_vname vars na in + | GLocalDef (na,_,_) -> Termops.add_vname vars na in push_context_binders vars bl let is_term_meta id metas = @@ -1014,9 +1014,9 @@ let unify_binder_upto alp b b' = | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') -> let alp, na = unify_name_upto alp na na' in alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t') - | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') -> + | GLocalDef (na,c,t), GLocalDef (na',c',t') -> let alp, na = unify_name_upto alp na na' in - alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') + alp, DAst.make ?loc @@ GLocalDef (na, unify_term alp c c', unify_opt_term alp t t') | GLocalPattern ((disjpat,ids),id,bk,t), GLocalPattern ((disjpat',_),_,bk',t') when List.length disjpat = List.length disjpat' -> let alp, p = List.fold_left2_map unify_pat_upto alp disjpat disjpat' in alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t') @@ -1061,7 +1061,7 @@ let rec unify_terms_binders alp cl bl' = | [], [] -> [] | c :: cl, b' :: bl' -> begin match DAst.get b' with - | GLocalDef ( _, _, _, t) -> unify_terms_binders alp cl bl' + | GLocalDef (_, _, t) -> unify_terms_binders alp cl bl' | _ -> unify_term_binder alp c b' :: unify_terms_binders alp cl bl' end | _ -> raise No_match @@ -1249,7 +1249,7 @@ let match_binderlist match_fun alp metas sigma rest x y iter termin revert = with No_match -> match DAst.get rest with | GLetIn (na,c,t,rest') when glue_inner_letin_with_decls -> - let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,Explicit (*?*), c,t) in + let b = DAst.make ?loc:rest.CAst.loc @@ GLocalDef (na,c,t) in (* collect let-in *) (try aux true sigma (b::bl) rest' with OnlyTrailingLetIns diff --git a/kernel/environ.ml b/kernel/environ.ml index a5f81d1e59..6f2aeab203 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -571,11 +571,26 @@ let is_primitive env c = | Declarations.Primitive _ -> true | _ -> false +let is_int63_type env c = + match env.retroknowledge.Retroknowledge.retro_int63 with + | None -> false + | Some c' -> Constant.CanOrd.equal c c' + +let is_float64_type env c = + match env.retroknowledge.Retroknowledge.retro_float64 with + | None -> false + | Some c' -> Constant.CanOrd.equal c c' + let is_array_type env c = match env.retroknowledge.Retroknowledge.retro_array with | None -> false | Some c' -> Constant.CanOrd.equal c c' +let is_primitive_type env c = + (* dummy match to force an update if we add a primitive type, seperated clauses to satisfy ocaml 4.05 *) + let _ = function CPrimitives.(PTE(PT_int63)) -> () | CPrimitives.(PTE(PT_float64)) -> () | CPrimitives.(PTE(PT_array)) -> () in + is_int63_type env c || is_float64_type env c || is_array_type env c + let polymorphic_constant cst env = Declareops.constant_is_polymorphic (lookup_constant cst env) diff --git a/kernel/environ.mli b/kernel/environ.mli index 900e2128ea..dfd9173d10 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -250,6 +250,10 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option val is_primitive : env -> Constant.t -> bool val is_array_type : env -> Constant.t -> bool +val is_int63_type : env -> Constant.t -> bool +val is_float64_type : env -> Constant.t -> bool +val is_primitive_type : env -> Constant.t -> bool + (** {6 Primitive projections} *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 4c1fe6417e..9abdc2ddbe 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -429,7 +429,15 @@ let pr_value env v = | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) -let error_ltac_variable ?loc id env v s = - CErrors.user_err ?loc (str "Ltac variable " ++ Id.print id ++ +exception CoercionError of Id.t * (Environ.env * Evd.evar_map) option * Val.t * string + +let () = CErrors.register_handler begin function +| CoercionError (id, env, v, s) -> + Some (str "Ltac variable " ++ Id.print id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") +| _ -> None +end + +let error_ltac_variable ?loc id env v s = + Loc.raise ?loc (CoercionError (id, env, v, s)) diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a957bc0fcd..9f93e5e6c1 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -137,7 +137,7 @@ type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g - | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option + | GLocalDef of Name.t * 'a glob_constr_g * 'a glob_constr_g option | GLocalPattern of ('a cases_pattern_disjunction_g * Id.t list) * Id.t * binding_kind * 'a glob_constr_g and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t diff --git a/test-suite/output/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out new file mode 100644 index 0000000000..131975c760 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.out @@ -0,0 +1,20 @@ +"abc" + : intList +"abc" + : intList +mk_intList [97%int63; 98%int63; 99%int63] + : intList +"abc" + : intArray +"abc" + : intArray + = "abc" + : nestArray +"abc" + : nestArray +"100" + : floatList +"100" + : floatList +mk_floatList [1%float; 0%float; 0%float] + : floatList diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v new file mode 100644 index 0000000000..23ef082013 --- /dev/null +++ b/test-suite/output/StringSyntaxPrimitive.v @@ -0,0 +1,139 @@ +Require Import Coq.Lists.List. +Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii. +Require Coq.Array.PArray Coq.Floats.PrimFloat. +Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63. + +Set Printing Depth 100000. +Set Printing Width 1000. + +Close Scope char_scope. +Close Scope string_scope. + +(* Notations for primitive integers inside polymorphic datatypes *) +Module Test1. + Inductive intList := mk_intList (_ : list int). + Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a. + + Definition from_byte_list (xs : list byte) : intList:= + mk_intList (List.map i63_from_byte xs). + + Declare Scope intList_scope. + Delimit Scope intList_scope with intList. + + String Notation intList from_byte_list to_byte_list : intList_scope. + + Open Scope intList_scope. + Import List.ListNotations. + Check mk_intList [97; 98; 99]%int63%list. + Check "abc"%intList. + + Definition int' := int. + Check mk_intList (@cons int' 97 [98; 99])%int63%list. +End Test1. + +Import PArray. + +(* Notations for primitive arrays *) +Module Test2. + Inductive intArray := mk_intArray (_ : array int). + + Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)). + Definition i63_to_byte (i : Int63.int) : byte := + match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end. + + Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x). + Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x). + + Local Fixpoint list_length_i63 {A} (xs : list A) :int := + match xs with + | nil => 0 + | cons _ xs => 1 + list_length_i63 xs + end. + + Definition to_byte_list '(mk_intArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc) + end) (nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (list_length_i63 xs) 0 in + mk_intArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x]) + end) 0 xs arr))%int63. + + Declare Scope intArray_scope. + Delimit Scope intArray_scope with intArray. + + String Notation intArray from_byte_list to_byte_list : intArray_scope. + + Open Scope intArray_scope. + Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array. + Check "abc"%intArray. + +End Test2. + +(* Primitive arrays inside primitive arrays *) +Module Test3. + + Inductive nestArray := mk_nestArray (_ : array (array int)). + Definition to_byte_list '(mk_nestArray a) := + ((fix go (n : nat) (i : Int63.int) (acc : list byte) := + match n with + | 0 => acc + | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc) + end) (Test2.nat_length a) (length a - 1) nil)%int63. + + Definition from_byte_list (xs : list byte) := + (let arr := make (Test2.list_length_i63 xs) (make 0 0) in + mk_nestArray ((fix go i xs acc := + match xs with + | nil => acc + | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)]) + end) 0 xs arr))%int63. + + Declare Scope nestArray_scope. + Delimit Scope nestArray_scope with nestArray. + + String Notation nestArray from_byte_list to_byte_list : nestArray_scope. + + Open Scope nestArray_scope. + Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array. + Check "abc"%nestArray. +End Test3. + + + +(* Notations for primitive floats inside polymorphic datatypes *) +Module Test4. + Import PrimFloat. + Inductive floatList := mk_floatList (_ : list float). + Definition float_from_byte (b : byte) : float := + if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one. + Definition float_to_byte (f : float) : byte := + if PrimFloat.is_zero f then "0" else "1". + Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a. + + Definition from_byte_list (xs : list byte) : floatList:= + mk_floatList (List.map float_from_byte xs). + + Declare Scope floatList_scope. + Delimit Scope floatList_scope with floatList. + + String Notation floatList from_byte_list to_byte_list : floatList_scope. + + Open Scope floatList_scope. + Import List.ListNotations. + Check mk_floatList [97; 0; 0]%float%list. + Check "100"%floatList. + + Definition float' := float. + Check mk_floatList (@cons float' 1 [0; 0])%float%list. +End Test4. |