diff options
Diffstat (limited to 'dev')
-rw-r--r-- | dev/base_include | 2 | ||||
-rw-r--r-- | dev/ci/README.md | 2 | ||||
-rw-r--r-- | dev/ci/ci-basic-overlay.sh | 104 | ||||
-rw-r--r-- | dev/ci/ci-common.sh | 45 | ||||
-rwxr-xr-x | dev/ci/ci-compcert.sh | 2 | ||||
-rwxr-xr-x | dev/ci/ci-iris-lambda-rust.sh | 4 | ||||
-rw-r--r-- | dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh | 4 | ||||
-rw-r--r-- | dev/ci/user-overlays/06535-fix-push-rel-to-named.sh | 4 | ||||
-rw-r--r-- | dev/ci/user-overlays/06686-ccnv-no-proj.sh | 4 | ||||
-rw-r--r-- | dev/db | 95 | ||||
-rw-r--r-- | dev/doc/COMPATIBILITY | 201 | ||||
-rw-r--r-- | dev/doc/changes.md | 11 | ||||
-rw-r--r-- | dev/doc/setup.txt | 24 | ||||
-rw-r--r-- | dev/include | 1 | ||||
-rwxr-xr-x | dev/lint-repository.sh | 13 | ||||
-rw-r--r-- | dev/ocamldebug-coq.run | 2 | ||||
-rw-r--r-- | dev/set_raw_db | 1 | ||||
-rwxr-xr-x | dev/tools/backport-pr.sh | 9 | ||||
-rwxr-xr-x | dev/tools/check-eof-newline.sh | 19 | ||||
-rwxr-xr-x | dev/tools/github-check-prs.py | 47 | ||||
-rwxr-xr-x | dev/tools/merge-pr.sh | 20 | ||||
-rwxr-xr-x | dev/tools/should-check-whitespace.sh | 6 | ||||
-rwxr-xr-x | dev/tools/sudo-apt-get-update.sh | 4 | ||||
-rw-r--r-- | dev/top_printers.ml | 15 | ||||
-rw-r--r-- | dev/top_printers.mli | 173 | ||||
-rw-r--r-- | dev/vm_printers.ml | 2 |
26 files changed, 637 insertions, 177 deletions
diff --git a/dev/base_include b/dev/base_include index 2a4ad4a15..472c0c605 100644 --- a/dev/base_include +++ b/dev/base_include @@ -52,7 +52,7 @@ #install_printer ppvblock;; #install_printer (* bigint *) ppbigint;; #install_printer (* loc *) pploc;; -#install_printer (* substitution *) prsubst;; +#install_printer (* substitution *) ppsubst;; (* Open main files *) diff --git a/dev/ci/README.md b/dev/ci/README.md index f4423558c..bb13587e9 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -103,6 +103,8 @@ The process to merge your PR is then to submit PRs to the external development repositories, merge the latter first (if the fixes are backward-compatible), drop the overlay commit and merge the PR on Coq then. +See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite. + Travis specific information --------------------------- diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 232b8a56e..784da6f97 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -4,141 +4,143 @@ # Maybe we should just use Ruby to have real objects... +# : "${foo:=bar}" sets foo to "bar" if it is unset or null + ######################################################################## # MathComp ######################################################################## -: ${mathcomp_CI_BRANCH:=master} -: ${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git} +: "${mathcomp_CI_BRANCH:=master}" +: "${mathcomp_CI_GITURL:=https://github.com/math-comp/math-comp.git}" ######################################################################## # UniMath ######################################################################## -: ${UniMath_CI_BRANCH:=master} -: ${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git} +: "${UniMath_CI_BRANCH:=master}" +: "${UniMath_CI_GITURL:=https://github.com/UniMath/UniMath.git}" ######################################################################## # Unicoq + Metacoq ######################################################################## -: ${unicoq_CI_BRANCH:=master} -: ${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git} +: "${unicoq_CI_BRANCH:=master}" +: "${unicoq_CI_GITURL:=https://github.com/unicoq/unicoq.git}" -: ${metacoq_CI_BRANCH:=master} -: ${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git} +: "${metacoq_CI_BRANCH:=master}" +: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/MetaCoq.git}" ######################################################################## # Mathclasses + Corn ######################################################################## -: ${math_classes_CI_BRANCH:=master} -: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git} +: "${math_classes_CI_BRANCH:=master}" +: "${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}" -: ${Corn_CI_BRANCH:=master} -: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git} +: "${Corn_CI_BRANCH:=master}" +: "${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}" ######################################################################## # Iris ######################################################################## -: ${stdpp_CI_BRANCH:=master} -: ${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git} +: "${stdpp_CI_BRANCH:=master}" +: "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git}" -: ${Iris_CI_BRANCH:=master} -: ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} +: "${Iris_CI_BRANCH:=master}" +: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git}" -: ${lambdaRust_CI_BRANCH:=master} -: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git} +: "${lambdaRust_CI_BRANCH:=master}" +: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git}" ######################################################################## # HoTT ######################################################################## -: ${HoTT_CI_BRANCH:=master} -: ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} +: "${HoTT_CI_BRANCH:=master}" +: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git}" ######################################################################## # Ltac2 ######################################################################## -: ${ltac2_CI_BRANCH:=master} -: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git} +: "${ltac2_CI_BRANCH:=master}" +: "${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git}" ######################################################################## # GeoCoq ######################################################################## -: ${GeoCoq_CI_BRANCH:=master} -: ${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git} +: "${GeoCoq_CI_BRANCH:=master}" +: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq.git}" ######################################################################## # Flocq ######################################################################## -: ${Flocq_CI_BRANCH:=master} -: ${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git} +: "${Flocq_CI_BRANCH:=master}" +: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}" ######################################################################## # Coquelicot ######################################################################## -: ${Coquelicot_CI_BRANCH:=master} -: ${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git} +: "${Coquelicot_CI_BRANCH:=master}" +: "${Coquelicot_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git}" ######################################################################## # CompCert ######################################################################## -: ${CompCert_CI_BRANCH:=master} -: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} +: "${CompCert_CI_BRANCH:=master}" +: "${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git}" ######################################################################## # VST ######################################################################## -: ${VST_CI_BRANCH:=master} -: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} +: "${VST_CI_BRANCH:=master}" +: "${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git}" ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=master} -: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} +: "${fiat_parsers_CI_BRANCH:=master}" +: "${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git}" ######################################################################## # fiat_crypto ######################################################################## -: ${fiat_crypto_CI_BRANCH:=master} -: ${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git} +: "${fiat_crypto_CI_BRANCH:=master}" +: "${fiat_crypto_CI_GITURL:=https://github.com/mit-plv/fiat-crypto.git}" ######################################################################## # formal-topology ######################################################################## -: ${formal_topology_CI_BRANCH:=ci} -: ${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git} +: "${formal_topology_CI_BRANCH:=ci}" +: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology.git}" ######################################################################## # coq-dpdgraph ######################################################################## -: ${coq_dpdgraph_CI_BRANCH:=coq-trunk} -: ${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git} +: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" +: "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" ######################################################################## # CoLoR ######################################################################## -: ${CoLoR_CI_BRANCH:=master} -: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} +: "${CoLoR_CI_BRANCH:=master}" +: "${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git}" ######################################################################## # SF ######################################################################## -: ${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz} -: ${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz} -: ${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz} +: "${sf_lf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/lf-current/lf.tgz}" +: "${sf_plf_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/plf-current/plf.tgz}" +: "${sf_vfa_CI_TARURL:=https://www.cis.upenn.edu/~bcpierce/sf/vfa-current/vfa.tgz}" ######################################################################## # TLC ######################################################################## -: ${tlc_CI_BRANCH:=master} -: ${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git} +: "${tlc_CI_BRANCH:=master}" +: "${tlc_CI_GITURL:=https://gforge.inria.fr/git/tlc/tlc.git}" ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=master} -: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} +: "${bignums_CI_BRANCH:=master}" +: "${bignums_CI_GITURL:=https://github.com/coq/bignums.git}" ######################################################################## # Equations ######################################################################## -: ${Equations_CI_BRANCH:=8.8+alpha} -: ${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git} +: "${Equations_CI_BRANCH:=8.8+alpha}" +: "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}" diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 58c90ff11..d7a356930 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,9 +2,13 @@ set -xe +# default value for NJOBS +: "${NJOBS:=1}" +export NJOBS + if [ -n "${GITLAB_CI}" ]; then - export COQBIN=`pwd`/_install_ci/bin + export COQBIN="$PWD/_install_ci/bin" export CI_BRANCH="$CI_COMMIT_REF_NAME" else if [ -n "${TRAVIS}" ]; @@ -15,8 +19,10 @@ else then export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER" export CI_BRANCH="$CIRCLE_BRANCH" + else # assume local + export CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)" fi - export COQBIN=`pwd`/bin + export COQBIN="$PWD/bin" fi export PATH="$COQBIN:$PATH" @@ -26,14 +32,16 @@ export COQBIN="$COQBIN/" ls "$COQBIN" # Where we clone and build external developments -CI_BUILD_DIR=`pwd`/_build_ci +CI_BUILD_DIR="$PWD/_build_ci" -for overlay in ${ci_dir}/user-overlays/*.sh; do - source ${overlay} +# shellcheck source=ci-basic-overlay.sh +source "${ci_dir}/ci-basic-overlay.sh" +for overlay in "${ci_dir}"/user-overlays/*.sh; do + # shellcheck source=/dev/null + source "${overlay}" done -source ${ci_dir}/ci-basic-overlay.sh -mathcomp_CI_DIR=${CI_BUILD_DIR}/math-comp +mathcomp_CI_DIR="${CI_BUILD_DIR}/math-comp" # git_checkout branch url dest will create a git repository # in <dest> (if it does not exist already) and checkout the @@ -46,15 +54,16 @@ git_checkout() # Allow an optional 4th argument for the commit local _COMMIT=${4:-FETCH_HEAD} - local _DEPTH=$(if [ -z "${4}" ]; then echo "--depth 1"; fi) - - mkdir -p ${_DEST} - ( cd ${_DEST} && \ - if [ ! -d .git ] ; then git clone ${_DEPTH} ${_URL} . ; fi && \ - echo "Checking out ${_DEST}" && \ - git fetch ${_URL} ${_BRANCH} && \ - git checkout ${_COMMIT} && \ - echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) + local _DEPTH=() + if [ -z "${4}" ]; then _DEPTH=(--depth 1); fi + + mkdir -p "${_DEST}" + ( cd "${_DEST}" && \ + if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ + echo "Checking out ${_DEST}" && \ + git fetch "${_URL}" "${_BRANCH}" && \ + git checkout "${_COMMIT}" && \ + echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } checkout_mathcomp() @@ -79,8 +88,8 @@ install_ssreflect() { echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' - checkout_mathcomp ${mathcomp_CI_DIR} - ( cd ${mathcomp_CI_DIR}/mathcomp && \ + checkout_mathcomp "${mathcomp_CI_DIR}" + ( cd "${mathcomp_CI_DIR}/mathcomp" && \ sed -i.bak '/ssrtest/d' Make && \ sed -i.bak '/odd_order/d' Make && \ sed -i.bak '/all\/all.v/d' Make && \ diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef342..6a0ce2aef 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -5,7 +5,7 @@ source ${ci_dir}/ci-common.sh CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert -opam install -j ${NJOBS} -y menhir +opam install -j "$NJOBS" -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} ( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh index cf24d202d..267e13359 100755 --- a/dev/ci/ci-iris-lambda-rust.sh +++ b/dev/ci/ci-iris-lambda-rust.sh @@ -34,8 +34,8 @@ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_UR # Build std++ ( cd ${stdpp_CI_DIR} && make && make install ) -# Build iris -( cd ${Iris_CI_DIR} && make && make install ) +# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris +( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install ) # Build lambdaRust ( cd ${lambdaRust_CI_DIR} && make && make install ) diff --git a/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh new file mode 100644 index 000000000..78789a6fc --- /dev/null +++ b/dev/ci/user-overlays/06482-ppedrot-check-poly-effects.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6483" ] || [ "$TRAVIS_BRANCH" = "check-poly-effects" ]; then + HoTT_CI_BRANCH=check-poly-effects + HoTT_CI_GITURL=https://github.com/ppedrot/HoTT.git +fi diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh new file mode 100644 index 000000000..8a50fb111 --- /dev/null +++ b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then + Equations_CI_BRANCH=fix-6535 + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations +fi diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh new file mode 100644 index 000000000..3a3ab44e0 --- /dev/null +++ b/dev/ci/user-overlays/06686-ccnv-no-proj.sh @@ -0,0 +1,4 @@ +if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then + Equations_CI_BRANCH=ccnv-fixes + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations +fi @@ -1,37 +1,67 @@ source core.dbg load_printer top_printers.cmo +install_printer Top_printers.pP install_printer Top_printers.ppfuture - install_printer Top_printers.ppid -install_printer Top_printers.ppidset -install_printer Top_printers.ppevar -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppintset install_printer Top_printers.pplab -install_printer Top_printers.ppdir install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir install_printer Top_printers.ppmp -install_printer Top_printers.ppkn install_printer Top_printers.ppcon -install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppproj +install_printer Top_printers.ppkn install_printer Top_printers.ppmind +install_printer Top_printers.ppind install_printer Top_printers.ppsp install_printer Top_printers.ppqualid install_printer Top_printers.ppclindex -install_printer Top_printers.ppbigint -install_printer Top_printers.pp_transparent_state - -install_printer Top_printers.pppattern -install_printer Top_printers.ppglob_constr - +install_printer Top_printers.ppscheme +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof install_printer Top_printers.ppuni -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuni_level install_printer Top_printers.ppuniverse_set install_printer Top_printers.ppuniverse_instance install_printer Top_printers.ppuniverse_context @@ -40,34 +70,19 @@ install_printer Top_printers.ppuniverse_subst install_printer Top_printers.ppuniverse_opt_subst install_printer Top_printers.ppuniverse_level_subst install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future install_printer Top_printers.ppcumulativity_info install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.pptype -install_printer Top_printers.ppj -install_printer Top_printers.ppenv +install_printer Top_printers.ppuniverses install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t - -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.ppproofview -install_printer Top_printers.pphintdb - +install_printer Top_printers.ppenv install_printer Top_printers.pptac install_printer Top_printers.ppobj install_printer Top_printers.pploc -install_printer Top_printers.prsubst -install_printer Top_printers.prdelta -install_printer Top_printers.ppfconstr +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument install_printer Top_printers.ppgenarginfo install_printer Top_printers.ppgenargargt install_printer Top_printers.ppist -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppididmap -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr diff --git a/dev/doc/COMPATIBILITY b/dev/doc/COMPATIBILITY new file mode 100644 index 000000000..a81afca32 --- /dev/null +++ b/dev/doc/COMPATIBILITY @@ -0,0 +1,201 @@ +Note: this file isn't used anymore. Incompatibilities are documented +as part of CHANGES. + +Potential sources of incompatibilities between Coq V8.6 and V8.7 +---------------------------------------------------------------- + +- Extra superfluous names in introduction patterns may now raise an + error rather than a warning when the superfluous name is already in + use. The easy fix is to remove the superfluous name. + +Potential sources of incompatibilities between Coq V8.5 and V8.6 +---------------------------------------------------------------- + +Symptom: An obligation generated by Program or an abstracted subproof +has different arguments. +Cause: Set Shrink Abstract and Set Shrink Obligations are on by default +and the subproof does not use the argument. +Remedy: +- Adapt the script. +- Write an explicit lemma to prove the obligation/subproof and use it + instead (compatible with 8.4). +- Unset the option for the program/proof the obligation/subproof originates + from. + +Symptom: In a goal, order of hypotheses, or absence of an equality of +the form "x = t" or "t = x", or no unfolding of a local definition. +Cause: This might be connected to a number of fixes in the tactic +"subst". The former behavior can be reactivated by issuing "Unset +Regular Subst Tactic". + +Potential sources of incompatibilities between Coq V8.4 and V8.5 +---------------------------------------------------------------- + +* List of typical changes to be done to adapt files from Coq 8.4 * +* to Coq 8.5 when not using compatibility option "-compat 8.4". * + +Symptom: "The reference omega was not found in the current environment". +Cause: "Require Omega" does not import the tactic "omega" any more +Possible solutions: +- use "Require Import OmegaTactic" (not compatible with 8.4) +- use "Require Import Omega" (compatible with 8.4) +- add definition "Ltac omega := Coq.omega.Omega.omega." + +Symptom: "intuition" cannot solve a goal (not working anymore on non standard connective) +Cause: "intuition" had an accidental non uniform behavior fixed on non standard connectives +Possible solutions: +- use "dintuition" instead; it is stronger than "intuition" and works + uniformly on non standard connectives, such as n-ary conjunctions or disjunctions + (not compatible with 8.4) +- do the script differently + +Symptom: The constructor foo (in type bar) expects n arguments. +Cause: parameters must now be given in patterns +Possible solutions: +- use option "Set Asymmetric Patterns" (compatible with 8.4) +- add "_" for the parameters (not compatible with 8.4) +- turn the parameters into implicit arguments (compatible with 8.4) + +Symptom: "NPeano.Nat.foo" not existing anymore +Possible solutions: +- use "Nat.foo" instead + +Symptom: typing problems with proj1_sig or similar +Cause: coercion from sig to sigT and similar coercions have been + removed so as to make the initial state easier to understand for + beginners +Solution: change proj1_sig into projT1 and similarly (compatible with 8.4) + +* Other detailed changes * + +(see also file CHANGES) + +- options for *coq* compilation (see below for ocaml). + +** [-I foo] is now deprecated and will not add directory foo to the + coq load path (only for ocaml, see below). Just replace [-I foo] by + [-Q foo ""] in your project file and re-generate makefile. Or + perform the same operation directly in your makefile if you edit it + by hand. + +** Option -R Foo bar is the same in v8.5 than in v8.4 concerning coq + load path. + +** Option [-I foo -as bar] is unchanged but discouraged unless you + compile ocaml code. Use -Q foo bar instead. + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Command line options for ocaml Compilation of ocaml code (plugins) + +** [-I foo] is *not* deprecated to add foo to the ocaml load path. + +** [-I foo -as bar] adds foo to the ocaml load path *and* adds foo to + the coq load path with logical name bar (shortcut for -I foo -Q foo + bar). + + for more details: file CHANGES or section "Customization at launch + time" of the reference manual. + +- Universe Polymorphism. + +- Refinement, unification and tactics are now aware of universes, + resulting in more localized errors. Universe inconsistencies + should no more get raised at Qed time but during the proof. + Unification *always* produces well-typed substitutions, hence + some rare cases of unifications that succeeded while producing + ill-typed terms before will now fail. + +- The [change p with c] tactic semantics changed, now typechecking + [c] at each matching occurrence [t] of the pattern [p], and + converting [t] with [c]. + +- Template polymorphic inductive types: the partial application + of a template polymorphic type (e.g. list) is not polymorphic. + An explicit parameter application (e.g [fun A => list A]) or + [apply (list _)] will result in a polymorphic instance. + +- The type inference algorithm now takes opacity of constants into + account. This may have effects on tactics using type inference + (e.g. induction). Extra "Transparent" might have to be added to + revert opacity of constants. + +Type classes. + +- When writing an Instance foo : Class A := {| proj := t |} (note the + vertical bars), support for typechecking the projections using the + type information and switching to proof mode is no longer available. + Use { } (without the vertical bars) instead. + +Tactic abstract. + +- Auxiliary lemmas generated by the abstract tactic are removed from + the global environment and inlined in the proof term when a proof + is ended with Qed. The behavior of 8.4 can be obtained by ending + proofs with "Qed exporting" or "Qed exporting ident, .., ident". + +Potential sources of incompatibilities between Coq V8.3 and V8.4 +---------------------------------------------------------------- + +(see also file CHANGES) + +The main known incompatibilities between 8.3 and 8.4 are consequences +of the following changes: + +- The reorganization of the library of numbers: + + Several definitions have new names or are defined in modules of + different names, but a special care has been taken to have this + renaming transparent for the user thanks to compatibility notations. + + However some definitions have changed, what might require some + adaptations. The most noticeable examples are: + - The "?=" notation which now bind to Pos.compare rather than former + Pcompare (now Pos.compare_cont). + - Changes in names may induce different automatically generated + names in proof scripts (e.g. when issuing "destruct Z_le_gt_dec"). + - Z.add has a new definition, hence, applying "simpl" on subterms of + its body might give different results than before. + - BigN.shiftl and BigN.shiftr have reversed arguments order, the + power function in BigN now takes two BigN. + +- Other changes in libraries: + + - The definition of functions over "vectors" (list of fixed length) + have changed. + - TheoryList.v has been removed. + +- Slight changes in tactics: + + - Less unfolding of fixpoints when applying destruct or inversion on + a fixpoint hiding an inductive type (add an extra call to simpl to + preserve compatibility). + - Less unexpected local definitions when applying "destruct" + (incompatibilities solvable by adapting name hypotheses). + - Tactic "apply" might succeed more often, e.g. by now solving + pattern-matching of the form ?f x y = g(x,y) (compatibility + ensured by using "Unset Tactic Pattern Unification"), but also + because it supports (full) betaiota (using "simple apply" might + then help). + - Tactic autorewrite does no longer instantiate pre-existing + existential variables. + - Tactic "info" is now available only for auto, eauto and trivial. + +- Miscellaneous changes: + + - The command "Load" is now atomic for backtracking (use "Unset + Atomic Load" for compatibility). + + +Incompatibilities beyond 8.4... + +- Syntax: "x -> y" has now lower priority than "<->" "A -> B <-> C" is + now "A -> (B <-> C)" + +- Tactics: tauto and intuition no longer accidentally destruct binary + connectives or records other than and, or, prod, sum, iff. In most + of cases, dtauto or dintuition, though stronger than 8.3 tauto and + 8.3 intuition will provide compatibility. + +- "Solve Obligations using" is now "Solve Obligations with". diff --git a/dev/doc/changes.md b/dev/doc/changes.md index e616bd566..aef62b009 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -58,6 +58,17 @@ Declaration of printers for arguments used only in vernac command happen. An alternative is to register the corresponding argument as a value, using "Geninterp.register_val0 wit None". +### STM API + +The STM API has seen a general overhaul. The main change is the +introduction of a "Coq document" type, which all operations now take +as a parameter. This effectively functionalize the STM API and will +allow in the future to handle several documents simultaneously. + +The main remarkable point is that key implicit global parameters such +as load-paths and required modules are now arguments to the document +creation function. This helps enforcing some key invariants. + ### XML IDE Protocol - Before 8.8, `Query` only executed the first command present in the diff --git a/dev/doc/setup.txt b/dev/doc/setup.txt index 26f3d0ddc..0003a2c21 100644 --- a/dev/doc/setup.txt +++ b/dev/doc/setup.txt @@ -58,30 +58,12 @@ behave as expected. A note about rlwrap ------------------- -Running "coqtop" under "rlwrap" is possible, but (on Debian) there is a catch. If you try: - - cd ~/git/coq - rlwrap bin/coqtop - -you will get an error: +When using "rlwrap coqtop" make sure the version of rlwrap is at least +0.42, otherwise you will get rlwrap: error: Couldn't read completions from /usr/share/rlwrap/completions/coqtop: No such file or directory -This is a known issue: - - https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=779692 - -It was fixed upstream in version 0.42, and in a Debian package that, at the time of writing, is not part of Debian stable/testing/sid archives but only of Debian experimental. - - https://packages.debian.org/experimental/rlwrap - -The quick solution is to grab it from there, since it installs fine on Debian stable (jessie). - - cd /tmp - wget http://ftp.us.debian.org/debian/pool/main/r/rlwrap/rlwrap_0.42-1_amd64.deb - sudo dpkg -i rlwrap_0.42-1_amd64.deb - -After that, "rlwrap" works fine with "coqtop". +If this happens either update or use an alternate readline wrapper like "ledit". How to install and configure Merlin (for Emacs) diff --git a/dev/include b/dev/include index 0d34595f4..b982f4c9f 100644 --- a/dev/include +++ b/dev/include @@ -36,7 +36,6 @@ #install_printer (* constraints *) ppconstraints;; #install_printer (* univ constraints *) ppuniverseconstraints;; #install_printer (* universe *) ppuni;; -#install_printer (* universes *) ppuniverse;; #install_printer (* universes *) ppuniverses;; #install_printer (* univ level *) ppuni_level;; #install_printer (* univ context *) ppuniverse_context;; diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index 87a829746..ee9c8777a 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -9,12 +9,12 @@ CODE=0 -if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ]; +if [ -n "${TRAVIS_PULL_REQUEST}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ]; then # skip PRs from before the linter existed if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ]; then - 2>&1 echo "Linting skipped: pull request older than the linter." + 1>&2 echo "Linting skipped: pull request older than the linter." exit 0 fi @@ -22,14 +22,13 @@ then # can still check that they don't worsen. CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*} PR_HEAD=${TRAVIS_COMMIT_RANGE##*...} - MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD) - dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1 + MERGE_BASE=$(git merge-base "$CUR_HEAD" "$PR_HEAD") + dev/lint-commits.sh "$MERGE_BASE" "$PR_HEAD" || CODE=1 fi # Check that the files with 'whitespace' gitattribute end in a newline. # xargs exit status is 123 if any file failed the test -find . "(" -path ./.git -prune ")" -type f \ --o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \ --print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1 +find . "(" -path ./.git -prune ")" -o -type f -print0 | + xargs -0 dev/tools/check-eof-newline.sh || CODE=1 exit $CODE diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3850c05fd..3cbccab44 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -17,7 +17,7 @@ export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ -I $CAMLP4LIB -I +threads \ -I $COQTOP \ - -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ + -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ diff --git a/dev/set_raw_db b/dev/set_raw_db deleted file mode 100644 index 5caff7e5d..000000000 --- a/dev/set_raw_db +++ /dev/null @@ -1 +0,0 @@ -install_printer Top_printers.ppconstrdb diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index d7acf01f1..e4359f703 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -50,6 +50,15 @@ else fi +if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then + echo + read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r + echo + if [[ ! $REPLY =~ ^[Yy]$ ]]; then + exit 1 + fi +fi + if [[ "${OPTION}" == "--stop-before-merging" ]]; then exit 0 fi diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh index 1c578c05c..9e4c8661d 100755 --- a/dev/tools/check-eof-newline.sh +++ b/dev/tools/check-eof-newline.sh @@ -1,9 +1,14 @@ #!/usr/bin/env bash -if [ -z "$(tail -c 1 "$1")" ] -then - exit 0 -else - echo "No newline at end of file $1!" - exit 1 -fi +CODE=0 +for f in "$@"; do + if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \ + git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \ + [ -n "$(tail -c 1 "$f")" ] + then + echo "No newline at end of file $f!" + CODE=1 + fi +done + +exit "$CODE" diff --git a/dev/tools/github-check-prs.py b/dev/tools/github-check-prs.py new file mode 100755 index 000000000..beb26d910 --- /dev/null +++ b/dev/tools/github-check-prs.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python3 + +# Requires PyGithub https://pypi.python.org/pypi/PyGithub, for instance +# debian package: python3-github +# nix: nix-shell -p python3 python3Packages.PyGithub --run ./github-check-rebase.py +from github import Github +import argparse + +REPO = "coq/coq" +REBASE_LABEL="needs: rebase" + +parser = argparse.ArgumentParser() +parser.add_argument("--token-file", type=argparse.FileType('r')) +args = parser.parse_args() + +if args.token_file is None: + token = input("Github access token: ").strip() +else: + token = args.token_file.read().rstrip("\n") + args.token_file.close() + +if token == "": + print ("Warning: using the GitHub API without a token") + print ("We may run into rate limit issues") + g = Github() +else: + g = Github(token) + +repo = g.get_repo(REPO) + +for pull in repo.get_pulls(): + # if conflicts then dirty + # otherwise blocked (because I have no rights) + dirty = pull.mergeable_state == "dirty" + labelled = False + for label in repo.get_issue(pull.number).get_labels(): + if label.name == REBASE_LABEL: + labelled = True + if labelled and not dirty: + print ("PR #" + str(pull.number) + " is not dirty but is labelled") + print ("("+ pull.html_url +")") + elif dirty and not labelled: + print ("PR #" + str(pull.number) + " is dirty and not labelled") + print ("("+ pull.html_url +")") + else: + # give some feedback so the user can see we didn't crash + print ("PR #" + str(pull.number) + " OK") diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index 0c4a79bfd..9f24960ff 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -9,18 +9,18 @@ set -e PR=$1 -CURRENT_LOCAL_BRANCH=`git rev-parse --abbrev-ref HEAD` -REMOTE=`git config --get branch.$CURRENT_LOCAL_BRANCH.remote` -git fetch $REMOTE refs/pull/$PR/head +CURRENT_LOCAL_BRANCH=$(git rev-parse --abbrev-ref HEAD) +REMOTE=$(git config --get "branch.$CURRENT_LOCAL_BRANCH.remote") +git fetch "$REMOTE" "refs/pull/$PR/head" API=https://api.github.com/repos/coq/coq -BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` +BASE_BRANCH=$(curl -s "$API/pulls/$PR" | jq -r '.base.label') -COMMIT=`git rev-parse FETCH_HEAD` -STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` +COMMIT=$(git rev-parse FETCH_HEAD) +STATUS=$(curl -s "$API/commits/$COMMIT/status" | jq -r '.state') -if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then +if [ "$BASE_BRANCH" != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" read -p "Bypass? [y/N] " -n 1 -r echo @@ -30,7 +30,7 @@ if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then fi fi; -if [ $STATUS != "success" ]; then +if [ "$STATUS" != "success" ]; then echo "CI status is \"$STATUS\"" read -p "Bypass? [y/N] " -n 1 -r echo @@ -40,10 +40,10 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: $(curl -s "$API/pulls/$PR" | jq -r '.title')" -e # TODO: improve this check -if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then +if ! git diff --quiet "$REMOTE/$CURRENT_LOCAL_BRANCH" -- dev/ci; then echo "******************************************" echo "** WARNING: does this PR have overlays? **" echo "******************************************" diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh deleted file mode 100755 index d85d65107..000000000 --- a/dev/tools/should-check-whitespace.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/usr/bin/env bash - -# determine if a file has whitespace checking enabled in .gitattributes - -git ls-files --error-unmatch "$1" >/dev/null 2>&1 && -git check-attr whitespace -- "$1" | grep -q -v -e 'unset$' -e 'unspecified$' diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh new file mode 100755 index 000000000..f8bf6bed4 --- /dev/null +++ b/dev/tools/sudo-apt-get-update.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err +! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $? diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ff3825787..af38ce4b8 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -50,13 +50,13 @@ let ppqualid qid = pp(pr_qualid qid) let ppclindex cl = pp(Classops.pr_cl_index cl) let ppscheme k = pp (Ind_tables.pr_scheme_kind k) -let pprecarg = function +let prrecarg = function | Declarations.Norec -> str "Norec" | Declarations.Mrec (mind,i) -> str "Mrec[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" | Declarations.Imbr (mind,i) -> str "Imbr[" ++ MutInd.print mind ++ pr_comma () ++ int i ++ str "]" -let ppwf_paths x = pp (Rtree.pp_tree pprecarg x) +let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) (* term printers *) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma @@ -65,8 +65,6 @@ let ppevar evk = pp (Evar.print evk) let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) let ppeconstr x = pp (Termops.print_constr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) -let ppconstrdb x = pp(Flags.with_option rawdebug Termops.print_constr (EConstr.of_constr x)) -let ppterm = ppconstr let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x)) @@ -111,7 +109,7 @@ let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> - str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") + str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") l open Ltac_pretype let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = @@ -149,8 +147,8 @@ let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) let ppj j = pp (genppj (envpp pr_ljudge_env) j) -let prsubst s = pp (Mod_subst.debug_pr_subst s) -let prdelta s = pp (Mod_subst.debug_pr_delta s) +let ppsubst s = pp (Mod_subst.debug_pr_subst s) +let ppdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) @@ -200,9 +198,8 @@ let pppftreestate p = pp(print_pftreestate p) let pproof p = pp(Proof.pr_proof p) -let ppuni u = pp(pr_uni u) +let ppuni u = pp(Universe.pr u) let ppuni_level u = pp (Level.pr u) -let ppuniverse u = pp (str"[" ++ Universe.pr u ++ str"]") let prlev = Universes.pr_with_global_universes let ppuniverse_set l = pp (LSet.pr prlev l) diff --git a/dev/top_printers.mli b/dev/top_printers.mli new file mode 100644 index 000000000..7b5e4a0b6 --- /dev/null +++ b/dev/top_printers.mli @@ -0,0 +1,173 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Printers for the ocaml toplevel. *) + +val pp : Pp.t -> unit +val pP : Pp.t -> unit (* with surrounding box *) + +val ppfuture : 'a Future.computation -> unit + +val ppid : Names.Id.t -> unit +val pplab : Names.Label.t -> unit +val ppmbid : Names.MBId.t -> unit +val ppdir : Names.DirPath.t -> unit +val ppmp : Names.ModPath.t -> unit +val ppcon : Names.Constant.t -> unit +val ppproj : Names.Projection.t -> unit +val ppkn : Names.KerName.t -> unit +val ppmind : Names.MutInd.t -> unit +val ppind : Names.inductive -> unit + +val ppsp : Libnames.full_path -> unit +val ppqualid : Libnames.qualid -> unit + +val ppclindex : Classops.cl_index -> unit + +val ppscheme : 'a Ind_tables.scheme_kind -> unit + +val prrecarg : Declarations.recarg -> Pp.t +val ppwf_paths : Declarations.recarg Rtree.t -> unit + +val pr_evar : Evar.t -> Pp.t +val ppevar : Evar.t -> unit + +(* Multiple printers for Constr.t *) +val ppconstr : Constr.t -> unit (* by Termops printer *) +val ppconstr_univ : Constr.t -> unit + +(* Extern as type *) +val pptype : Constr.types -> unit + +val ppsconstr : Constr.constr Mod_subst.substituted -> unit +val ppeconstr : EConstr.constr -> unit (* Termops printer *) +val ppconstr_expr : Constrexpr.constr_expr -> unit +val ppglob_constr : 'a Glob_term.glob_constr_g -> unit +val pppattern : Pattern.constr_pattern -> unit +val ppfconstr : CClosure.fconstr -> unit + +val ppbigint : Bigint.bigint -> unit + +val ppintset : Int.Set.t -> unit +val ppidset : Names.Id.Set.t -> unit + +val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t +val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit + +val pridmapgen : 'a Names.Id.Map.t -> Pp.t +val ppidmapgen : 'a Names.Id.Map.t -> unit + +val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t +val ppididmap : Names.Id.t Names.Id.Map.t -> unit + +val prconstrunderbindersidmap : + (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> Pp.t +val ppconstrunderbindersidmap : + (Names.Id.t list * EConstr.constr) Names.Id.Map.t -> unit + +val ppevarsubst : + (Constr.t * Constr.t option * Names.Id.Map.key) list Names.Id.Map.t -> unit + +val ppunbound_ltac_var_map : + 'a Genarg.generic_argument Names.Id.Map.t -> unit + +val pr_closure : Ltac_pretype.closure -> Pp.t +val pr_closed_glob_constr_idmap : + Ltac_pretype.closed_glob_constr Names.Id.Map.t -> Pp.t +val pr_closed_glob_constr : Ltac_pretype.closed_glob_constr -> Pp.t +val ppclosure : Ltac_pretype.closure -> unit +val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit +val ppclosedglobconstridmap : + Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit + +val ppglobal : Globnames.global_reference -> unit + +val ppconst : + Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit +val ppvar : Names.Id.t * Constr.constr -> unit + +val genppj : ('a -> Pp.t * Pp.t) -> 'a -> Pp.t +val ppj : EConstr.unsafe_judgment -> unit + +val ppsubst : Mod_subst.substitution -> unit +val ppdelta : Mod_subst.delta_resolver -> unit + +val pp_idpred : Names.Id.Pred.t -> unit +val pp_cpred : Names.Cpred.t -> unit +val pp_transparent_state : Names.transparent_state -> unit + +val pp_stack_t : Constr.t Reductionops.Stack.t -> unit +val pp_cst_stack_t : Reductionops.Cst_stack.t -> unit +val pp_state_t : Reductionops.state -> unit + +val ppmetas : Evd.Metaset.t -> unit +val ppevm : Evd.evar_map -> unit +val ppevmall : Evd.evar_map -> unit + +val pr_existentialset : Evar.Set.t -> Pp.t +val ppexistentialset : Evar.Set.t -> unit + +val ppexistentialfilter : Evd.Filter.t -> unit + +val ppclenv : Clenv.clausenv -> unit + +val ppgoalgoal : Goal.goal -> unit + +val ppgoal : Proof_type.goal Evd.sigma -> unit +(* also print evar map *) +val ppgoalsigma : Proof_type.goal Evd.sigma -> unit + +val pphintdb : Hints.Hint_db.t -> unit +val ppproofview : Proofview.proofview -> unit +val ppopenconstr : Evd.open_constr -> unit + +val pproof : Proof.t -> unit + +(* Universes *) +val ppuni : Univ.Universe.t -> unit +val ppuni_level : Univ.Level.t -> unit (* raw *) +val prlev : Univ.Level.t -> Pp.t (* with global names (does this work?) *) +val ppuniverse_set : Univ.LSet.t -> unit +val ppuniverse_instance : Univ.Instance.t -> unit +val ppuniverse_context : Univ.UContext.t -> unit +val ppuniverse_context_set : Univ.ContextSet.t -> unit +val ppuniverse_subst : Univ.universe_subst -> unit +val ppuniverse_opt_subst : Universes.universe_opt_subst -> unit +val ppuniverse_level_subst : Univ.universe_level_subst -> unit +val ppevar_universe_context : UState.t -> unit +val ppconstraints : Univ.Constraint.t -> unit +val ppuniverseconstraints : Universes.Constraints.t -> unit +val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit +val ppcumulativity_info : Univ.CumulativityInfo.t -> unit +val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit +val ppuniverses : UGraph.t -> unit + +val ppnamedcontextval : Environ.named_context_val -> unit +val ppenv : Environ.env -> unit +val ppenvwithcst : Environ.env -> unit + +val pptac : Tacexpr.glob_tactic_expr -> unit + +val ppobj : Libobject.obj -> unit + +(* Some super raw printers *) +val cast_kind_display : Constr.cast_kind -> string +val constr_display : Constr.constr -> unit +val print_pure_constr : Constr.types -> unit + +val pploc : Loc.t -> unit + +val pp_argument_type : Genarg.argument_type -> unit +val pp_generic_argument : 'a Genarg.generic_argument -> unit + +val prgenarginfo : Geninterp.Val.t -> Pp.t +val ppgenarginfo : Geninterp.Val.t -> unit + +val ppgenargargt : ('a, 'b, 'c) Genarg.ArgT.tag -> unit + +val ppist : Geninterp.interp_sign -> unit diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 8e43bf6ed..f819d2e6a 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -3,7 +3,7 @@ open Term open Names open Cbytecodes open Cemitcodes -open Vm +open Vmvalues let ppripos (ri,pos) = (match ri with |