diff options
35 files changed, 371 insertions, 268 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 108ecb5a04..f54f64bf28 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -174,20 +174,17 @@ after_script: script: - set -e - echo 'start:coq.test' - - make -f Makefile.ci -j "$NJOBS" ${TEST_TARGET} + - make -f Makefile.ci -j "$NJOBS" "${CI_JOB_NAME#*:}" - echo 'end:coq.test' - set +e dependencies: - build:base - variables: &ci-template-vars - TEST_TARGET: "$CI_JOB_NAME" .ci-template-flambda: &ci-template-flambda <<: *ci-template dependencies: - build:edge+flambda variables: - <<: *ci-template-vars OPAM_SWITCH: "edge" OPAM_VARIANT: "+flambda" @@ -260,6 +257,18 @@ windows32: except: - /^pr-.*$/ +lint: + image: docker:git + stage: test + script: + - apk add bash + - dev/lint-repository.sh + dependencies: [] + before_script: [] + variables: + # we need an unknown amount of history for per-commit linting + GIT_DEPTH: "" + pkg:opam: stage: test # OPAM will build out-of-tree so no point in importing artifacts @@ -445,93 +454,101 @@ validate:edge+flambda: OPAM_SWITCH: edge OPAM_VARIANT: "+flambda" -ci-aac_tactics: - <<: *ci-template +# Libraries are by convention the projects that depend on Coq +# but not on its ML API -ci-bedrock2: +library:ci-bedrock2: <<: *ci-template allow_failure: true -ci-bignums: - <<: *ci-template - -ci-color: +library:ci-color: <<: *ci-template-flambda -ci-compcert: +library:ci-compcert: <<: *ci-template-flambda -ci-coq_dpdgraph: +library:ci-coquelicot: <<: *ci-template -ci-coquelicot: +library:ci-cross-crypto: <<: *ci-template -ci-cross-crypto: +library:ci-fcsl-pcm: <<: *ci-template -ci-elpi: - <<: *ci-template +library:ci-fiat-crypto: + <<: *ci-template-flambda -ci-equations: - <<: *ci-template +library:ci-fiat-crypto-legacy: + <<: *ci-template-flambda -ci-fcsl-pcm: +library:ci-flocq: <<: *ci-template -ci-fiat-crypto: +library:ci-corn: <<: *ci-template-flambda -ci-fiat-crypto-legacy: +library:ci-geocoq: <<: *ci-template-flambda -ci-fiat-parsers: +library:ci-hott: <<: *ci-template -ci-flocq: +library:ci-iris-lambda-rust: + <<: *ci-template-flambda + +library:ci-math-comp: + <<: *ci-template-flambda + +library:ci-sf: <<: *ci-template -ci-formal-topology: +library:ci-unimath: <<: *ci-template-flambda -ci-geocoq: +library:ci-verdi-raft: <<: *ci-template-flambda -ci-coqhammer: +library:ci-vst: + <<: *ci-template-flambda + +# Plugins are by definition the projects that depend on Coq's ML API + +plugin:ci-aac_tactics: <<: *ci-template -ci-hott: +plugin:ci-bignums: <<: *ci-template -ci-iris-lambda-rust: - <<: *ci-template-flambda +plugin:ci-coq_dpdgraph: + <<: *ci-template -ci-ltac2: +plugin:ci-coqhammer: <<: *ci-template -ci-math-comp: - <<: *ci-template-flambda +plugin:ci-elpi: + <<: *ci-template -ci-mtac2: +plugin:ci-equations: <<: *ci-template -ci-paramcoq: +plugin:ci-fiat-parsers: <<: *ci-template -ci-plugin_tutorial: +plugin:ci-ltac2: <<: *ci-template -ci-quickchick: - <<: *ci-template-flambda +plugin:ci-mtac2: + <<: *ci-template -ci-relation-algebra: +plugin:ci-paramcoq: <<: *ci-template -ci-sf: +plugin:ci-plugin_tutorial: <<: *ci-template -ci-unimath: +plugin:ci-quickchick: <<: *ci-template-flambda -ci-vst: - <<: *ci-template-flambda +plugin:ci-relation-algebra: + <<: *ci-template @@ -10,6 +10,7 @@ ## either amend this file and commit it, or contact the coqdev list Abhishek Anand <abhishek.anand.iitg@gmail.com> Abhishek Anand (@brixpro-home) <abhishek.anand.iitg@gmail.com> +Léo Andrès <leo@ndrs.fr> zapashcanon <leo@ndrs.fr> Jim Apple <github.public@jbapple.com> jbapple <github.public@jbapple.com> Bruno Barras <bruno.barras@inria.fr> barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> Bruno Barras <bruno.barras@inria.fr> barras-local <barras-local@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -19,9 +20,11 @@ Yves Bertot <yves.bertot@inria.fr> Yves Bertot <bertot@inria.fr> Yves Bertot <yves.bertot@inria.fr> Yves Bertot <Yves.Bertot@inria.fr> Frédéric Besson <frederic.besson@inria.fr> fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> Siddharth Bhat <siddu.druid@gmail.com> Siddharth <siddu.druid@gmail.com> +Simon Boulier <simon.boulier@ens-rennes.fr> SimonBoulier <simon.boulier@ens-rennes.fr> Pierre Boutillier <pierre.boutillier@ens-lyon.org> pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@ens-lyon.org> Pierre Boutillier <pierre.boutillier@pps.univ-paris-diderot.fr> +Arthur Charguéraud <arthur@chargueraud.org> charguer <arthur@chargueraud.org> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7> Xavier Clerc <xavier.clerc@inria.fr> xclerc <xavier.clerc@inria.fr> Pierre Corbineau <Pierre.Corbineau@NOSPAM@imag.fr> corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -32,6 +35,7 @@ Maxime Dénès <mail@maximedenes.fr> mdenes <mdenes@85f007b7-540 Maxime Dénès <mail@maximedenes.fr> Maxime Denes <maximedenes@gillespie.inria.fr> Olivier Desmettre <desmettr@gforge> desmettr <desmettr@85f007b7-540e-0410-9357-904b9bb8a0f7> Damien Doligez <doligez@gforge> doligez <doligez@85f007b7-540e-0410-9357-904b9bb8a0f7> +İsmail Dönmez <ismail-s@users.noreply.github.com> Ismail <ismail-s@users.noreply.github.com> Andres Erbsen <andreser@mit.edu> Andres Erbsen <andres@kevix.co> Jim Fehrle <jfehrle@sbcglobal.net> Jim <jfehrle@sbcglobal.net> Jean-Christophe Filliâtre <Jean-Christophe.Filliatre@lri.fr> filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -63,11 +67,14 @@ Florent Kirchner <fkirchne@gforge> kirchner <kirchner@85f007b7-5 Johannes Kloos <jkloos@mpi-sws.org> jkloos <jkloos@mpi-sws.org> Matej Košík <matej.kosik@inria.fr> Matej Kosik <m4tej.kosik@gmail.com> Matej Košík <matej.kosik@inria.fr> Matej Kosik <matej.kosik@inria.fr> +Ambroise Lafont <chaster_killer@hotmail.fr> amblaf <you@example.com> +Ambroise Lafont <chaster_killer@hotmail.fr> Ambroise <chaster_killer@hotmail.fr> Vincent Laporte <Vincent.Laporte@fondation-inria.fr> Vincent Laporte <Vincent.Laporte@gmail.com> Marc Lasson <marc.lasson@gmail.com> mlasson <marc.lasson@gmail.com> William Lawvere <mundungus.corleone@gmail.com> william-lawvere <mundungus.corleone@gmail.com> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre Letouzey <pierre.letouzey@inria.fr> letouzey <pierre.letouzey@inria.fr> +Xia Li-yao <lysxia@gmail.com> Lysxia <lysxia@gmail.com> Assia Mahboubi <assia.mahboubi@inria.fr> amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> Evgeny Makarov <emakarov@gforge> emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> Gregory Malecha <gmalecha@eecs.harvard.edu> Gregory Malecha <gmalecha@cs.harvard.edu> @@ -88,6 +95,7 @@ Russell O'Connor <roconnor@blockstream.io> roconnor-blockstream <roconno Christine Paulin <cpaulin@gforge> cpaulin <cpaulin@85f007b7-540e-0410-9357-904b9bb8a0f7> Christine Paulin <cpaulin@gforge> mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> +Frederic Peschanski <frederic.peschanski@lip6.fr> fredokun <frederic.peschanski@lip6.fr> Clément Pit-Claudel <clement.pitclaudel@live.com> Clément Pit--Claudel <clement.pitclaudel@live.com> Loïc Pottier <pottier@gforge> pottier <pottier@85f007b7-540e-0410-9357-904b9bb8a0f7> Matthias Puech <puech@gforge> puech <puech@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -98,6 +106,7 @@ Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> Daniel De Rauglaudre <ddr@g Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> regisgia <regisgia@85f007b7-540e-0410-9357-904b9bb8a0f7> Yann Régis-Gianas <yrg@pps.univ-paris-diderot.fr> Regis-Gianas <yrg@pps.univ-paris-diderot.fr> Clément Renard <clrenard@gforge> clrenard <clrenard@85f007b7-540e-0410-9357-904b9bb8a0f7> +Matthew Ryan <mr_1993@hotmail.co.uk> mrmr1993 <mr_1993@hotmail.co.uk> Claudio Sacerdoti Coen <sacerdot@gforge> sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> Kazuhiko Sakaguchi <pi8027@gmail.com> Kazuhiko Sakaguchi <sakaguchi@coins.tsukuba.ac.jp> Vincent Siles <vsiles@gforge> vsiles <vsiles@85f007b7-540e-0410-9357-904b9bb8a0f7> @@ -108,6 +117,7 @@ Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <matthieu.soz Matthieu Sozeau <mattam@mattam.org> Matthieu Sozeau <mattam@eduroam-prg-sg-1-46-137.net.univ-paris-diderot.fr> Arnaud Spiwack <arnaud@spiwack.net> aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> Paul Steckler <steck@stecksoft.com> Paul Steckler <psteck@mit.edu> +Frank Steffahn <fdsteffahn@gmail.com> staffehn <fdsteffahn@gmail.com> Enrico Tassi <Enrico.Tassi@inria.fr> gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <enrico.tassi@inria.fr> Enrico Tassi <Enrico.Tassi@inria.fr> Enrico Tassi <gares@fettunta.org> @@ -123,5 +133,8 @@ Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> Théo Zimmermann <theo. # Anonymous accounts anonymous < > coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> -anonymous < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> + +# Bot accounts + +cvs2svn < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> +serpyc-bot < > serpyc <serpyc@85f007b7-540e-0410-9357-904b9bb8a0f7> diff --git a/.travis.yml b/.travis.yml index 02b94f4a8e..855d36048d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -28,17 +28,6 @@ env: matrix: include: - - env: - - TEST_TARGET="lint" - install: [] - before_script: [] - addons: - apt: - sources: [] - packages: [] - script: - - dev/lint-repository.sh - - os: osx env: - TEST_TARGET="test-suite" diff --git a/Makefile.ci b/Makefile.ci index 2df6a792b6..84be169f57 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -27,7 +27,6 @@ CI_TARGETS= \ ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ - ci-formal-topology \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -44,6 +43,7 @@ CI_TARGETS= \ ci-simple-io \ ci-tlc \ ci-unimath \ + ci-verdi-raft \ ci-vst .PHONY: ci-all $(CI_TARGETS) @@ -63,8 +63,6 @@ ci-corn: ci-math-classes ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io -ci-formal-topology: ci-corn - # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md index fa8962a06f..6663fbecf8 100644 --- a/dev/ci/README-developers.md +++ b/dev/ci/README-developers.md @@ -10,12 +10,14 @@ We are currently running tests on the following platforms: - GitLab CI is the main CI platform. It tests the compilation of Coq, of the documentation, and of CoqIDE on Linux with several versions of OCaml and with warnings as errors; it runs the test-suite and - tests the compilation of several external developments. + tests the compilation of several external developments. It also runs + a linter that checks whitespace discipline. A [pre-commit + hook](../tools/pre-commit) is automatically installed by + `./configure`. It should allow complying with this discipline + without pain. - Travis CI is used to test the compilation of Coq and run the test-suite on - macOS. It also runs a linter that checks whitespace discipline. A - [pre-commit hook](../tools/pre-commit) is automatically installed by - `./configure`. It should allow complying with this discipline without pain. + macOS. - AppVeyor is used to test the compilation of Coq and run the test-suite on Windows. diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index e0f4f50fa9..e74a7853b9 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -150,13 +150,6 @@ : "${fiat_crypto_CI_ARCHIVEURL:=${fiat_crypto_CI_GITURL}/archive}" ######################################################################## -# formal-topology -######################################################################## -: "${formal_topology_CI_REF:=ci}" -: "${formal_topology_CI_GITURL:=https://github.com/bmsherman/topology}" -: "${formal_topology_CI_ARCHIVEURL:=${formal_topology_CI_GITURL}/archive}" - -######################################################################## # coq_dpdgraph ######################################################################## : "${coq_dpdgraph_CI_REF:=coq-master}" @@ -273,3 +266,26 @@ : "${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}" + +######################################################################## +# 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}" + +: "${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}" + +: "${cheerios_CI_REF:=master}" +: "${cheerios_CI_GITURL:=https://github.com/uwplse/cheerios}" +: "${cheerios_CI_ARCHIVEURL:=${cheerios_CI_GITURL}/archive}" + +: "${verdi_CI_REF:=master}" +: "${verdi_CI_GITURL:=https://github.com/uwplse/verdi}" +: "${verdi_CI_ARCHIVEURL:=${verdi_CI_GITURL}/archive}" + +: "${verdi_raft_CI_REF:=master}" +: "${verdi_raft_CI_GITURL:=https://github.com/uwplse/verdi-raft}" +: "${verdi_raft_CI_ARCHIVEURL:=${verdi_raft_CI_GITURL}/archive}" diff --git a/dev/ci/ci-formal-topology.sh b/dev/ci/ci-formal-topology.sh deleted file mode 100755 index 8be5a06ed2..0000000000 --- a/dev/ci/ci-formal-topology.sh +++ /dev/null @@ -1,8 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download formal_topology - -( cd "${CI_BUILD_DIR}/formal_topology" && make ) diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi-raft.sh new file mode 100755 index 0000000000..3bcd52c464 --- /dev/null +++ b/dev/ci/ci-verdi-raft.sh @@ -0,0 +1,24 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download struct_tact + +( cd "${CI_BUILD_DIR}/struct_tact" && ./configure && make && make install ) + +git_download inf_seq_ext + +( cd "${CI_BUILD_DIR}/inf_seq_ext" && ./configure && make && make install ) + +git_download cheerios + +( cd "${CI_BUILD_DIR}/cheerios" && ./configure && make && make install ) + +git_download verdi + +( cd "${CI_BUILD_DIR}/verdi" && ./configure && make && make install ) + +git_download verdi_raft + +( cd "${CI_BUILD_DIR}/verdi_raft" && ./configure && make ) diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh index cd09b6d305..f588c20d02 100755 --- a/dev/lint-repository.sh +++ b/dev/lint-repository.sh @@ -4,33 +4,25 @@ # lint-commits.sh seeks to prevent the worsening of already present # problems, such as tab indentation in ml files. lint-repository.sh -# seeks to prevent the (re-)introduction of solved problems, such as -# newlines at the end of .v files. +# also seeks to prevent the (re-)introduction of solved problems, such +# as newlines at the end of .v files. CODE=0 -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 - 1>&2 echo "Linting skipped: pull request older than the linter." - exit 0 - fi - - # Some problems are too widespread to fix in one commit, but we - # 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 -fi +# We assume that all merge commits are from the main branch +# For Coq it is extremely rare for this assumption to be broken +read -r base < <(git log -n 1 --merges --pretty='format:%H') +head=$(git rev-parse HEAD) + +dev/lint-commits.sh "$base" "$head" || CODE=1 # Check that the files with 'whitespace' gitattribute end in a newline. # xargs exit status is 123 if any file failed the test +echo Checking end of file newlines find . "(" -path ./.git -prune ")" -o -type f -print0 | xargs -0 dev/tools/check-eof-newline.sh || CODE=1 +echo Checking overlays dev/tools/check-overlays.sh || CODE=1 exit $CODE diff --git a/doc/README.md b/doc/README.md index 3db1261656..c41d269437 100644 --- a/doc/README.md +++ b/doc/README.md @@ -101,18 +101,21 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. -If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 -to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits -upon detecting the first warning. You can set this on the Sphinx `make` -command line or as an environment variable: - -- `make refman SPHINXWARNERROR=0` - -- ~~~ - export SPHINXWARNERROR=0 - ⋮ - make refman - ~~~ +To build the Sphinx documentation without stopping at the first +warning with the legacy Makefile, set `SPHINXWARNERROR` to 0 as such: + +``` +SPHINXWARNERROR=0 make refman-html +``` + +To do the same with the Dune build system, change the value of the +`SPHINXWARNOPT` variable (default is `-W`). The following will build +the Sphinx documentation without stopping at the first warning, and +store all the warnings in the file `/tmp/warn.log`: + +``` +SPHINXWARNOPT="-w/tmp/warn.log" dune build @refman-html +``` Installation ------------ @@ -10,8 +10,10 @@ ; + tools/coqdoc/coqdoc.css (package coq) (source_tree sphinx) - (source_tree tools)) - (action (run sphinx-build -j4 -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (source_tree tools) + (env_var SPHINXWARNOPT)) + (action + (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 7bc5d090b4..95a0039b0a 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -293,9 +293,6 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty -let ids_of_cases_indtype p = - cases_pattern_fold_names Id.Set.add Id.Set.empty p - let ids_of_cases_tomatch tms = List.fold_right (fun (_, ona, indnal) l -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 8c735edfc9..f1a8ed202f 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -113,9 +113,6 @@ val map_constr_expr_with_binders : val replace_vars_constr_expr : Id.t Id.Map.t -> constr_expr -> constr_expr -(** Specific function for interning "in indtype" syntax of "match" *) -val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t - val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0d0b6158d9..444ac5ab6d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -67,10 +67,7 @@ let print_no_symbol = ref false (**********************************************************************) (* Turning notations and scopes on and off for printing *) -module IRuleSet = Set.Make(struct - type t = interp_rule - let compare x y = Pervasives.compare x y - end) +module IRuleSet = InterpRuleSet let inactive_notations_table = Summary.ref ~name:"inactive_notations_table" (IRuleSet.empty) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7aa85a0810..c8c38ffe05 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -573,12 +573,17 @@ let find_fresh_name renaming (terms,termlists,binders,binderlists) avoid id = (* TODO binders *) next_ident_away_from id (fun id -> Id.Set.mem id fvs3) -let is_var store pat = +let is_patvar c = + match DAst.get c with + | PatVar _ -> true + | _ -> false + +let is_patvar_store store pat = match DAst.get pat with | PatVar na -> ignore(store na); true | _ -> false -let out_var pat = +let out_patvar pat = match pat.v with | CPatAtom (Some qid) when qualid_is_ident qid -> Name (qualid_basename qid) @@ -600,7 +605,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let pat = coerce_to_cases_pattern_expr (fst (Id.Map.find id terms)) in let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -610,7 +615,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env = set_env_scopes env scopes in if onlyident then (* Do not try to interpret a variable as a constructor *) - let na = out_var pat in + let na = out_patvar pat in let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else @@ -618,7 +623,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with - | [pat] when is_var store pat -> let na = get () in None, na + | [pat] when is_patvar_store store pat -> let na = get () in None, na | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> @@ -743,7 +748,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in if onlyident then - let na = out_var c in term_of_name na, None + let na = out_patvar c in term_of_name na, None else let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in match disjpat with @@ -805,7 +810,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = (* and since we are only interested in the pattern as a term *) let env = reset_hidden_inductive_implicit_test env in if onlyident then - term_of_name (out_var pat) + term_of_name (out_patvar pat) else let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in match disjpat with @@ -1741,7 +1746,7 @@ let intern_ind_pattern genv ntnvars scopes pat = let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in (with_letin, match product_of_cases_patterns empty_alias idslpl with - | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin) + | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin) | _ -> error_bad_inductive_type ?loc) | x -> error_bad_inductive_type ?loc @@ -1979,30 +1984,30 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = end | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> - Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na) - inb) Id.Set.empty tms in + (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na)) + Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in - let tms,ex_ids,match_from_in = List.fold_right - (fun citm (inds,ex_ids,matchs) -> - let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in - (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs) - tms ([],Id.Set.empty,[]) in + let tms,ex_ids,aliases,match_from_in = List.fold_right + (fun citm (inds,ex_ids,asubst,matchs) -> + let ((tm,ind),extra_id,(ind_ids,alias_subst,match_td)) = + intern_case_item env forbidden_vars citm in + (tm,ind)::inds, + Id.Set.union ind_ids (Option.fold_right Id.Set.add extra_id ex_ids), + merge_subst alias_subst asubst, + List.rev_append match_td matchs) + tms ([],Id.Set.empty,Id.Map.empty,[]) in let env' = Id.Set.fold (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ Name var)) (Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in (* PatVars before a real pattern do not need to be matched *) let stripped_match_from_in = - let is_patvar c = match DAst.get c with - | PatVar _ -> true - | _ -> false - in let rec aux = function | [] -> [] | (_, c) :: q when is_patvar c -> aux q | l -> l in aux match_from_in in + let rtnpo = Option.map (replace_vars_constr_expr aliases) rtnpo in let rtnpo = match stripped_match_from_in with | [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *) | l -> @@ -2150,7 +2155,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (* the "in" part *) let match_td,typ = match t with | Some t -> - let with_letin,(ind,l) = intern_ind_pattern globalenv ntnvars (None,env.scopes) t in + let with_letin,(ind,ind_ids,alias_subst,l) = + intern_ind_pattern globalenv ntnvars (None,env.scopes) t in let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in (* for "in Vect n", we answer (["n","n"],[(loc,"n")]) @@ -2186,9 +2192,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let _,args_rel = List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in canonize_args args_rel l forbidden_names_for_gen [] [] in - match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) + (Id.Set.of_list (List.map (fun id -> id.CAst.v) ind_ids),alias_subst,match_to_do), + Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal)) | None -> - [], None in + (Id.Set.empty,Id.Map.empty,[]), None in (tm',(na.CAst.v, typ)), extra_id, match_td and intern_impargs c env l subscopes args = diff --git a/interp/notation.ml b/interp/notation.ml index b0854de4a3..ca27d439fb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -50,15 +50,25 @@ let notation_entry_level_eq s1 s2 = match (s1,s2) with | InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> String.equal s1 s2 && n1 = n2 | (InConstrEntrySomeLevel | InCustomEntryLevel _), _ -> false +let notation_entry_level_compare s1 s2 = match (s1,s2) with +| InConstrEntrySomeLevel, InConstrEntrySomeLevel -> 0 +| InCustomEntryLevel (s1,n1), InCustomEntryLevel (s2,n2) -> + pair_compare String.compare Int.compare (s1,n1) (s2,n2) +| InConstrEntrySomeLevel, _ -> -1 +| InCustomEntryLevel _, _ -> 1 + let notation_eq (from1,ntn1) (from2,ntn2) = notation_entry_level_eq from1 from2 && String.equal ntn1 ntn2 let pr_notation (from,ntn) = qstring ntn ++ match from with InConstrEntrySomeLevel -> mt () | InCustomEntryLevel (s,n) -> str " in custom " ++ str s +let notation_compare = + pair_compare notation_entry_level_compare String.compare + module NotationOrd = struct type t = notation - let compare = Pervasives.compare + let compare = notation_compare end module NotationSet = Set.Make(NotationOrd) @@ -178,6 +188,17 @@ type scoped_notation_rule_core = scope_name * notation * interpretation * int op type notation_rule_core = interp_rule * interpretation * int option type notation_rule = notation_rule_core * delimiters option * bool +let interp_rule_compare r1 r2 = match r1, r2 with + | NotationRule (sc1,ntn1), NotationRule (sc2,ntn2) -> + pair_compare (Option.compare String.compare) notation_compare (sc1,ntn1) (sc2,ntn2) + | SynDefRule kn1, SynDefRule kn2 -> KerName.compare kn1 kn2 + | (NotationRule _ | SynDefRule _), _ -> -1 + +module InterpRuleSet = Set.Make(struct + type t = interp_rule + let compare = interp_rule_compare + end) + (* Scopes for uninterpretation: includes abbreviations (i.e. syntactic definitions) and *) type uninterp_scope_elem = diff --git a/interp/notation.mli b/interp/notation.mli index 75034cad70..a482e00e81 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -210,6 +210,8 @@ type interp_rule = | NotationRule of scope_name option * notation | SynDefRule of KerName.t +module InterpRuleSet : Set.S with type elt = interp_rule + val declare_notation_interpretation : notation -> scope_name option -> interpretation -> notation_location -> onlyprint:bool -> unit diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1f61bcae2e..196bb16f32 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -374,46 +374,6 @@ let rec stack_args_size = function | Zupdate(_)::s -> stack_args_size s | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 -(* When used as an argument stack (only Zapp can appear) *) -let rec decomp_stack = function - | Zapp v :: s -> - (match Array.length v with - 0 -> decomp_stack s - | 1 -> Some (v.(0), s) - | _ -> - Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None -let array_of_stack s = - let rec stackrec = function - | [] -> [] - | Zapp args :: s -> args :: (stackrec s) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false - in Array.concat (stackrec s) -let rec stack_assign s p c = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then - Zapp args :: stack_assign s (p-q) c - else - (let nargs = Array.copy args in - nargs.(p) <- c; - Zapp nargs :: s) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s -let rec stack_tail p s = - if Int.equal p 0 then s else - match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_tail (p-q) s - else Zapp (Array.sub args p (q-p)) :: s - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> failwith "stack_tail" -let rec stack_nth s p = match s with - | Zapp args :: s -> - let q = Array.length args in - if p >= q then stack_nth s (p-q) - else args.(p) - | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> raise Not_found - (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it when the lift is 0. *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index c2d53eed47..46be1bb279 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -123,8 +123,7 @@ type fterm = (*********************************************************************** s A [stack] is a context of arguments, arguments are pushed by - [append_stack] one array at a time but popped with [decomp_stack] - one by one *) + [append_stack] one array at a time *) type stack_member = | Zapp of fconstr array @@ -139,13 +138,7 @@ and stack = stack_member list val empty_stack : stack val append_stack : fconstr array -> stack -> stack -val decomp_stack : stack -> (fconstr * stack) option -val array_of_stack : stack -> fconstr array -val stack_assign : stack -> int -> fconstr -> stack val stack_args_size : stack -> int -val stack_tail : int -> stack -> stack -val stack_nth : stack -> int -> fconstr -val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack (** To lazy reduce a constr, create a [clos_infos] with diff --git a/lib/util.ml b/lib/util.ml index 38d73d3453..0389336258 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -20,6 +20,12 @@ let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) let on_pi3 f (a,b,c) = (a,b,f c) +(* Comparing pairs *) + +let pair_compare cmpx cmpy (x1,y1 as p1) (x2,y2 as p2) = + if p1 == p2 then 0 else + let c = cmpx x1 x2 in if c == 0 then cmpy y1 y2 else c + (* Projections from triplets *) let pi1 (a,_,_) = a diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..fa3b622621 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,6 +17,10 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b +(** Comparing pairs *) + +val pair_compare : ('a -> 'a -> int) -> ('b -> 'b -> int) -> ('a * 'b -> 'a * 'b -> int) + (** Mapping under triple *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd diff --git a/parsing/cLexer.ml b/parsing/cLexer.ml index c2b7fa117d..49d6cf01d9 100644 --- a/parsing/cLexer.ml +++ b/parsing/cLexer.ml @@ -548,20 +548,27 @@ let process_sequence loc bp c cs = aux 1 cs (* Must be a special token *) -let process_chars loc bp c cs = +let process_chars ~diff_mode loc bp c cs = let t = progress_from_byte loc None (-1) !token_tree cs c in let ep = Stream.count cs in match t with | Some t -> (KEYWORD t, set_loc_pos loc bp ep) | None -> let ep' = bp + utf8_char_size loc cs c in - njunk (ep' - ep) cs; - let loc = set_loc_pos loc bp ep' in - err loc Undefined_token + if diff_mode then begin + let len = ep' - bp in + ignore (store 0 c); + ignore (nstore (len - 1) 1 cs); + IDENT (get_buff len), set_loc_pos loc bp ep + end else begin + njunk (ep' - ep) cs; + let loc = set_loc_pos loc bp ep' in + err loc Undefined_token + end (* Parse what follows a dot *) -let parse_after_dot loc c bp s = match Stream.peek s with +let parse_after_dot ~diff_mode loc c bp s = match Stream.peek s with | Some ('a'..'z' | 'A'..'Z' | '_' as d) -> Stream.junk s; let len = @@ -576,11 +583,11 @@ let parse_after_dot loc c bp s = match Stream.peek s with let len = ident_tail loc (nstore n 0 s) s in let field = get_buff len in (try find_keyword loc ("."^field) s with Not_found -> FIELD field) - | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s) + | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars ~diff_mode loc bp c s) (* Parse what follows a question mark *) -let parse_after_qmark loc bp s = +let parse_after_qmark ~diff_mode loc bp s = match Stream.peek s with | Some ('a'..'z' | 'A'..'Z' | '_') -> LEFTQMARK | None -> KEYWORD "?" @@ -588,7 +595,7 @@ let parse_after_qmark loc bp s = match lookup_utf8 loc s with | Utf8Token (st, _) when Unicode.is_valid_ident_initial st -> LEFTQMARK | AsciiChar | Utf8Token _ | EmptyStream -> - fst (process_chars loc bp '?' s) + fst (process_chars ~diff_mode loc bp '?' s) let blank_or_eof cs = match Stream.peek cs with @@ -598,20 +605,20 @@ let blank_or_eof cs = (* Parse a token in a char stream *) -let rec next_token loc s = +let rec next_token ~diff_mode loc s = let bp = Stream.count s in match Stream.peek s with | Some ('\n' as c) -> Stream.junk s; let ep = Stream.count s in - comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s + comm_loc bp; push_char c; next_token ~diff_mode (bump_loc_line loc ep) s | Some (' ' | '\t' | '\r' as c) -> Stream.junk s; - comm_loc bp; push_char c; next_token loc s + comm_loc bp; push_char c; next_token ~diff_mode loc s | Some ('.' as c) -> Stream.junk s; let t = - try parse_after_dot loc c bp s with + try parse_after_dot ~diff_mode loc c bp s with Stream.Failure -> raise (Stream.Error "") in let ep = Stream.count s in @@ -630,13 +637,13 @@ let rec next_token loc s = Stream.junk s; let t,new_between_commands = if !between_commands then process_sequence loc bp c s, true - else process_chars loc bp c s,false + else process_chars ~diff_mode loc bp c s,false in comment_stop bp; between_commands := new_between_commands; t | Some '?' -> Stream.junk s; let ep = Stream.count s in - let t = parse_after_qmark loc bp s in + let t = parse_after_qmark ~diff_mode loc bp s in comment_stop bp; (t, set_loc_pos loc bp ep) | Some ('a'..'z' | 'A'..'Z' | '_' as c) -> Stream.junk s; @@ -670,12 +677,16 @@ let rec next_token loc s = Stream.junk s; begin try match Stream.peek s with + | Some '*' when diff_mode -> + Stream.junk s; + let ep = Stream.count s in + (IDENT "(*", set_loc_pos loc bp ep) | Some '*' -> Stream.junk s; comm_loc bp; push_string "(*"; - let loc = comment loc bp s in next_token loc s - | _ -> let t = process_chars loc bp c s in comment_stop bp; t + let loc = comment loc bp s in next_token ~diff_mode loc s + | _ -> let t = process_chars ~diff_mode loc bp c s in comment_stop bp; t with Stream.Failure -> raise (Stream.Error "") end | Some ('{' | '}' as c) -> @@ -683,7 +694,7 @@ let rec next_token loc s = let ep = Stream.count s in let t,new_between_commands = if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true - else process_chars loc bp c s, false + else process_chars ~diff_mode loc bp c s, false in comment_stop bp; between_commands := new_between_commands; t | _ -> @@ -695,14 +706,14 @@ let rec next_token loc s = comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep | AsciiChar | Utf8Token _ -> - let t = process_chars loc bp (Stream.next s) s in + let t = process_chars ~diff_mode loc bp (Stream.next s) s in comment_stop bp; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) (* (* Debug: uncomment this for tracing tokens seen by coq...*) -let next_token loc s = - let (t,loc as r) = next_token loc s in +let next_token ~diff_mode loc s = + let (t,loc as r) = next_token ~diff_mode loc s in Printf.eprintf "(line %i, %i-%i)[%s]\n%!" (Ploc.line_nb loc) (Ploc.first_pos loc) (Ploc.last_pos loc) (Tok.to_string t); r *) @@ -743,7 +754,7 @@ let token_text = function | (con, "") -> con | (con, prm) -> con ^ " \"" ^ prm ^ "\"" -let func cs = +let func next_token cs = let loct = loct_create () in let cur_loc = ref (Loc.create !current_file 1 0 0 0) in let ts = @@ -755,8 +766,8 @@ let func cs = in (ts, loct_func loct) -let lexer = { - Plexing.tok_func = func; +let make_lexer ~diff_mode = { + Plexing.tok_func = func (next_token ~diff_mode); Plexing.tok_using = (fun pat -> match Tok.of_pattern pat with | KEYWORD s -> add_keyword s @@ -765,6 +776,8 @@ let lexer = { Plexing.tok_match = Tok.match_pattern; Plexing.tok_text = token_text } +let lexer = make_lexer ~diff_mode:false + (** Terminal symbols interpretation *) let is_ident_not_keyword s = diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index c0ebdd45ef..af3fd7f318 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -56,3 +56,14 @@ val set_lexer_state : lexer_state -> unit val get_lexer_state : unit -> lexer_state val drop_lexer_state : unit -> unit val get_comment_state : lexer_state -> ((int * int) * string) list + +(** Create a lexer. true enables alternate handling for computing diffs. +It ensures that, ignoring white space, the concatenated tokens equal the input +string. Specifically: +- for strings, return the enclosing quotes as tokens and treat the quoted value +as if it was unquoted, possibly becoming multiple tokens +- for comments, return the "(*" as a token and treat the contents of the comment as if +it was not in a comment, possibly becoming multiple tokens +- return any unrecognized Ascii or UTF-8 character as a string +*) +val make_lexer : diff_mode:bool -> Tok.t Gramlib.Plexing.lexer diff --git a/parsing/tok.ml b/parsing/tok.ml index c0d5b6742d..03825e350f 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -40,18 +40,19 @@ let extract_string diff_mode = function | KEYWORD s -> s | IDENT s -> s | STRING s -> - if diff_mode then - let escape_quotes s = - let len = String.length s in - let buf = Buffer.create len in - for i = 0 to len-1 do - let ch = String.get s i in - Buffer.add_char buf ch; - if ch = '"' then Buffer.add_char buf '"' else () - done; - Buffer.contents buf - in - "\"" ^ (escape_quotes s) ^ "\"" else s + if diff_mode then + let escape_quotes s = + let len = String.length s in + let buf = Buffer.create len in + for i = 0 to len-1 do + let ch = String.get s i in + Buffer.add_char buf ch; + if ch = '"' then Buffer.add_char buf '"' else () + done; + Buffer.contents buf + in + "\"" ^ (escape_quotes s) ^ "\"" + else s | PATTERNIDENT s -> s | FIELD s -> if diff_mode then "." ^ s else s | INT s -> s diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index e6e1530e36..ed28cc7725 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -46,15 +46,10 @@ let () = Goptions.(declare_bool_option { (* Functions to deal with impossible cases *) (*******************************************) let impossible_default_case env = - let type_of_id = - let open Names.GlobRef in - match Coqlib.lib_ref "core.IDProp.type" with - | ConstRef c -> c - | VarRef _ | IndRef _ | ConstructRef _ -> assert false - in + let type_of_id = Coqlib.lib_ref "core.IDProp.type" in let c, ctx = UnivGen.fresh_global_instance env (Coqlib.(lib_ref "core.IDProp.idProp")) in - let (_, u) = Constr.destConst c in - Some (c, Constr.mkConstU (type_of_id, u), ctx) + let (_, u) = Constr.destRef c in + Some (c, Constr.mkRef (type_of_id, u), ctx) let coq_unit_judge = let open Environ in diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index b280ce909b..c1ea067567 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -88,7 +88,8 @@ let tokenize_string s = let st = CLexer.get_lexer_state () in try let istr = Stream.of_string s in - let lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in + let lexer = CLexer.make_lexer ~diff_mode:true in + let lex = lexer.Gramlib.Plexing.tok_func istr in let toks = stream_tok [] (fst lex) in CLexer.set_lexer_state st; toks diff --git a/test-suite/bugs/closed/bug_8369.v b/test-suite/bugs/closed/bug_8369.v new file mode 100644 index 0000000000..9816954d0c --- /dev/null +++ b/test-suite/bugs/closed/bug_8369.v @@ -0,0 +1,3 @@ +(* Was failing in master with a not_found generated by the printer *) + +Fail Definition foo := fun '(u, v) p2 => (u, v). diff --git a/test-suite/bugs/closed/bug_9240.v b/test-suite/bugs/closed/bug_9240.v new file mode 100644 index 0000000000..e0901dc2d9 --- /dev/null +++ b/test-suite/bugs/closed/bug_9240.v @@ -0,0 +1,12 @@ +Register unit as core.IDProp.type. +Register tt as core.IDProp.idProp. + + +Inductive vec (A : Type) : nat -> Type := +| nil : vec A 0 +| cons : forall n : nat, A -> vec A n -> vec A (S n). + +Definition hd (A : Type) (n : nat) (v : vec A (S n)) : A := +match v in (vec _ (S n)) return A with +| cons _ _ h _ => h +end. (* assertion failure in evarconv *) diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index cf2d5b2850..14c48e8fa0 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -9,10 +9,11 @@ The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. Instance is not well-typed in the environment of ?x. The command has indeed failed with message: -Cannot infer the domain of the type of f. +Cannot infer ?T in the partial instance "?T -> nat" found for the type of f. The command has indeed failed with message: -Cannot infer the domain of the implicit parameter A of id whose type is -"Type". +Cannot infer ?T in the partial instance "?T -> nat" found for the implicit +parameter A of id whose type is "Type". The command has indeed failed with message: -Cannot infer the codomain of the type of f in environment: +Cannot infer ?T in the partial instance "forall x : nat, ?T" found for the +type of f in environment: x : nat diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index d58e4bf2d6..94016e170b 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +Notation Cn := Foo.FooCn +Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 61206b6dd0..309115848f 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -164,3 +164,20 @@ Open Scope my_scope. Check ##. End H. + +(* Fixing a bug reported by G. Gonthier in #9207 *) + +Module J. + +Module Import Mfoo. +Module Foo. +Definition FooCn := 2. +Module Bar. +Notation Cn := FooCn. +End Bar. +End Foo. +Export Foo.Bar. +End Mfoo. +About Cn. + +End J. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 52fe98ac07..232ac17cbf 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -1873,3 +1873,12 @@ Check match niln in listn O return O=O with niln => eq_refl end. (* (was failing up to May 2017) *) Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end. + +(* A test about binding variables of "in" clause of "match" *) +(* (was failing from 8.5 to Dec 2018) *) + +Check match O in nat return nat with O => O | _ => O end. + +(* Checking that aliases are substituted in the correct order *) + +Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0. diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml index 7f9e6cc6e0..d0b8d21b69 100644 --- a/test-suite/unit-tests/printing/proof_diffs_test.ml +++ b/test-suite/unit-tests/printing/proof_diffs_test.ml @@ -51,23 +51,28 @@ let t () = assert_equal ~msg:"has `Removed" ~printer:string_of_bool true has_removed let _ = add_test "diff_str add/remove" t -(* example of a limitation, not really a test *) -let t () = - try - let _ = diff_str "a" ">" in - assert_failure "unlexable string gives an exception" - with _ -> () -let _ = add_test "diff_str unlexable" t - -(* problematic examples for tokenize_string: - comments omitted - quoted string loses quote marks (are escapes supported/handled?) - char constant split into 2 +(* lexer tweaks: + comments are lexed as multiple tokens + strings tokens include begin/end quotes and embedded "" + single multibyte characters returned even if they're not keywords + + inputs that give a lexer failure (but no use case needs them yet): + ".12" + unterminated string + invalid UTF-8 sequences *) let t () = - List.iter (fun x -> cprintf "'%s' " x) (tokenize_string "(* comment *) \"string\" 'c' xx"); - cprintf "\n" -let _ = add_test "tokenize_string examples" t + let str = "(* comment.field *) ?id () \"str\"\"ing\" \\ := Ж > ∃ 'c' xx" in + let toks = tokenize_string str in + (*List.iter (fun x -> cprintf "'%s' " x) toks;*) + (*cprintf "\n";*) + let str_no_white = String.concat "" (String.split_on_char ' ' str) in + assert_equal ~printer:(fun x -> x) str_no_white (String.concat "" toks); + List.iter (fun s -> + assert_equal ~msg:("'" ^ s ^ "' is a single token") ~printer:string_of_bool true (List.mem s toks)) + [ "(*"; "()"; ":="] + +let _ = add_test "tokenize_string/diff_mode in lexer" t open Pp diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a2b5c8d70a..f3e1e1fc49 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -511,7 +511,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +551,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index b40bccf27e..61540024ef 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -36,7 +36,8 @@ let do_if_not_cached rf f v = let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); - shallow = marshallable } + shallow = false; + } let unfreeze_interp_state { system; proof } = do_if_not_cached s_cache States.unfreeze system; |