diff options
73 files changed, 785 insertions, 644 deletions
diff --git a/INSTALL.md b/INSTALL.md index f672bb45d3..74f4091134 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -99,3 +99,13 @@ dependencies...) as Coq. Distribution of pre-compiled plugins and Coq version compiled with the same OCaml toolchain. An OCaml setup mismatch is the most probable cause for an `Error while loading ...: implementation mismatch on ...`. + +coq_environment.txt +------------------- +Coq binaries which honor environment variables, such as `COQLIB`, can +be seeded values for these variables by placing a text file named +`coq_environment.txt` next to them. The file can contain assignments +like `COQLIB="some path"`, that is a variable name followed by `=` and +a string that follows OCaml's escaping conventions. This feature can be +used by installers of binary package to make Coq aware of its installation +path. diff --git a/clib/cList.ml b/clib/cList.ml index 6b13fac48c..d5520aa2b7 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -23,6 +23,7 @@ sig val for_all_i : (int -> 'a -> bool) -> int -> 'a list -> bool val for_all2eq : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool val prefix_of : 'a eq -> 'a list -> 'a list -> bool + val same_length : 'a list -> 'b list -> bool val interval : int -> int -> int list val make : int -> 'a -> 'a list val addn : int -> 'a -> 'a list -> 'a list @@ -154,6 +155,11 @@ external cast : 'a cell -> 'a list = "%identity" (** {6 Equality, testing} *) +let rec same_length l1 l2 = match l1, l2 with +| [], [] -> true +| _ :: l1, _ :: l2 -> same_length l1 l2 +| ([], _ :: _) | (_ :: _, []) -> false + let rec compare cmp l1 l2 = if l1 == l2 then 0 else match l1,l2 with diff --git a/clib/cList.mli b/clib/cList.mli index c8e471f989..6c8df88767 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -42,6 +42,9 @@ sig (** [prefix_of eq l1 l2] returns [true] if [l1] is a prefix of [l2], [false] otherwise. It uses [eq] to compare elements *) + val same_length : 'a list -> 'b list -> bool + (** A more efficient variant of [for_all2eq (fun _ _ -> true)] *) + (** {6 Creating lists} *) val interval : int -> int -> int list diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 18fdd83218..b65430aa51 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 "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 hierarchy_builder "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/ci-elpi.sh b/dev/ci/ci-elpi.sh index 4f185db813..d8caf8ee87 100755 --- a/dev/ci/ci-elpi.sh +++ b/dev/ci/ci-elpi.sh @@ -7,6 +7,6 @@ git_download elpi ( cd "${CI_BUILD_DIR}/elpi" && make && make install ) -git_download elpi_hb +git_download hierarchy_builder -( cd "${CI_BUILD_DIR}/elpi_hb" && make && make install ) +( cd "${CI_BUILD_DIR}/hierarchy_builder" && make && make install ) diff --git a/dev/ci/ci-gappa.sh b/dev/ci/ci-gappa.sh index c346354b70..1af37aa7c1 100755 --- a/dev/ci/ci-gappa.sh +++ b/dev/ci/ci-gappa.sh @@ -7,6 +7,6 @@ git_download gappa_tool ( cd "${CI_BUILD_DIR}/gappa_tool" && ( if [ ! -x ./configure ]; then autoreconf && touch stamp-config_h.in && ./configure --prefix=${CI_INSTALL_DIR}; fi ) && ./remake "-j${NJOBS}" && ./remake install ) -git_download gappa_plugin +git_download gappa -( cd "${CI_BUILD_DIR}/gappa_plugin" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) +( cd "${CI_BUILD_DIR}/gappa" && ( if [ ! -x ./configure ]; then autoconf && ./configure; fi ) && ./remake "-j${NJOBS}" && ./remake install ) 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..cf1d71c1cd 100644 --- a/dev/ci/user-overlays/README.md +++ b/dev/ci/user-overlays/README.md @@ -5,30 +5,29 @@ 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. 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. - +version so that testing is possible. 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: `13128-SkySkimmer-noinstance.sh` containing - +This file must contain one or more invocation of the `overlay` function: ``` -if [ "$CI_PULL_REQUEST" = "13128" ] || [ "$CI_BRANCH" = "noinstance" ]; then - - overlay elpi https://github.com/SkySkimmer/coq-elpi noinstance +overlay <project> <giturl> <ref> <prnumber> [<prbranch>] +``` +Each call creates an overlay for `project` using a given `giturl` and +`ref` which is active for `prnumber` or `prbranch` (`prbranch` defaults +to `ref`). -fi +Example of an overlay for the project `elpi` that uses the branch `noinstance` +from the fork of `SkySkimmer` and is active for pull request `13128` +``` +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)) +Such a file can be created automatically using the scripts +[`create_overlays.sh`](../../dev/tools/create_overlays.sh). +See also the list of projects for which one can write an overlay in +the file [`ci-basic-overlay.sh`](../ci-basic-overlay.sh). ### 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/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh index dbf54d7f0a..676688bedc 100755 --- a/dev/tools/pin-ci.sh +++ b/dev/tools/pin-ci.sh @@ -38,9 +38,7 @@ process_development() { # Execute the script to set the overlay variables . $OVERLAYS -# Find all variables declared in the base overlay of the form *_CI_GITURL -for REPO_VAR in $(compgen -A variable | grep _CI_GITURL) +for project in ${projects[@]} do - DEV=${REPO_VAR%_CI_GITURL} - process_development $DEV + process_development $project done 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/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst new file mode 100644 index 0000000000..06c1e280c3 --- /dev/null +++ b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst @@ -0,0 +1,6 @@ +- **Removed:** + Deprecated flag ``Bracketing Last Introduction Pattern`` affecting the + behavior of trailing disjunctive introduction patterns is + definitively removed + (`#13509 <https://github.com/coq/coq/pull/13509>`_, + by Hugo Herbelin). diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-vernac-commands-and-options/00000-title.rst index fe50ae0e16..fe50ae0e16 100644 --- a/doc/changelog/07-commands-and-options/00000-title.rst +++ b/doc/changelog/07-vernac-commands-and-options/00000-title.rst diff --git a/doc/changelog/07-commands-and-options/13556-master.rst b/doc/changelog/07-vernac-commands-and-options/13556-master.rst index 05a60026a3..05a60026a3 100644 --- a/doc/changelog/07-commands-and-options/13556-master.rst +++ b/doc/changelog/07-vernac-commands-and-options/13556-master.rst diff --git a/doc/changelog/08-cli-tools/00000-title.rst b/doc/changelog/08-cli-tools/00000-title.rst new file mode 100644 index 0000000000..4c0de43f66 --- /dev/null +++ b/doc/changelog/08-cli-tools/00000-title.rst @@ -0,0 +1,4 @@ + +Command-line tools +^^^^^^^^^^^^^^^^^^ + diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst deleted file mode 100644 index 581585a8a7..0000000000 --- a/doc/changelog/08-tools/00000-title.rst +++ /dev/null @@ -1,4 +0,0 @@ - -Tools -^^^^^ - diff --git a/doc/changelog/10-standard-library/13582-exp_ineq.rst b/doc/changelog/10-standard-library/13582-exp_ineq.rst new file mode 100644 index 0000000000..27d89b2f8b --- /dev/null +++ b/doc/changelog/10-standard-library/13582-exp_ineq.rst @@ -0,0 +1,9 @@ +- **Changed:** + Minor Changes to Rpower: + Generalizes exp_ineq1 to hold for all non-zero numbers. + Adds exp_ineq1_le, which holds for all reals (but is a <= instead of a <). + + (`#13582 <https://github.com/coq/coq/pull/13582>`_, + by Avi Shinnar and Barry Trager, with help from Laurent Théry + +). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 726a6309d4..fcb150e3da 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -370,7 +370,8 @@ Notations by Pierre Roux, review by Jason Gross and Jim Fehrle for the reference manual). - **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`. + This feature is considered experimental. (`#12765 <https://github.com/coq/coq/pull/12765>`_, by Hugo Herbelin). - **Added:** diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 246568d3c1..bce88cebde 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -220,7 +220,7 @@ html_context = { ("dev", "https://coq.github.io/doc/master/refman/"), ("stable", "https://coq.inria.fr/distrib/current/refman/"), ("v8.13", "https://coq.github.io/doc/v8.13/refman/"), - ("8.12", "https://coq.inria.fr/distrib/V8.12.1/refman/"), + ("8.12", "https://coq.inria.fr/distrib/V8.12.2/refman/"), ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"), ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"), ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"), diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8f5c045929..d8c4fb61c2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -264,17 +264,6 @@ These patterns can be used when the hypothesis is an equality: :n:`@simple_intropattern_closed`. :ref:`Example <intropattern_injection_ex>` -.. flag:: Bracketing Last Introduction Pattern - - For :n:`intros @intropattern_list`, controls how to handle a - conjunctive pattern that doesn't give enough simple patterns to match - all the arguments in the constructor. If set (the default), Coq generates - additional names to match the number of arguments. - Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more - similar to |SSR|'s intro patterns. - - .. deprecated:: 8.10 - .. _intropattern_cons_note: .. note:: diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index b7f2927000..3649202b45 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -522,7 +522,7 @@ the conversion in hypotheses :n:`{+ @ident}`. use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. - The :tacn:`cbn` tactic is claimed to be a more principled, faster and more + The :tacn:`cbn` tactic was intended to be a more principled, faster and more predictable replacement for :tacn:`simpl`. The :tacn:`cbn` tactic accepts the same flags as :tacn:`cbv` and diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 73f90b0056..f454f4313d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -857,7 +857,8 @@ example showing a notation for a chain of equalities. It relies on an artificial expansion of the intended denotation so as to expose a ``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the beta-redexes are contracted, the notations stops to be used for -printing. +printing. Support for notations defined in this way should be considered +experimental. .. coqtop:: in @@ -1740,7 +1741,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 +1906,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/proofview.ml b/engine/proofview.ml index 22863f451d..b3061eaa81 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -909,10 +909,11 @@ let tclPROGRESS t = in let test = quick_test || + (CList.same_length initial.comb final.comb && Util.List.for_all2eq begin fun i f -> Progress.goal_equal ~evd:initial.solution ~extended_evd:final.solution (drop_state i) (drop_state f) - end initial.comb final.comb + end initial.comb final.comb) in if not test then tclUNIT res 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 c35ba44aa5..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])) @@ -782,13 +795,7 @@ end let z_two = Z.of_int 2 (** Conversion from bigint to int63 *) -let rec int63_of_pos_bigint i = - if Z.(equal i zero) then Uint63.of_int 0 - else - let quo, remi = Z.div_rem i z_two in - if Z.(equal remi one) then Uint63.add (Uint63.of_int 1) - (Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo)) - else Uint63.mul (Uint63.of_int 2) (int63_of_pos_bigint quo) +let int63_of_pos_bigint i = Uint63.of_int64 (Z.to_int64 i) module Numbers = struct (** * Number notation *) @@ -1041,7 +1048,7 @@ let interp_int63 ?loc n = let bigint_of_int63 c = match Constr.kind c with - | Int i -> Z.of_string (Uint63.to_string i) + | Int i -> Z.of_int64 (Uint63.to_int64 i) | _ -> raise NotAValidPrimToken let interp o ?loc n = 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/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index d92bbe87eb..13568957c2 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -20,7 +20,7 @@ # define DECLARE_NULLOP(name) \ value uint63_##name() { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam0(); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(*cb); \ @@ -28,7 +28,7 @@ value uint63_##name() { \ # define DECLARE_UNOP(name) \ value uint63_##name##_ml(value x) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam1(x); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback(*cb, x)); \ @@ -53,7 +53,7 @@ value uint63_##name##_ml(value x) { \ # define DECLARE_BINOP(name) \ value uint63_##name##_ml(value x, value y) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam2(x, y); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback2(*cb, x, y)); \ @@ -79,7 +79,7 @@ value uint63_##name##_ml(value x, value y) { \ # define DECLARE_TEROP(name) \ value uint63_##name##_ml(value x, value y, value z) { \ - static value* cb = 0; \ + static value const *cb = 0; \ CAMLparam3(x, y, z); \ if (!cb) cb = caml_named_value("uint63 " #name); \ CAMLreturn(caml_callback3(*cb, x, y, z)); \ 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/kernel/uint63.mli b/kernel/uint63.mli index 6b47dfc61d..6b2519918a 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -17,6 +17,7 @@ val maxuint31 : t val of_int : int -> t val to_int2 : t -> int * int (* msb, lsb *) val of_int64 : Int64.t -> t +val to_int64 : t -> Int64.t (* val of_uint : int -> t *) @@ -32,7 +33,6 @@ val hash : t -> int (* conversion to a string *) val to_string : t -> string -val of_string : string -> t val compile : t -> string diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 5b2d934b5d..988611df3e 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -23,9 +23,10 @@ let one = Int64.one (* conversion from an int *) let mask63 i = Int64.logand i maxuint63 -let of_int i = Int64.of_int i +let of_int i = mask63 (Int64.of_int i) let to_int2 i = (Int64.to_int (Int64.shift_right_logical i 31), Int64.to_int i) -let of_int64 i = i +let of_int64 = mask63 +let to_int64 i = i let to_int_min n m = if Int64.(compare n (of_int m)) < 0 then Int64.to_int n else m @@ -41,13 +42,6 @@ let hash i = (* conversion of an uint63 to a string *) let to_string i = Int64.to_string i -let of_string s = - let i64 = Int64.of_string s in - if Int64.compare Int64.zero i64 <= 0 - && Int64.compare i64 maxuint63 <= 0 - then i64 - else raise (Failure "Int63.of_string") - (* Compiles an unsigned int to OCaml code *) let compile i = Printf.sprintf "Uint63.of_int64 (%LiL)" i @@ -72,12 +66,12 @@ let l_xor x y = Int64.logxor x y (* addition of int63 *) let add x y = mask63 (Int64.add x y) -let addcarry x y = add (add x y) Int64.one +let addcarry x y = mask63 Int64.(add (add x y) one) (* subtraction *) let sub x y = mask63 (Int64.sub x y) -let subcarry x y = sub (sub x y) Int64.one +let subcarry x y = mask63 Int64.(sub (sub x y) one) (* multiplication *) let mul x y = mask63 (Int64.mul x y) diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 21f57e2bfb..8d052d6593 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -25,7 +25,8 @@ let of_int i = i let to_int2 i = (0,i) -let of_int64 _i = assert false +let of_int64 = Int64.to_int +let to_int64 = to_uint64 let of_float = int_of_float @@ -39,13 +40,6 @@ let hash i = i (* conversion of an uint63 to a string *) let to_string i = Int64.to_string (to_uint64 i) -let of_string s = - let i64 = Int64.of_string s in - if Int64.compare Int64.zero i64 <= 0 - && Int64.compare i64 maxuint63 <= 0 - then Int64.to_int i64 - else raise (Failure "Int64.of_string") - (* Compiles an unsigned int to OCaml code *) let compile i = Printf.sprintf "Uint63.of_int (%i)" i diff --git a/lib/envars.ml b/lib/envars.ml index 585d5185b4..1702b5d7a2 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -12,7 +12,37 @@ open Util (** {1 Helper functions} *) -let getenv_else s dft = try Sys.getenv s with Not_found -> dft () +let parse_env_line l = + try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value)) + with _ -> None + +let with_ic file f = + let ic = open_in file in + try + let rc = f ic in + close_in ic; + rc + with e -> close_in ic; raise e + +let getenv_from_file name = + let base = Filename.dirname Sys.executable_name in + try + with_ic (base ^ "/coq_environment.txt") (fun ic -> + let rec find () = + let l = input_line ic in + match parse_env_line l with + | Some(n,v) when n = name -> v + | _ -> find () + in + find ()) + with + | Sys_error s -> raise Not_found + | End_of_file -> raise Not_found + +let system_getenv name = + try Sys.getenv name with Not_found -> getenv_from_file name + +let getenv_else s dft = try system_getenv s with Not_found -> dft () let safe_getenv warning n = getenv_else n (fun () -> @@ -145,7 +175,7 @@ let coqpath = (** {2 Caml paths} *) -let ocamlfind () = Coq_config.ocamlfind +let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind) (** {1 XDG utilities} *) 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/constr_matching.ml b/pretyping/constr_matching.ml index a3f1c0b004..0e69b814c7 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -528,10 +528,9 @@ let sub_match ?(closed=true) env sigma pat c = let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - begin try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () + begin match Retyping.expand_projection env sigma p c' [] with + | term -> aux env term mk_ctx next + | exception Retyping.RetypeError _ -> next () end | Array(u, t, def, ty) -> let next_mk_ctx = function 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/pretyping/recordops.ml b/pretyping/recordops.ml index b6e44265ae..aa862a912e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref = let lookup_canonical_conversion env (proj,pat) = assoc_pat env pat (GlobRef.Map.find proj !object_table) -let decompose_projection sigma c args = +let rec get_nth n = function +| [] -> raise Not_found +| arg :: args -> + let len = Array.length arg in + if n < len then arg.(n) + else get_nth (n - len) args + +let rec decompose_projection sigma c args = match EConstr.kind sigma c with + | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args + | Cast (c, _, _) -> decompose_projection sigma c args + | App (c, arg) -> decompose_projection sigma c (arg :: args) | Const (c, u) -> let n = find_projection_nparams (GlobRef.ConstRef c) in (* Check if there is some canonical projection attached to this structure *) let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in - let arg = Stack.nth args n in - arg + get_nth n args | Proj (p, c) -> let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in c | _ -> raise Not_found -let is_open_canonical_projection env sigma (c,args) = +let is_open_canonical_projection env sigma c = let open EConstr in try - let arg = decompose_projection sigma c args in + let arg = decompose_projection sigma c [] in try let arg = whd_all env sigma arg in let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 5b8dc8184a..83927085e9 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map -> cs -> unit val subst_canonical_structure : Mod_subst.substitution -> cs -> cs val is_open_canonical_projection : - Environ.env -> Evd.evar_map -> Reductionops.state -> bool + Environ.env -> Evd.evar_map -> EConstr.t -> bool val canonical_projections : unit -> ((GlobRef.t * cs_pattern) * obj_typ) list diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3352bfce38..7a5d0897b5 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -930,14 +930,6 @@ let stack_red_of_state_red f = let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in f -(* Drops the Cst_stack *) -let iterate_whd_gen flags env sigma s = - let rec aux t = - let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in - let whd_sk = Stack.map aux sk in - Stack.zip sigma (hd,whd_sk) - in aux s - let red_of_state_red f env sigma x = Stack.zip sigma (f env sigma (x,Stack.empty)) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index d404a7e414..04dfc5ffe6 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -106,8 +106,6 @@ end (************************************************************************) -type state = constr * constr Stack.t - type reduction_function = env -> evar_map -> constr -> constr type e_reduction_function = env -> evar_map -> constr -> evar_map * constr @@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type stack_reduction_function = env -> evar_map -> constr -> constr * constr list -type state_reduction_function = - env -> evar_map -> state -> state - -val pr_state : env -> evar_map -> state -> Pp.t - (** {6 Reduction Function Operators } *) val strong_with_flags : @@ -127,12 +120,6 @@ val strong_with_flags : (CClosure.RedFlags.reds -> reduction_function) val strong : reduction_function -> reduction_function -val whd_state_gen : - CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state - -val iterate_whd_gen : CClosure.RedFlags.reds -> - Environ.env -> Evd.evar_map -> constr -> constr - (** {6 Generic Optimized Reduction Function using Closures } *) val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function @@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function val whd_allnolet_stack : stack_reduction_function val whd_betalet_stack : stack_reduction_function -val whd_nored_state : state_reduction_function -val whd_beta_state : state_reduction_function -val whd_betaiota_state : state_reduction_function -val whd_betaiotazeta_state : state_reduction_function -val whd_all_state : state_reduction_function -val whd_allnolet_state : state_reduction_function -val whd_betalet_state : state_reduction_function - (** {6 Head normal forms } *) val whd_delta_stack : stack_reduction_function -val whd_delta_state : state_reduction_function val whd_delta : reduction_function val whd_betadeltazeta_stack : stack_reduction_function -val whd_betadeltazeta_state : state_reduction_function val whd_betadeltazeta : reduction_function val whd_zeta_stack : stack_reduction_function -val whd_zeta_state : state_reduction_function val whd_zeta : reduction_function val shrink_eta : Environ.env -> constr -> constr @@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t -> (** {6 Heuristic for Conversion with Evar } *) +type state = constr * constr Stack.t + +type state_reduction_function = + env -> evar_map -> state -> state + +val pr_state : env -> evar_map -> state -> Pp.t + +val whd_nored_state : state_reduction_function + val whd_betaiota_deltazeta_for_iota_state : - TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state + TransparentState.t -> state_reduction_function (** {6 Meta-related reduction functions } *) val meta_instance : env -> evar_map -> constr freelisted -> constr diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 1c24578a1c..3d3010d1a4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp_or_Proj sigma cM then - let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in - if is_open_canonical_projection curenv sigma f1l1 then - let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in - solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn + if is_open_canonical_projection curenv sigma cM then + solve_canonical_projection curenvnb pb opt cM cN substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in @@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e else try f1 () with e when precatchable_exception e -> if isApp_or_Proj sigma cN then - let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in - if is_open_canonical_projection curenv sigma f2l2 then - let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in - solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn + if is_open_canonical_projection curenv sigma cN then + solve_canonical_projection curenvnb pb opt cN cM substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) = + and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) = + let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in + let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) diff --git a/tactics/genredexpr.ml b/tactics/genredexpr.ml index 1f6b04c1d3..9939490e79 100644 --- a/tactics/genredexpr.ml +++ b/tactics/genredexpr.ml @@ -35,13 +35,13 @@ type 'a glob_red_flag = { (** Generic kinds of reductions *) -type ('a,'b,'c) red_expr_gen = +type ('a, 'b, 'c, 'flags) red_expr_gen0 = | Red of bool | Hnf - | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option - | Cbv of 'b glob_red_flag - | Cbn of 'b glob_red_flag - | Lazy of 'b glob_red_flag + | Simpl of 'flags * ('b, 'c) Util.union Locus.with_occurrences option + | Cbv of 'flags + | Cbn of 'flags + | Lazy of 'flags | Unfold of 'b Locus.with_occurrences list | Fold of 'a list | Pattern of 'a Locus.with_occurrences list @@ -49,6 +49,9 @@ type ('a,'b,'c) red_expr_gen = | CbvVm of ('b,'c) Util.union Locus.with_occurrences option | CbvNative of ('b,'c) Util.union Locus.with_occurrences option +type ('a, 'b, 'c) red_expr_gen = + ('a, 'b, 'c, 'b glob_red_flag) red_expr_gen0 + type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index a8747e0a7c..9c2df71f82 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -129,6 +129,9 @@ let set_strategy local str = type red_expr = (constr, evaluable_global_reference, constr_pattern) red_expr_gen +type red_expr_val = + (constr, evaluable_global_reference, constr_pattern, CClosure.RedFlags.reds) red_expr_gen0 + let make_flag_constant = function | EvalVarRef id -> fVAR id | EvalConstRef sp -> fCONST sp @@ -221,38 +224,117 @@ let warn_simpl_unfolding_modifiers = (fun () -> Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.") -let reduction_of_red_expr env = - let make_flag = make_flag env in - let rec reduction_of_red_expr = function +let rec eval_red_expr env = function +| Simpl (f, o) -> + let () = + if not (simplIsCbn () || List.is_empty f.rConst) then + warn_simpl_unfolding_modifiers () in + let f = if simplIsCbn () then make_flag env f else CClosure.all (* dummy *) in + Simpl (f, o) +| Cbv f -> Cbv (make_flag env f) +| Cbn f -> Cbn (make_flag env f) +| Lazy f -> Lazy (make_flag env f) +| ExtraRedExpr s -> + begin match String.Map.find s !red_expr_tab with + | e -> eval_red_expr env e + | exception Not_found -> ExtraRedExpr s (* delay to runtime interpretation *) + end +| (Red _ | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e + +let reduction_of_red_expr_val = function | Red internal -> if internal then (e_red try_red_product,DEFAULTcast) else (e_red red_product,DEFAULTcast) | Hnf -> (e_red hnf_constr,DEFAULTcast) | Simpl (f,o) -> - let whd_am = if simplIsCbn () then whd_cbn (make_flag f) else whd_simpl in - let am = if simplIsCbn () then strong_cbn (make_flag f) else simpl in - let () = - if not (simplIsCbn () || List.is_empty f.rConst) then - warn_simpl_unfolding_modifiers () in + let whd_am = if simplIsCbn () then whd_cbn f else whd_simpl in + let am = if simplIsCbn () then strong_cbn f else simpl in (contextualize (if head_style then whd_am else am) am o,DEFAULTcast) - | Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast) + | Cbv f -> (e_red (cbv_norm_flags f),DEFAULTcast) | Cbn f -> - (e_red (strong_cbn (make_flag f)), DEFAULTcast) - | Lazy f -> (e_red (clos_norm_flags (make_flag f)),DEFAULTcast) + (e_red (strong_cbn f), DEFAULTcast) + | Lazy f -> (e_red (clos_norm_flags f),DEFAULTcast) | Unfold ubinds -> (e_red (unfoldn (List.map out_with_occurrences ubinds)),DEFAULTcast) | Fold cl -> (e_red (fold_commands cl),DEFAULTcast) | Pattern lp -> (pattern_occs (List.map out_with_occurrences lp),DEFAULTcast) | ExtraRedExpr s -> (try (e_red (String.Map.find s !reduction_tab),DEFAULTcast) with Not_found -> - (try reduction_of_red_expr (String.Map.find s !red_expr_tab) - with Not_found -> user_err ~hdr:"Redexpr.reduction_of_red_expr" - (str "unknown user-defined reduction \"" ++ str s ++ str "\""))) + (str "unknown user-defined reduction \"" ++ str s ++ str "\"")) | CbvVm o -> (contextualize cbv_vm cbv_vm o, VMcast) | CbvNative o -> (contextualize cbv_native cbv_native o, NATIVEcast) + +let reduction_of_red_expr env r = + reduction_of_red_expr_val (eval_red_expr env r) + +(* Possibly equip a reduction with the occurrences mentioned in an + occurrence clause *) + +let error_illegal_clause () = + CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.") + +let error_illegal_non_atomic_clause () = + CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.") + +let error_occurrences_not_unsupported () = + CErrors.user_err Pp.(str "Occurrences not supported for this reduction tactic.") + +let bind_red_expr_occurrences occs nbcl redexp = + let open Locus in + let has_at_clause = function + | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l + | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l + | Simpl (_,Some (occl,_)) -> occl != AllOccurrences + | _ -> false in + if occs == AllOccurrences then + if nbcl > 1 && has_at_clause redexp then + error_illegal_non_atomic_clause () + else + redexp + else + match redexp with + | Unfold (_::_::_) -> + error_illegal_clause () + | Unfold [(occl,c)] -> + if occl != AllOccurrences then + error_illegal_clause () + else + Unfold [(occs,c)] + | Pattern (_::_::_) -> + error_illegal_clause () + | Pattern [(occl,c)] -> + if occl != AllOccurrences then + error_illegal_clause () + else + Pattern [(occs,c)] + | Simpl (f,Some (occl,c)) -> + if occl != AllOccurrences then + error_illegal_clause () + else + Simpl (f,Some (occs,c)) + | CbvVm (Some (occl,c)) -> + if occl != AllOccurrences then + error_illegal_clause () + else + CbvVm (Some (occs,c)) + | CbvNative (Some (occl,c)) -> + if occl != AllOccurrences then + error_illegal_clause () + else + CbvNative (Some (occs,c)) + | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ + | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> + error_occurrences_not_unsupported () + | Unfold [] | Pattern [] -> + assert false + +let reduction_of_red_expr_val ?occs r = + let r = match occs with + | None -> r + | Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r in - reduction_of_red_expr + reduction_of_red_expr_val r let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) diff --git a/tactics/redexpr.mli b/tactics/redexpr.mli index d43785218f..5f3a7b689b 100644 --- a/tactics/redexpr.mli +++ b/tactics/redexpr.mli @@ -19,10 +19,18 @@ open Reductionops open Locus type red_expr = - (constr, evaluable_global_reference, constr_pattern) red_expr_gen + (constr, evaluable_global_reference, constr_pattern) red_expr_gen + +type red_expr_val val out_with_occurrences : 'a with_occurrences -> occurrences * 'a +val eval_red_expr : Environ.env -> red_expr -> red_expr_val + +val reduction_of_red_expr_val : ?occs:(Locus.occurrences_expr * int) -> + red_expr_val -> e_reduction_function * cast_kind + +(** Composition of {!reduction_of_red_expr_val} with {!eval_red_expr} *) val reduction_of_red_expr : Environ.env -> red_expr -> e_reduction_function * cast_kind diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5aa31092e9..130e0e97c2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -85,24 +85,6 @@ let () = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* The following boolean governs what "intros []" do on examples such - as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; - if false, it behaves as "intro H; case H; clear H" for fresh H. - Kept as false for compatibility. - *) - -let bracketing_last_or_and_intro_pattern = ref true - -let use_bracketing_last_or_and_intro_pattern () = - !bracketing_last_or_and_intro_pattern - -let () = - declare_bool_option - { optdepr = true; - optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; - optread = (fun () -> !bracketing_last_or_and_intro_pattern); - optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } - (*********************************************) (* Tactics *) (*********************************************) @@ -634,70 +616,10 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where env sigma dec in (sigma, LocalDef (id,b',ty')) -(* Possibly equip a reduction with the occurrences mentioned in an - occurrence clause *) - -let error_illegal_clause () = - error "\"at\" clause not supported in presence of an occurrence clause." - -let error_illegal_non_atomic_clause () = - error "\"at\" clause not supported in presence of a non atomic \"in\" clause." - -let error_occurrences_not_unsupported () = - error "Occurrences not supported for this reduction tactic." - let bind_change_occurrences occs = function | None -> None | Some c -> Some (Redexpr.out_with_occurrences (occs,c)) -let bind_red_expr_occurrences occs nbcl redexp = - let has_at_clause = function - | Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l - | Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l - | Simpl (_,Some (occl,_)) -> occl != AllOccurrences - | _ -> false in - if occs == AllOccurrences then - if nbcl > 1 && has_at_clause redexp then - error_illegal_non_atomic_clause () - else - redexp - else - match redexp with - | Unfold (_::_::_) -> - error_illegal_clause () - | Unfold [(occl,c)] -> - if occl != AllOccurrences then - error_illegal_clause () - else - Unfold [(occs,c)] - | Pattern (_::_::_) -> - error_illegal_clause () - | Pattern [(occl,c)] -> - if occl != AllOccurrences then - error_illegal_clause () - else - Pattern [(occs,c)] - | Simpl (f,Some (occl,c)) -> - if occl != AllOccurrences then - error_illegal_clause () - else - Simpl (f,Some (occs,c)) - | CbvVm (Some (occl,c)) -> - if occl != AllOccurrences then - error_illegal_clause () - else - CbvVm (Some (occs,c)) - | CbvNative (Some (occl,c)) -> - if occl != AllOccurrences then - error_illegal_clause () - else - CbvNative (Some (occs,c)) - | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _ - | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None -> - error_occurrences_not_unsupported () - | Unfold [] | Pattern [] -> - assert false - (* The following two tactics apply an arbitrary reduction function either to the conclusion or to a certain hypothesis *) @@ -959,17 +881,16 @@ let reduce redexp cl = | Red _ | Hnf | CbvVm _ | CbvNative _ -> StableHypConv | ExtraRedExpr _ -> StableHypConv (* Should we be that lenient ?*) in + let redexp = Redexpr.eval_red_expr env redexp in begin match cl.concl_occs with | NoOccurrences -> Proofview.tclUNIT () | occs -> - let redexp = bind_red_expr_occurrences occs nbcl redexp in - let redfun = Redexpr.reduction_of_red_expr env redexp in + let redfun = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in e_change_in_concl ~check (revert_cast redfun) end <*> let f (id, occs, where) = - let redexp = bind_red_expr_occurrences occs nbcl redexp in - let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in + let (redfun, _) = Redexpr.reduction_of_red_expr_val ~occs:(occs, nbcl) redexp in let redfun _ env sigma c = redfun env sigma c in let redfun env sigma d = e_pf_change_decl redfun where env sigma d in (id, redfun) @@ -1083,10 +1004,10 @@ let intros_using_then l tac = intros_using_then_helper tac [] l let intros = Tacticals.New.tclREPEAT intro -let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = +let intro_forthcoming_then_gen name_flag move_flag dep_flag bound n tac = let rec aux n ids = (* Note: we always use the bound when there is one for "*" and "**" *) - if (match bound with None -> true | Some (_,p) -> n < p) then + if (match bound with None -> true | Some p -> n < p) then Proofview.tclORELSE begin intro_then_gen name_flag move_flag false dep_flag @@ -2306,7 +2227,7 @@ let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make () let (forward_subst_one, subst_one) = Hook.make () let error_unexpected_extra_pattern loc bound pat = - let _,nb = Option.get bound in + let nb = Option.get bound in let s1,s2,s3 = match pat with | IntroNaming (IntroIdentifier _) -> "name", (String.plural nb " introduction pattern"), "no" @@ -2339,14 +2260,14 @@ let intro_decomp_eq ?loc l thin tac id = match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) + (fun n -> tac ((CAst.make id)::thin) (Some n) l) (eq,t,eq_args) (c, t) | None -> let info = Exninfo.reify () in Tacticals.New.tclZEROMSG ~info (str "Not a primitive equality here.") end -let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = +let intro_or_and_pattern ?loc with_evars ll thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in let env = Proofview.Goal.env gl in @@ -2360,11 +2281,11 @@ let intro_or_and_pattern ?loc with_evars bracketed ll thin tac id = Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Tacticals.New.tclTHENLASTn (Tacticals.New.tclTHEN (simplest_ecase c) (clear [id])) - (Array.map2 (fun n l -> tac thin (Some (bracketed,n)) l) + (Array.map2 (fun n l -> tac thin (Some n) l) nv_with_let ll)) end -let rewrite_hyp_then assert_style with_evars thin l2r id tac = +let rewrite_hyp_then with_evars thin l2r id tac = let rew_on l2r = Hook.get forward_general_rewrite_clause l2r with_evars (mkVar id,NoBindings) in let subst_on l2r x rhs = @@ -2476,11 +2397,11 @@ let make_tmp_naming avoid l = function let fit_bound n = function | None -> true - | Some (use_bound,n') -> not use_bound || n = n' + | Some n' -> n = n' let exceed_bound n = function | None -> false - | Some (use_bound,n') -> use_bound && n >= n' + | Some n' -> n >= n' (* We delay thinning until the completion of the whole intros tactic to ensure that dependent hypotheses are cleared in the right @@ -2501,60 +2422,59 @@ let exceed_bound n = function [patl]: introduction patterns to interpret *) -let rec intro_patterns_core with_evars b avoid ids thin destopt bound n tac = +let rec intro_patterns_core with_evars avoid ids thin destopt bound n tac = function | [] when fit_bound n bound -> tac ids thin | [] -> (* Behave as IntroAnonymous *) - intro_patterns_core with_evars b avoid ids thin destopt bound n tac + intro_patterns_core with_evars avoid ids thin destopt bound n tac [CAst.make @@ IntroNaming IntroAnonymous] | {CAst.loc;v=pat} :: l -> if exceed_bound n bound then error_unexpected_extra_pattern loc bound pat else match pat with | IntroForthcoming onlydeps -> intro_forthcoming_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) - destopt onlydeps n bound - (fun ids -> intro_patterns_core with_evars b avoid ids thin destopt bound + destopt onlydeps bound n + (fun ids -> intro_patterns_core with_evars avoid ids thin destopt bound (n+List.length ids) tac l) | IntroAction pat -> intro_then_gen (make_tmp_naming avoid l pat) destopt true false - (intro_pattern_action ?loc with_evars (b || not (List.is_empty l)) false - pat thin destopt - (fun thin bound' -> intro_patterns_core with_evars b avoid ids thin destopt bound' 0 + (intro_pattern_action ?loc with_evars pat thin destopt + (fun thin bound' -> intro_patterns_core with_evars avoid ids thin destopt bound' 0 (fun ids thin -> - intro_patterns_core with_evars b avoid ids thin destopt bound (n+1) tac l))) + intro_patterns_core with_evars avoid ids thin destopt bound (n+1) tac l))) | IntroNaming pat -> - intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound (n+1) tac l + intro_pattern_naming loc with_evars avoid ids pat thin destopt bound (n+1) tac l (* Pi-introduction rule, used backwards *) -and intro_pattern_naming loc with_evars b avoid ids pat thin destopt bound n tac l = +and intro_pattern_naming loc with_evars avoid ids pat thin destopt bound n tac l = match pat with | IntroIdentifier id -> check_thin_clash_then id thin avoid (fun thin -> intro_then_gen (NamingMustBe CAst.(make ?loc id)) destopt true false - (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l)) + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l)) | IntroAnonymous -> intro_then_gen (NamingAvoid (Id.Set.union avoid (explicit_intro_names l))) destopt true false - (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) | IntroFresh id -> (* todo: avoid thinned names to interfere with generation of fresh name *) intro_then_gen (NamingBasedOn (id, Id.Set.union avoid (explicit_intro_names l))) destopt true false - (fun id -> intro_patterns_core with_evars b avoid (id::ids) thin destopt bound n tac l) + (fun id -> intro_patterns_core with_evars avoid (id::ids) thin destopt bound n tac l) -and intro_pattern_action ?loc with_evars b style pat thin destopt tac id = +and intro_pattern_action ?loc with_evars pat thin destopt tac id = match pat with | IntroWildcard -> tac (CAst.(make ?loc id)::thin) None [] | IntroOrAndPattern ll -> - intro_or_and_pattern ?loc with_evars b ll thin tac id + intro_or_and_pattern ?loc with_evars ll thin tac id | IntroInjection l' -> intro_decomp_eq ?loc l' thin tac id | IntroRewrite l2r -> - rewrite_hyp_then style with_evars thin l2r id (fun thin -> tac thin None []) + rewrite_hyp_then with_evars thin l2r id (fun thin -> tac thin None []) | IntroApplyOn ({CAst.loc=loc';v=f},{CAst.loc;v=pat}) -> let naming,tac_ipat = prepare_intros ?loc with_evars (IntroIdentifier id) destopt pat in @@ -2575,28 +2495,26 @@ and prepare_intros ?loc with_evars dft destopt = function | IntroAction ipat -> prepare_naming ?loc dft, (let tac thin bound = - intro_patterns_core with_evars true Id.Set.empty [] thin destopt bound 0 + intro_patterns_core with_evars Id.Set.empty [] thin destopt bound 0 (fun _ l -> clear_wildcards l) in fun id -> - intro_pattern_action ?loc with_evars true true ipat [] destopt tac id) + intro_pattern_action ?loc with_evars ipat [] destopt tac id) | IntroForthcoming _ -> user_err ?loc (str "Introduction pattern for one hypothesis expected.") -let intro_patterns_head_core with_evars b destopt bound pat = +let intro_patterns_head_core with_evars destopt bound pat = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in check_name_unicity env [] [] pat; - intro_patterns_core with_evars b Id.Set.empty [] [] destopt + intro_patterns_core with_evars Id.Set.empty [] [] destopt bound 0 (fun _ l -> clear_wildcards l) pat end let intro_patterns_bound_to with_evars n destopt = - intro_patterns_head_core with_evars true destopt - (Some (true,n)) + intro_patterns_head_core with_evars destopt (Some n) let intro_patterns_to with_evars destopt = - intro_patterns_head_core with_evars (use_bracketing_last_or_and_intro_pattern ()) - destopt None + intro_patterns_head_core with_evars destopt None let intro_pattern_to with_evars destopt pat = intro_patterns_to with_evars destopt [CAst.make pat] @@ -3271,7 +3189,7 @@ let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = (intros_move newlstatus) let dest_intro_patterns with_evars avoid thin dest pat tac = - intro_patterns_core with_evars true avoid [] thin dest None 0 tac pat + intro_patterns_core with_evars avoid [] thin dest None 0 tac pat let safe_dest_intro_patterns with_evars avoid thin dest pat tac = Proofview.tclORELSE diff --git a/test-suite/bugs/closed/bug_4787.v b/test-suite/bugs/closed/bug_4787.v deleted file mode 100644 index a1444a4f63..0000000000 --- a/test-suite/bugs/closed/bug_4787.v +++ /dev/null @@ -1,7 +0,0 @@ -(* [Unset Bracketing Last Introduction Pattern] was not working *) - -Unset Bracketing Last Introduction Pattern. - -Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y. -do 10 ((intros [] || intro); simpl); reflexivity. -Qed. diff --git a/test-suite/dune b/test-suite/dune index 6ab2988331..1864153021 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -9,6 +9,10 @@ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ )))) (rule + (targets bin.inc) + (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ )))) + +(rule (targets summary.log) (deps ; File that should be promoted. @@ -44,4 +48,4 @@ ; %{bin:fake_ide} (action (progn - (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) + (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}")))) diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh new file mode 100755 index 0000000000..667d11f89e --- /dev/null +++ b/test-suite/misc/coq_environment.sh @@ -0,0 +1,51 @@ +#!/usr/bin/env bash + +export COQBIN=$BIN +export PATH=$COQBIN:$PATH + +TMP=`mktemp -d` +cd $TMP + +cat > coq_environment.txt <<EOT +# we override COQLIB because we can +COQLIB="$TMP/overridden" # bla bla +OCAMLFIND="$TMP/overridden" +FOOBAR="one more" +EOT + +cp $BIN/coqc . +cp $BIN/coq_makefile . +mkdir -p overridden/tools/ +cp $COQLIB/tools/CoqMakefile.in overridden/tools/ + +unset COQLIB +N=`./coqc -config | grep COQLIB | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by coq_environment + coqc -config + exit 1 +fi +N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo OCAMLFIND not overridden by coq_environment + coqc -config + exit 1 +fi +./coq_makefile -o CoqMakefile -R . foo > /dev/null +N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l` +if [ $N -ne 1 ]; then + echo COQMF_OCAMLFIND not overridden by coq_environment + cat CoqMakefile.conf + exit 1 +fi + +export COQLIB="/overridden2" +N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l` +if [ $N -ne 1 ]; then + echo COQLIB not overridden by COQLIB when coq_environment present + coqc -config + exit 1 +fi + +rm -rf $TMP +exit 0 diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml index afa3deea3a..054a921b93 100644 --- a/test-suite/ocaml_pwd.ml +++ b/test-suite/ocaml_pwd.ml @@ -1,7 +1,26 @@ +open Arg + +let quoted = ref false +let trailing_slash = ref false + +let arguments = [ + "-quoted",Set quoted, "Quote path"; + "-trailing-slash",Set trailing_slash, "End the path with a /"; +] +let subject = ref None +let set_subject x = + if !subject <> None then + failwith "only one path"; + subject := Some x + let _ = - let quoted = Sys.argv.(1) = "-quoted" in - let ch_dir = Sys.argv.(if quoted then 2 else 1) in - Sys.chdir ch_dir; + Arg.parse arguments set_subject "Usage:"; + let subject = + match !subject with + | None -> failwith "no path given"; + | Some x -> x in + Sys.chdir subject; let dir = Sys.getcwd () in - let dir = if quoted then Filename.quote dir else dir in + let dir = if !trailing_slash then dir ^ "/" else dir in + let dir = if !quoted then Filename.quote dir else dir in Format.printf "%s%!" dir 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. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index ef09188c33..8b78f73d2e 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -128,19 +128,37 @@ Proof. elim (Rlt_irrefl _ (Rlt_trans _ _ _ H H2)). Qed. -Lemma exp_ineq1 : forall x:R, 0 < x -> 1 + x < exp x. -Proof. - intros; apply Rplus_lt_reg_l with (- exp 0); rewrite <- (Rplus_comm (exp x)); - assert (H0 := MVT_cor1 exp 0 x derivable_exp H); elim H0; - intros; elim H1; intros; unfold Rminus in H2; rewrite H2; - rewrite Ropp_0; rewrite Rplus_0_r; - replace (derive_pt exp x0 (derivable_exp x0)) with (exp x0). - rewrite exp_0; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; - pattern x at 1; rewrite <- Rmult_1_r; rewrite (Rmult_comm (exp x0)); - apply Rmult_lt_compat_l. - apply H. - rewrite <- exp_0; apply exp_increasing; elim H3; intros; assumption. - symmetry ; apply derive_pt_eq_0; apply derivable_pt_lim_exp. +Lemma exp_ineq1 : forall x : R, x <> 0 -> 1 + x < exp x. +Proof. + assert (Hd : forall c : R, + derivable_pt_lim (fun x : R => exp x - (x + 1)) c (exp c - 1)). + intros. + apply derivable_pt_lim_minus; [apply derivable_pt_lim_exp | ]. + replace (1) with (1 + 0) at 1 by lra. + apply derivable_pt_lim_plus; + [apply derivable_pt_lim_id | apply derivable_pt_lim_const]. + intros x xdz; destruct (Rtotal_order x 0) as [xlz|[xez|xgz]]. + - destruct (MVT_cor2 _ _ x 0 xlz (fun c _ => Hd c)) as [c [HH1 HH2]]. + rewrite exp_0 in HH1. + assert (H1 : 0 < x * exp c - x); [| lra]. + assert (H2 : x * exp 0 < x * exp c); [| rewrite exp_0 in H2; lra]. + apply Rmult_lt_gt_compat_neg_l; auto. + now apply exp_increasing. + - now case xdz. + - destruct (MVT_cor2 _ _ 0 x xgz (fun c _ => Hd c)) as [c [HH1 HH2]]. + rewrite exp_0 in HH1. + assert (H1 : 0 < x * exp c - x); [| lra]. + assert (H2 : x * exp 0 < x * exp c); [| rewrite exp_0 in H2; lra]. + apply Rmult_lt_compat_l; auto. + now apply exp_increasing. +Qed. + +Lemma exp_ineq1_le (x : R) : 1 + x <= exp x. +Proof. + destruct (Req_EM_T x 0) as [xeq|?]. + - rewrite xeq, exp_0; lra. + - left. + now apply exp_ineq1. Qed. Lemma ln_exists1 : forall y:R, 1 <= y -> { z:R | y = exp z }. @@ -159,7 +177,7 @@ Proof. unfold f; apply Rplus_le_reg_l with y; left; apply Rlt_trans with (1 + y). rewrite <- (Rplus_comm y); apply Rplus_lt_compat_l; apply Rlt_0_1. - replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y H0) | ring ]. + replace (y + (exp y - y)) with (exp y); [ apply (exp_ineq1 y); lra | ring ]. unfold f; change (continuity (exp - fct_cte y)); apply continuity_minus; [ apply derivable_continuous; apply derivable_exp diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 0cbfd46e80..07550b67e3 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -216,7 +216,7 @@ let generate_conf_coq_config oc = section oc "Coq configuration."; let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; - fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) + fprintf oc "COQMF_WINDRIVE=%s\n" (windrive (Envars.coqlib())) ;; let generate_conf_files oc |