diff --git a/.gitignore b/.gitignore index 39c39c189743..829e0075be7c 100644 --- a/.gitignore +++ b/.gitignore @@ -107,6 +107,7 @@ result doc/unreleased.rst doc/refman-html doc/refman-pdf +doc/refman-indices doc/common/version.tex doc/faq/html/ doc/faq/axioms.eps diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index a1a7176caf64..059fa1400653 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -40,8 +40,8 @@ variables: # The $hash is the first 10 characters of the md5 of the Dockerfile. e.g. # echo $(md5sum dev/ci/docker/old_ubuntu_lts/Dockerfile | head -c 10) # echo $(md5sum dev/ci/docker/edge_ubuntu/Dockerfile | head -c 10) - BASE_CACHEKEY: "old_ubuntu_lts-V2026-06-10-d4125f9d9e" - EDGE_CACHEKEY: "edge_ubuntu-V2026-06-10-0c389ac2f4" + BASE_CACHEKEY: "old_ubuntu_lts-v9.3-V2026-07-06-00242ff07f" + EDGE_CACHEKEY: "edge_ubuntu-v9.3-V2026-07-06-62b9804f8c" BASE_IMAGE: "$CI_REGISTRY_IMAGE:$BASE_CACHEKEY" EDGE_IMAGE: "$CI_REGISTRY_IMAGE:$EDGE_CACHEKEY" diff --git a/Makefile b/Makefile index c604a4a5abd4..f50763ef674a 100644 --- a/Makefile +++ b/Makefile @@ -11,7 +11,7 @@ # Dune Makefile for Rocq .PHONY: help help-install states world rocqide watch check # Main developer targets -.PHONY: refman-html refman-pdf corelib-html apidoc # Documentation targets +.PHONY: refman-html refman-pdf refman-indices corelib-html apidoc # Documentation targets .PHONY: test-suite dev-targets .PHONY: fmt ocheck obuild ireport clean # Maintenance targets .PHONY: dunestrap release install # Miscellaneous @@ -63,6 +63,7 @@ help: @echo "" @echo " - refman-html: build Rocq's reference manual [HTML version]" @echo " - refman-pdf: build Rocq's reference manual [PDF version]" + @echo " - refman-indices: build Rocq's JSON indices" @echo " - corelib-html: build Rocq's Corelib documentation [HTML version]" @echo " - apidoc: build ML API documentation" @echo "" @@ -192,6 +193,10 @@ refman-pdf: world doc/unreleased.rst +$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b latex doc/sphinx doc/refman-pdf $(MAKE) -C doc/refman-pdf LATEXMKOPTS=-silent +refman-indices: world doc/unreleased.rst + rm -rf doc/refman-indices + +$(WITHPYPATH) $(WITHJOBS) dune exec -- sphinx-build -q -W -b indices doc/sphinx doc/refman-indices + corelib-html: dunestrap dune build @corelib-html diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 9a49ca14d100..f955c4f651b4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -368,7 +368,7 @@ project atbr 'https://github.com/coq-community/atbr' '1806f95dd68b953312cbee4422 ######################################################################## # metarocq ######################################################################## -project metarocq 'https://github.com/MetaRocq/metarocq' '2d501a9787ff3560f9872340bf0c3628edc58ed4' +project metarocq 'https://github.com/MetaRocq/metarocq' '9242c14bc377611a56d45283977ea754fd499c47' # Contact @mattam82, @yforster on github ######################################################################## diff --git a/dev/ci/docker/edge_ubuntu/Dockerfile b/dev/ci/docker/edge_ubuntu/Dockerfile index 44797ac4e68d..8d0e0697e360 100644 --- a/dev/ci/docker/edge_ubuntu/Dockerfile +++ b/dev/ci/docker/edge_ubuntu/Dockerfile @@ -36,7 +36,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ # More dependencies of the sphinx doc RUN pip3 install --break-system-packages docutils==0.21.2 sphinx==8.2.3 sphinx_rtd_theme==3.0.2 \ - antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==2.6.3 \ + antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==2.6.3 sphinx-markdown-builder==0.6.10 \ && rm -rf ~/.cache/pip # We need to install OPAM 2.0 manually for now. diff --git a/dev/ci/docker/old_ubuntu_lts/Dockerfile b/dev/ci/docker/old_ubuntu_lts/Dockerfile index cf915236ea7e..2626e66b3b01 100644 --- a/dev/ci/docker/old_ubuntu_lts/Dockerfile +++ b/dev/ci/docker/old_ubuntu_lts/Dockerfile @@ -21,7 +21,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ texlive-latex-extra texlive-fonts-recommended texlive-xetex latexmk \ python3-sphinx python3-docutils python3-sphinx-rtd-theme \ python3-antlr4 python3-sphinxcontrib.bibtex \ - python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \ + python3-pip python3-setuptools python3-pexpect python3-bs4 fonts-freefont-otf \ # Dependency of stdlib-doc graphviz \ # Dependencies of source-doc and coq-makefile @@ -34,6 +34,11 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \ python3-venv \ && rm -rf /var/lib/apt/lists /usr/share/doc +# More dependencies of the sphinx doc +RUN pip3 install sphinx-markdown-builder==0.6.10 \ + && rm -rf ~/.cache/pip + + # We need to install OPAM 2.0 manually for now. RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam diff --git a/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh b/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh new file mode 100644 index 000000000000..1931c3015303 --- /dev/null +++ b/dev/ci/user-overlays/22164-JasonGross-print-assumptions-all-flags.sh @@ -0,0 +1 @@ +overlay metarocq https://github.com/JasonGross/metacoq print-assumptions-all-flags 22164 diff --git a/dev/doc/critical-bugs.md b/dev/doc/critical-bugs.md index dae77afd6099..c19a1be0dd35 100644 --- a/dev/doc/critical-bugs.md +++ b/dev/doc/critical-bugs.md @@ -10,7 +10,6 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - [Non fixed bugs](#non-fixed-bugs) - [buffer overflow on large records and closures (infinite loop with OCaml 5)](#buffer-overflow-on-large-records-and-closures-infinite-loop-with-ocaml-5) - [memory corruption by evaluating on ill-typed terms (obtained from unsafe tactics)](#memory-corruption-by-evaluating-on-ill-typed-terms-obtained-from-unsafe-tactics) - - [kernel and checker accept incorrect name aliasing information](#kernel-and-checker-accept-incorrect-name-aliasing-information) - [coqchk checks too little about primitive declarations](#coqchk-checks-too-little-about-primitive-declarations) - [Print Assumptions + Parameter Inline fails to report some inconsistent flags](#print-assumptions-parameter-inline-fails-to-report-some-inconsistent-flags) - [Print Assumptions does not report Unset Universe Checking used during functor application](#print-assumptions-does-not-report-unset-universe-checking-used-during-functor-application) @@ -29,7 +28,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - [guard checker does not check for correct recursive calls when passed as uniform argument in a nested fixpoint](#guard-checker-does-not-check-for-correct-recursive-calls-when-passed-as-uniform-argument-in-a-nested-fixpoint) - [guard checker does not count argument-less recursive calls to compute uniform arguments of a nested mutual fixpoint](#guard-checker-does-not-count-argument-less-recursive-calls-to-compute-uniform-arguments-of-a-nested-mutual-fixpoint) - [guard checker does not check arguments of recursive calls in uniformity analysis](#guard-checker-does-not-check-arguments-of-recursive-calls-in-uniformity-analysis) - - [guard checker sometimes does reduction in the wrong context, accepting wrong fixpoints](#guard-checker-sometimes-does-reduction-in-the-wrong-context-accepting-wrong-fixpoints) + - [guard checker sometimes does reduction in the wrong context accepting wrong fixpoints](#guard-checker-sometimes-does-reduction-in-the-wrong-context-accepting-wrong-fixpoints) - [guard checker sometimes forgets to check lambda domains in nested fixpoints](#guard-checker-sometimes-forgets-to-check-lambda-domains-in-nested-fixpoints) - [Module system](#module-system) - [missing universe constraints in typing "with" clause of a module type](#missing-universe-constraints-in-typing-with-clause-of-a-module-type) @@ -41,6 +40,7 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - [Missing substitution when strengthening aliased functors](#missing-substitution-when-strengthening-aliased-functors) - [Incorrect subtyping rule for universe polymorphic "with Definition".](#incorrect-subtyping-rule-for-universe-polymorphic-with-definition) - [Subtyping ignored elimination constraints](#subtyping-ignored-elimination-constraints) + - [kernel and checker accept incorrect name aliasing information](#kernel-and-checker-accept-incorrect-name-aliasing-information) - [Universes](#universes) - [issue with two parameters in the same universe level](#issue-with-two-parameters-in-the-same-universe-level) - [universe polymorphism can capture global universes](#universe-polymorphism-can-capture-global-universes) @@ -125,18 +125,6 @@ This file recollects knowledge about critical bugs found in Coq since version 8. - risk: could be activated by chance but unlikely to produce anything other than SIGSEV outside a deliberate attack -#### kernel and checker accept incorrect name aliasing information - -- component: name handling / typechecker -- introduced: a long time ago -- impacted versions: -NOW -- impacted coqchk versions: same -- fixed in: NONE -- found by: Pierre-Marie Pédrot -- GH issue number: rocq-prover/rocq#7609 -- exploit: see issue (requires a plugin or hand crafted .vo file) -- risk: low - #### coqchk checks too little about primitive declarations - component: primitive types and operators @@ -459,6 +447,18 @@ and lack of checking of relevance marks on constants in coqchk - risk: high when combining module subyping with sort polymorphism (but not possible in non-rc version) +#### kernel and checker accept incorrect name aliasing information + +- component: name handling / typechecker +- introduced: a long time ago +- impacted versions: until 9.2.0 +- impacted coqchk versions: same +- fixed in: 9.2.0 +- found by: Pierre-Marie Pédrot +- GH issue number: rocq-prover/rocq#7609 +- exploit: see issue (requires a plugin or hand crafted .vo file) +- risk: low + ### Universes #### issue with two parameters in the same universe level diff --git a/doc/README.md b/doc/README.md index ee32e0e56cf9..aaf5ebc8848d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -36,12 +36,14 @@ reference manual requires Python 3, and the following Python packages: - antlr4-python3-runtime >= 4.7.1 & <= 4.9.3 - pexpect >= 4.8.0 - sphinxcontrib-bibtex >= 2.4.2 + - sphinx-markdown-builder >= 0.6.10 To install them, you should first install pip and setuptools (for instance, with `apt install python3-pip python3-setuptools` on Debian / Ubuntu) then run: pip3 install sphinx sphinx_rtd_theme beautifulsoup4 \ - antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex + antlr4-python3-runtime==4.7.1 pexpect sphinxcontrib-bibtex \ + sphinx-markdown-builder==0.6.10 Nix users should get the correct development environment to build the HTML documentation from Coq's [`default.nix`](../default.nix) (note this @@ -71,6 +73,71 @@ Or if you want to use less disk space: apt install texlive-latex-extra texlive-fonts-recommended texlive-xetex \ latexmk fonts-freefont-otf +### JSON indices + +The documentation generator can also produce computer-readable JSON files for individual indices +with `make refman-indices`. These files are meant to be useful for tool developers, for instance +to power autocompletion in editors. They output files are found in `doc/refman-indices/*.json`. + +Each JSON index has the following shape: + +```typescript +{ + // a key is the name of the index entry + [string]: { + // the refman documentation page path for that entry + "documentation_path": string. + // the anchor on that page that leads to the documentation entry + "documentation_anchor": string, + // the grammar description + "syntax": Syntax, + // a simpler, markdown documentation + "documentation": string, + } +} +``` + +Where `Syntax` can be used to match some text against the index entry or to propose the +user a code snippet. It is of the following shape: + +```ts +type Syntax = + | ["Literal", Literal] + | ["Reference", Reference] + | ["Alternative", Alternative] + | ["Repeat", Repeat] + +// the literal string +type Literal = { + value: string + // an optional subscript, for example "1" which should be rendered as "₁" + subscript: string | null +} + +// a reference to a different entry in the documentation +type Reference = { + value: string + // an optional subscript, for example "1" which should be rendered as "₁" + subscript: string | null +} + +// an alternative between a list of options +type Alternative = { + children: Syntax[] +} + +// repetition of a list of syntax nodes +type Repeat = { + // nodes have to repeat at least this many times + min: number + // nodes can repeat up to and including this many times + max: number | null + // each repetition has to be separated with this + separator: string | null + children: Syntax[] +} +``` + ### Setting the locale for Python Make sure that the locale is configured on your platform so that Python encodes @@ -106,6 +173,9 @@ The current documentation targets are: - `make corelib-html` Build Rocq core library documentation into `_build/default/doc/corelib/html` +- `make refman-indices` + Build the JSON indices into `doc/refman-indices` + - `make apidoc` Build the ML API's documentation into `_build/default/_doc/_html` diff --git a/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst b/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst new file mode 100644 index 000000000000..ac80a1ad7fea --- /dev/null +++ b/doc/changelog/04-tactics/22251-underp-proof-with-Changed.rst @@ -0,0 +1,4 @@ +- **Changed:** + `...` (:cmd:`Proof with`) is not deprecated anymore and is expected to remain available + (`#22251 `_, + by Gaëtan Gilbert). diff --git a/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst b/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst new file mode 100644 index 000000000000..bb44bfee1da3 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22164-print-assumptions-all-flags-Added.rst @@ -0,0 +1,7 @@ +- **Added:** + ``Printing All Assumptions`` flag making :cmd:`Print Assumptions` report + theory assumptions (impredicativity of :g:`Set`, rewrite rules, disabled + universe checking, indices not mattering) according to each definition's + typing flags in addition to the settings of the current environment + (`#22164 `_, + by Jason Gross). diff --git a/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst b/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst new file mode 100644 index 000000000000..cf743b1d9596 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22231-coqdep-warn-loc-Changed.rst @@ -0,0 +1,5 @@ +- **Changed:** + `rocq dep` errors have more readable locations, and warnings have locations + (`#22231 `_, + fixes `#10815 `_, + by Gaëtan Gilbert). diff --git a/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst b/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst new file mode 100644 index 000000000000..636a22f0deae --- /dev/null +++ b/doc/changelog/11-corelib/22221-template-scheme-univs-Fixed.rst @@ -0,0 +1,13 @@ +- **Fixed:** + Rewriting schemes over template polymorphic inductive types + (generated by :cmd:`Scheme` ``Rewriting``, or on the fly by tactics + such as :tacn:`rewrite` on user-defined equality types) no longer + mention the global template universes in their types. In + particular, the types of ``eq_sym``, ``eq_sym_involutive`` and + ``eq_rew_r_dep`` now use a universe local to the scheme instead of + ``eq.u0``, so that using these constants no longer adds constraints + on ``eq.u0`` (which is deprecated, see the ``bad-template-constraint`` + warning) + (`#22221 `_, + fixes `#22220 `_, + by Jason Gross). diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 2d32b1cde61a..a7c9dafe0a1c 100644 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -60,6 +60,7 @@ 'sphinx.ext.mathjax', 'sphinx.ext.todo', 'sphinxcontrib.bibtex', + 'sphinx_markdown_builder', 'rocqrst.rocqdomain' ] @@ -211,9 +212,10 @@ def setup(app): 'versions': [ ("dev", "https://rocq-prover.org/doc/master/refman/"), ("stable", "https://rocq-prover.org/refman/"), - ("9.2", "https://rocq-prover.org/doc/v9.2/refman/"), - ("9.1", "https://rocq-prover.org/doc/v9.1/refman/"), - ("9.0", "https://rocq-prover.org/doc/v9.0/refman/"), + ("9.3", "https://rocq-prover.org/doc/v9.3/refman/"), + ("9.2", "https://rocq-prover.org/doc/V9.2.0/refman/"), + ("9.1", "https://rocq-prover.org/doc/V9.1.1/refman/"), + ("9.0", "https://rocq-prover.org/doc/V9.0.1/refman/"), ("8.20", "https://rocq-prover.org/doc/V8.20.1/refman/"), ("8.19", "https://rocq-prover.org/doc/V8.19.2/refman/"), ("8.18", "https://rocq-prover.org/doc/V8.18.0/refman/"), diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index d5b550ed6786..5d990b2bd188 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -454,6 +454,21 @@ Requests to the environment The message "Closed under the global context" indicates that all the theorems and definitions have no dependencies. +.. flag:: Printing All Assumptions + + Turn this :term:`flag` on to make :cmd:`Print Assumptions` report + theory assumptions (impredicativity of :g:`Set`, rewrite rules, + disabled universe checking, indices not mattering) according to the + typing flags each dependency was typechecked with, in addition to + the settings of the current environment. For instance, a definition + typechecked with ``-impredicative-set`` is reported as assuming the + impredicativity of :g:`Set` even when it is imported into a + predicative environment, and an inductive type relying on indices + not mattering is reported even when :flag:`Indices Matter` is off in + the current environment (without this flag, such inductive types are + reported only when :flag:`Indices Matter` is currently on, since an + environment where indices do not matter subsumes that assumption). + .. cmd:: Print Opaque Dependencies {+ @reference } Displays the assumptions and opaque constants that :n:`@reference` depends on. diff --git a/doc/tools/rocqrst/notations/TacticNotations.g b/doc/tools/rocqrst/notations/TacticNotations.g index ef6b633173a6..446fae0ecef5 100644 --- a/doc/tools/rocqrst/notations/TacticNotations.g +++ b/doc/tools/rocqrst/notations/TacticNotations.g @@ -46,7 +46,7 @@ RBRACE: '}'; ESCAPED: '%{' | '%}' | '%|' | '`%{' | '@%{' | '%|-' | '%|->' | '%||' | '%|||' | '%||||'; // for SSR PIPE: '|'; -ATOM: '@' | '_' | ~[@_{}| ]+; +ATOM: '@' | '_' | ~[@_{}| ]+ ('_' ~[@_{}| ]+)*; ID: '@' ('_'? [a-zA-Z0-9])+; SUB: '_' '_' [a-zA-Z0-9]+; WHITESPACE: ' '+; diff --git a/doc/tools/rocqrst/notations/TacticNotationsLexer.py b/doc/tools/rocqrst/notations/TacticNotationsLexer.py index f143a87a4965..ce455af5488e 100644 --- a/doc/tools/rocqrst/notations/TacticNotationsLexer.py +++ b/doc/tools/rocqrst/notations/TacticNotationsLexer.py @@ -8,21 +8,22 @@ def serializedATN(): with StringIO() as buf: buf.write("\3\u608b\ua72a\u8133\ub9ed\u417c\u3be7\u7786\u5964\2\f") - buf.write("f\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") + buf.write("q\b\1\4\2\t\2\4\3\t\3\4\4\t\4\4\5\t\5\4\6\t\6\4\7\t\7") buf.write("\4\b\t\b\4\t\t\t\4\n\t\n\4\13\t\13\3\2\3\2\3\2\3\3\3\3") buf.write("\3\3\3\3\3\3\3\3\5\3!\n\3\3\4\3\4\3\5\3\5\3\6\3\6\3\6") buf.write("\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3") buf.write("\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6\3\6") - buf.write("\3\6\5\6F\n\6\3\7\3\7\3\b\3\b\6\bL\n\b\r\b\16\bM\5\bP") - buf.write("\n\b\3\t\3\t\5\tT\n\t\3\t\6\tW\n\t\r\t\16\tX\3\n\3\n\3") - buf.write("\n\6\n^\n\n\r\n\16\n_\3\13\6\13c\n\13\r\13\16\13d\2\2") - buf.write("\f\3\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5") - buf.write("\4\2BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2v\2\3\3\2\2\2") + buf.write("\3\6\5\6F\n\6\3\7\3\7\3\b\3\b\6\bL\n\b\r\b\16\bM\3\b\3") + buf.write("\b\6\bR\n\b\r\b\16\bS\7\bV\n\b\f\b\16\bY\13\b\5\b[\n\b") + buf.write("\3\t\3\t\5\t_\n\t\3\t\6\tb\n\t\r\t\16\tc\3\n\3\n\3\n\6") + buf.write("\ni\n\n\r\n\16\nj\3\13\6\13n\n\13\r\13\16\13o\2\2\f\3") + buf.write("\3\5\4\7\5\t\6\13\7\r\b\17\t\21\n\23\13\25\f\3\2\5\4\2") + buf.write("BBaa\6\2\"\"BBaa}\177\5\2\62;C\\c|\2\u0083\2\3\3\2\2\2") buf.write("\2\5\3\2\2\2\2\7\3\2\2\2\2\t\3\2\2\2\2\13\3\2\2\2\2\r") buf.write("\3\2\2\2\2\17\3\2\2\2\2\21\3\2\2\2\2\23\3\2\2\2\2\25\3") buf.write("\2\2\2\3\27\3\2\2\2\5 \3\2\2\2\7\"\3\2\2\2\t$\3\2\2\2") - buf.write("\13E\3\2\2\2\rG\3\2\2\2\17O\3\2\2\2\21Q\3\2\2\2\23Z\3") - buf.write("\2\2\2\25b\3\2\2\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2") + buf.write("\13E\3\2\2\2\rG\3\2\2\2\17Z\3\2\2\2\21\\\3\2\2\2\23e\3") + buf.write("\2\2\2\25m\3\2\2\2\27\30\7}\2\2\30\31\7~\2\2\31\4\3\2") buf.write("\2\2\32\33\7}\2\2\33!\7-\2\2\34\35\7}\2\2\35!\7,\2\2\36") buf.write("\37\7}\2\2\37!\7A\2\2 \32\3\2\2\2 \34\3\2\2\2 \36\3\2") buf.write("\2\2!\6\3\2\2\2\"#\7}\2\2#\b\3\2\2\2$%\7\177\2\2%\n\3") @@ -34,14 +35,16 @@ def serializedATN(): buf.write("~\2\2?F\7~\2\2@A\7\'\2\2AB\7~\2\2BC\7~\2\2CD\7~\2\2DF") buf.write("\7~\2\2E&\3\2\2\2E(\3\2\2\2E*\3\2\2\2E,\3\2\2\2E/\3\2") buf.write("\2\2E\62\3\2\2\2E\65\3\2\2\2E9\3\2\2\2E<\3\2\2\2E@\3\2") - buf.write("\2\2F\f\3\2\2\2GH\7~\2\2H\16\3\2\2\2IP\t\2\2\2JL\n\3\2") - buf.write("\2KJ\3\2\2\2LM\3\2\2\2MK\3\2\2\2MN\3\2\2\2NP\3\2\2\2O") - buf.write("I\3\2\2\2OK\3\2\2\2P\20\3\2\2\2QV\7B\2\2RT\7a\2\2SR\3") - buf.write("\2\2\2ST\3\2\2\2TU\3\2\2\2UW\t\4\2\2VS\3\2\2\2WX\3\2\2") - buf.write("\2XV\3\2\2\2XY\3\2\2\2Y\22\3\2\2\2Z[\7a\2\2[]\7a\2\2\\") - buf.write("^\t\4\2\2]\\\3\2\2\2^_\3\2\2\2_]\3\2\2\2_`\3\2\2\2`\24") - buf.write("\3\2\2\2ac\7\"\2\2ba\3\2\2\2cd\3\2\2\2db\3\2\2\2de\3\2") - buf.write("\2\2e\26\3\2\2\2\13\2 EMOSX_d\2") + buf.write("\2\2F\f\3\2\2\2GH\7~\2\2H\16\3\2\2\2I[\t\2\2\2JL\n\3\2") + buf.write("\2KJ\3\2\2\2LM\3\2\2\2MK\3\2\2\2MN\3\2\2\2NW\3\2\2\2O") + buf.write("Q\7a\2\2PR\n\3\2\2QP\3\2\2\2RS\3\2\2\2SQ\3\2\2\2ST\3\2") + buf.write("\2\2TV\3\2\2\2UO\3\2\2\2VY\3\2\2\2WU\3\2\2\2WX\3\2\2\2") + buf.write("X[\3\2\2\2YW\3\2\2\2ZI\3\2\2\2ZK\3\2\2\2[\20\3\2\2\2\\") + buf.write("a\7B\2\2]_\7a\2\2^]\3\2\2\2^_\3\2\2\2_`\3\2\2\2`b\t\4") + buf.write("\2\2a^\3\2\2\2bc\3\2\2\2ca\3\2\2\2cd\3\2\2\2d\22\3\2\2") + buf.write("\2ef\7a\2\2fh\7a\2\2gi\t\4\2\2hg\3\2\2\2ij\3\2\2\2jh\3") + buf.write("\2\2\2jk\3\2\2\2k\24\3\2\2\2ln\7\"\2\2ml\3\2\2\2no\3\2") + buf.write("\2\2om\3\2\2\2op\3\2\2\2p\26\3\2\2\2\r\2 EMSWZ^cjo\2") return buf.getvalue() diff --git a/doc/tools/rocqrst/notations/object.py b/doc/tools/rocqrst/notations/object.py new file mode 100644 index 000000000000..e5d591a4d903 --- /dev/null +++ b/doc/tools/rocqrst/notations/object.py @@ -0,0 +1,126 @@ +from dataclasses import asdict, dataclass +from typing import TypeVar + +from .parsing import parse +from .TacticNotationsParser import TacticNotationsParser +from .TacticNotationsVisitor import TacticNotationsVisitor + + +class NotationObject: + def asdict(self): + return asdict(self) + +TaggedNotationObject = tuple[str, NotationObject] + +SelfLiteral = TypeVar("Self", bound="Literal") +@dataclass +class Literal(NotationObject): + value: str + subscript: str | None + @classmethod + def new(cls, value: SelfLiteral) -> tuple[str, SelfLiteral]: + return ("Literal", value) + +SelfReference = TypeVar("Self", bound="Reference") +@dataclass +class Reference(NotationObject): + value: str + subscript: str | None + @classmethod + def new(cls, value: SelfReference) -> tuple[str, SelfReference]: + return ("Reference", value) + +SelfAlternative = TypeVar("Self", bound="Alternative") +@dataclass +class Alternative(NotationObject): + children: list[TaggedNotationObject] + @classmethod + def new(cls, value: SelfAlternative) -> tuple[str, SelfAlternative]: + return ("Alternative", value) + +SelfRepeat = TypeVar("Self", bound="Repeat") +@dataclass +class Repeat(NotationObject): + min: int + max: int | None + separator: str | None + children: list[TaggedNotationObject] + @classmethod + def new(cls, value: SelfRepeat) -> tuple[str, SelfRepeat]: + return ("Repeat", value) + +class TacticNotationsToObjectVisitor(TacticNotationsVisitor): + def defaultResult(self): + return [] + + def aggregateResult(self, aggregate, nextResult): + # Flattening results into a single list of nodes + if nextResult: + if isinstance(nextResult, list): + aggregate.extend(nextResult) + else: + aggregate.append(nextResult) + return aggregate + + def visitAlternative(self, ctx: TacticNotationsParser.AlternativeContext): + return [Alternative.new(Alternative(children=self.visitChildren(ctx)))] + + def visitAltblock(self, ctx: TacticNotationsParser.AltblockContext): + return self.visitChildren(ctx) + + def visitRepeat(self, ctx: TacticNotationsParser.RepeatContext): + separator = ctx.ATOM() or ctx.PIPE() + # skip the '{' + repeat_marker = ctx.LGROUP().getText()[1] + + min_rep, max_rep = None, None + match repeat_marker: + case "?": + min_rep, max_rep = 0, 1 + case "+": + min_rep, max_rep = 1, None + case "*": + min_rep, max_rep = 0, None + case _: + raise ValueError(f"Unexpected repeat marker: {repeat_marker}") + + return [Repeat.new(Repeat( + min=min_rep, + max=max_rep, + separator=separator.getText() if separator else None, + children=self.visitChildren(ctx) + ))] + + def visitCurlies(self, ctx: TacticNotationsParser.CurliesContext): + return [ + Literal.new(Literal(value=ctx.LBRACE().getText(), subscript=None)), + *self.visitChildren(ctx), + Literal.new(Literal(value=ctx.RBRACE().getText(), subscript=None))] + + def visitAtomic(self, ctx: TacticNotationsParser.AtomicContext): + return [Literal.new(Literal( + value=ctx.ATOM().getText(), + # skip '__' + subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None + ))] + + def visitHole(self, ctx: TacticNotationsParser.HoleContext): + return [Reference.new(Reference( + value=ctx.ID().getText()[1:], + # skip '__' + subscript=ctx.SUB().getText()[2:] if ctx.SUB() else None + ))] + + def visitEscaped(self, ctx: TacticNotationsParser.EscapedContext): + return [Literal.new(Literal( + value=ctx.ESCAPED().getText().replace("%", ""), + subscript=None + ))] + +def objectify(notation: str) -> list[TaggedNotationObject]: + """Translate a notation into an object. + + It is essentially a simplified and normalized version of the ANTLR AST. + """ + visitor = TacticNotationsToObjectVisitor() + return visitor.visit(parse(notation)) diff --git a/doc/tools/rocqrst/rocqdomain.py b/doc/tools/rocqrst/rocqdomain.py index 65051ffcce90..f60e3886f41b 100644 --- a/doc/tools/rocqrst/rocqdomain.py +++ b/doc/tools/rocqrst/rocqdomain.py @@ -21,9 +21,11 @@ # pylint: disable=import-outside-toplevel, abstract-method, too-many-lines import os +import json import re import shlex from itertools import chain +from dataclasses import dataclass from collections import defaultdict from docutils import nodes, utils @@ -33,6 +35,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes, version_info as sphinx_version +from sphinx.application import Sphinx from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.errors import ExtensionError @@ -41,12 +44,16 @@ from sphinx.util.logging import getLogger, get_node_location from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from sphinx.writers.latex import LaTeXTranslator +from sphinx.builders.text import TextBuilder +from sphinx_markdown_builder.translator import MarkdownTranslator, pushing_context +from sphinx_markdown_builder.contexts import WrappedContext from . import rocqdoc from .repl import ansicolors from .repl.rocqtop import RocqTop, RocqTopError from .notations.parsing import ParseError from .notations.sphinx import sphinxify +from .notations import object as object_notations from .notations.plain import stringify_with_ellipses # FIXME: Patch this in Sphinx @@ -84,6 +91,14 @@ def visit_desc_signature(self, node): Offending notation: {} Error message: {}""" +@dataclass +class SubdomainItemData: + """Data stored for each object in a subdomain""" + docname: str + objtype: str + targetid: str + syntax: list[object_notations.TaggedNotationObject] + def notation_to_sphinx(notation, source, line, rawtext=None): """Parse notation and wrap it in an inline node""" try: @@ -170,6 +185,14 @@ def _render_signature(self, signature, signode): """Render a signature, placing resulting nodes into signode.""" raise NotImplementedError(self) + def _signature_to_syntax(self, signature: str) -> list[object_notations.TaggedNotationObject]: + """Convert a signature into a syntax tree, used in generated plain JSON indices. + + By default, returns the signature as a literal string. + + """ + return [object_notations.Literal.new(object_notations.Literal(value=signature, subscript=None))] + option_spec = { # Explicit object naming 'name': directives.unchanged, @@ -179,7 +202,7 @@ def _render_signature(self, signature, signode): 'noindex': directives.flag } - def subdomain_data(self): + def subdomain_data(self) -> dict[str, SubdomainItemData]: if self.subdomain is None: raise ValueError() return self.env.domaindata['rocq']['objects'][self.subdomain] @@ -207,14 +230,14 @@ def handle_signature(self, signature, signode): names = [name] if name else None return names - def _warn_if_duplicate_name(self, objects, name, signode): + def _warn_if_duplicate_name(self, objects: dict[str, SubdomainItemData], name: str, signode): """Check that two objects in the same domain don't have the same name.""" if name in objects: MSG = 'Duplicate name {} (other is in {}) attached to {}' - msg = MSG.format(name, self.env.doc2path(objects[name][0]), signode) + msg = MSG.format(name, self.env.doc2path(objects[name].docname), signode) self.state_machine.reporter.warning(msg, line=self.lineno) - def _record_name(self, name, target_id, signode): + def _record_name(self, name, target_id, signature: str, signode): """Record a `name` in the current subdomain, mapping it to `target_id`. Warns if another object of the same name already exists; `signode` is @@ -222,19 +245,19 @@ def _record_name(self, name, target_id, signode): """ names_in_subdomain = self.subdomain_data() self._warn_if_duplicate_name(names_in_subdomain, name, signode) - names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + names_in_subdomain[name] = SubdomainItemData(self.env.docname, self.objtype, target_id, self._signature_to_syntax(signature)) def _target_id(self, name): return make_target(self.objtype, make_id(name)) - def _add_target(self, signode, name): + def _add_target(self, signature: str, signode, name): """Register a link target ‘name’, pointing to signode.""" targetid = self._target_id(name) if targetid not in self.state.document.ids: signode['ids'].append(targetid) signode['names'].append(name) signode['first'] = (not self.names) - self._record_name(name, targetid, signode) + self._record_name(name, targetid, signature, signode) else: # We don't warn for duplicates in the SSReflect chapter, because # it's the style of this chapter to repeat all the defined @@ -253,14 +276,14 @@ def _add_index_entry(self, name, target): index_text += " " + self.index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) - def add_target_and_index(self, names, _, signode): + def add_target_and_index(self, names, signature: str, signode): """Attach a link target to `signode` and index entries for `names`. This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified.""" if names: for name in names: if isinstance(name, str) and name.startswith('_'): continue - target = self._add_target(signode, name) + target = self._add_target(signature, signode, name) self._add_index_entry(name, target) self.state.document.note_explicit_target(signode) @@ -320,6 +343,9 @@ class NotationObject(DocumentableObject): Objects that inherit from this class can use the notation grammar (“{+ …}”, “@…”, etc.) in their signature. """ + def _signature_to_syntax(self, signature: str) -> list[object_notations.TaggedNotationObject]: + return object_notations.objectify(signature) + def _render_signature(self, signature, signode): position = self.state_machine.get_source_and_line(self.lineno) tacn_node = notation_to_sphinx(signature, *position) @@ -457,7 +483,7 @@ def _add_index_entry(self, name, target): def _target_id(self, name): return make_id('grammar-token-{}'.format(name[1])) - def _record_name(self, name, targetid, signode): + def _record_name(self, name, targetid, signature, signode): env = self.state.document.settings.env objects = env.domaindata['std']['objects'] self._warn_if_duplicate_name(objects, name, signode) @@ -975,12 +1001,12 @@ def generate(self, docnames=None): items = chain(*(self.domain.data['objects'][subdomain].items() for subdomain in self.subdomains)) - for itemname, (docname, _, anchor) in sorted(items, key=lambda x: x[0].lower()): - if docnames and docname not in docnames: + for itemname, data in sorted(items, key=lambda x: x[0].lower()): + if docnames and data.docname not in docnames: continue entries = content[itemname[0].lower()] - entries.append([itemname, 0, docname, anchor, '', '', '']) + entries.append([itemname, 0, data.docname, data.targetid, '', '', '']) collapse = False content = sorted(content.items()) @@ -1158,7 +1184,7 @@ class RocqDomain(Domain): initial_data = { # Collect everything under a key that we control, since Sphinx adds # others, such as “version” - 'objects' : { # subdomain → name → docname, objtype, targetid + 'objects' : { # subdomain → name → SubdomainItemData 'cmd': {}, 'tacn': {}, 'opt': {}, @@ -1182,8 +1208,8 @@ def find_index_by_name(targetid): def get_objects(self): # Used for searching and object inventories (intersphinx) for _, objects in self.data['objects'].items(): - for name, (docname, objtype, targetid) in objects.items(): - yield (name, name, objtype, docname, targetid, self.object_types[objtype].attrs['searchprio']) + for name, data in objects.items(): + yield (name, name, data.objtype, data.docname, data.targetid, self.object_types[data.objtype].attrs['searchprio']) for index in self.indices: yield (index.name, index.localname, 'index', "rocq-" + index.name, '', -1) @@ -1191,11 +1217,11 @@ def merge_domaindata(self, docnames, otherdata): DUP = "Duplicate declaration: '{}' also defined in '{}'.\n" for subdomain, their_objects in otherdata['objects'].items(): our_objects = self.data['objects'][subdomain] - for name, (docname, objtype, targetid) in their_objects.items(): - if docname in docnames: + for name, data in their_objects.items(): + if data.docname in docnames: if name in our_objects: - self.env.warn(docname, DUP.format(name, our_objects[name][0])) - our_objects[name] = (docname, objtype, targetid) + self.env.warn(data.docname, DUP.format(name, our_objects[name].docname)) + our_objects[name] = data def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contnode): # ‘target’ is the name that was written in the document @@ -1207,14 +1233,13 @@ def resolve_xref(self, env, fromdocname, builder, role, targetname, node, contno else: resolved = self.data['objects'][role].get(targetname) if resolved: - (todocname, _, targetid) = resolved - return make_refnode(builder, fromdocname, todocname, targetid, contnode, targetname) + return make_refnode(builder, fromdocname, resolved.docname, resolved.targetid, contnode, targetname) return None def clear_doc(self, docname_to_clear): for subdomain_objects in self.data['objects'].values(): - for name, (docname, _, _) in list(subdomain_objects.items()): - if docname == docname_to_clear: + for name, data in list(subdomain_objects.items()): + if data.docname == docname_to_clear: del subdomain_objects[name] def is_rocqtop_or_rocqdoc_block(node): @@ -1238,6 +1263,97 @@ def simplify_source_code_blocks_for_latex(app, doctree, fromdocname): # pylint: else: node.replace_self(nodes.literal_block(node.rawsource, node.rawsource, language="Coq")) +class IndicesMarkdownTranslator(MarkdownTranslator): + @pushing_context + def visit_caution(self, _node): + self._push_box("CAUTION") + + def visit_admonition(self, node): + self.add('\n\n') + def depart_admonition(self, node): + self.add('\n\n') + + # we do not create links in markdown + def visit_reference(self, node): + pass + def visit_download_reference(self, node): + pass + + + @pushing_context + def visit_desc_annotation(self, node): + text = node.astext().strip() + if text == "Error": + self.add("*Possible error*:") + raise nodes.SkipNode + elif text == "Warning": + self.add("*Possible warning*:") + raise nodes.SkipNode + self._push_context(WrappedContext("_")) + + def visit_subscript(self, node): + self.add('(') + def depart_subscript(self, node): + self.add(')') + + +class IndicesBuilder(TextBuilder): + """Custom sphinx builder to generate JSON files containing the content of our indices. + + It is based on the TextBuilder to be able to generate the content of the documentation for each object.""" + name = 'indices' + format = 'json' + allow_parallel = False + + default_translator_class = IndicesMarkdownTranslator + + def init(self): + super().init() + self.rendered: dict[str, str] = {} + + def write_doc(self, docname: str, doctree: nodes.document) -> None: + domain = self.env.get_domain('rocq') + # find all nodes that are handled by our rocq domain + for node in doctree.findall(lambda n: isinstance(n, nodes.Element) and n.get('objtype') in domain.object_types): + # all IDs will be associated to this content + all_target_ids = [] + for sig in node.traverse(addnodes.desc_signature): + all_target_ids.extend(sig.get('ids', [])) + + # the content is the next node + content_node = node.next_node(addnodes.desc_content) + + if all_target_ids and content_node: + # translate sphinx nodes to text and associate it to all IDs + translator = self.create_translator(doctree, self) + translator.visit_document(doctree) + content_node.walkabout(translator) + translator.depart_document(doctree) + text = translator.astext().strip() + # remove some leftover formatting + text = text.replace('\u200b', '|').replace('\\\\textquotesingle{}', "").replace('\\textquotesingle{}', "") + for tid in all_target_ids: + self.rendered[tid] = text + + def finish(self): + domain = self.env.get_domain('rocq') + + for index in RocqDomain.indices: + items: list[tuple[str, SubdomainItemData]] = chain(*(domain.data['objects'][subdomain].items() + for subdomain in index.subdomains)) + + output_data = {} + for name, data in items: + output_data[name] = { + "documentation_path": data.docname, + "documentation_anchor": data.targetid, + "syntax": [[tag, notation.asdict()] for [tag, notation] in data.syntax], + "documentation": self.rendered.get(data.targetid, "") + } + + with open(self.outdir / f"{index.name}.json", "w") as f: + json.dump(output_data, f, indent=2) + ROCQ_ADDITIONAL_DIRECTIVES = [RocqtopDirective, RocqdocDirective, ExampleDirective, @@ -1260,6 +1376,7 @@ def setup(app): # Add domain, directives, and roles app.add_domain(RocqDomain) + app.add_builder(IndicesBuilder) app.add_index_to_domain('std', StdGlossaryIndex) for role in ROCQ_ADDITIONAL_ROLES: diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 29cc29c3657b..986ed1324307 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -601,7 +601,7 @@ let update_delta_resolver resolver1 resolver2 = in let kn_apply_rslv kkey hint1 rslv = let hint = match hint1 with - | Equiv kequ -> solve_delta_kn resolver2 kequ + | Equiv kequ -> Equiv (kn_of_delta resolver2 kequ) | Inline (_,Some _) -> hint1 | Inline (_,None) -> (try Deltamap.find_kn kkey resolver2 with Not_found -> hint1) diff --git a/lib/feedback.ml b/lib/feedback.ml index 9823a2c8a415..0ace8e857699 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -102,13 +102,9 @@ let msg_debug ?loc x = feedback_logger ?loc Debug x (* Helper for tools willing to understand only the messages *) let console_feedback_listener fmt = let open Format in - let pp_loc fmt loc = let open Loc in match loc with - | None -> fprintf fmt "" - | Some loc -> - let where = - match loc.fname with InFile { file } -> file | ToplevelInput -> "Toplevel input" in - fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" - where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let pp_loc fmt = function + | None -> () + | Some loc -> Pp.pp_with fmt Pp.(Loc.pr loc ++ str ":" ++ fnl()) in let checker_feed (fb : feedback) = match fb.contents with | Processed -> () diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 91b703b6367c..603692598881 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1405,14 +1405,20 @@ struct Cases.compile_cases ?loc ~program_mode:flags.program_mode sty (pretype, sigma) tycon env (po,tml,eqns) let warn_nonbool_if = - let quickfix ~loc (cloc, pp) = - let qf loc = let loc = Loc.after loc 0 0 in [Quickfix.make ~loc pp] in - Option.cata qf [] cloc in + let quickfix ~loc:_ (cloc, ctor) = + match cloc with + | None -> [] + | Some cloc -> + let loc = Loc.after cloc 0 0 in + let pp = Pp.(str " is " ++ Nametab.pr_global_env Id.Set.empty (ConstructRef ctor)) in + [Quickfix.make ~loc pp] + in CWarnings.create ~name:"non-boolean-if" ~category:Deprecation.Version.v9_3 ~quickfix - (fun _ -> - strbrk "The \"if then _\" syntax for non boolean guard is deprecated. " - ++ strbrk "Use \"if is then _\" instead.") + (fun (_,ctor) -> + str "The \"if then _\" syntax for non boolean guard is deprecated." ++ spc() ++ + fmt "Use \"if is %t then _\" instead." + (fun () -> Nametab.pr_global_env Id.Set.empty (ConstructRef ctor))) let pretype_if self (c, (na, po), b1, b2) = fun ?loc ~flags tycon env sigma -> @@ -1436,7 +1442,7 @@ struct | Some bool -> GlobRef.CanOrd.equal (IndRef ind) bool in if not indf_is_bool then let cloc = loc_of_glob_constr c in - warn_nonbool_if ?loc (cloc, Pp.str " is " ++ Id.print cstrs.(0).cs_name) in + warn_nonbool_if ?loc (cloc, fst cstrs.(0).cs_cstr) in let arsgn, indr = let arsgn = get_arity !!env indf in (* Make dependencies from arity signature impossible *) diff --git a/printing/printer.ml b/printing/printer.ml index 94bdb06ce4c4..8379352eca6a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -610,6 +610,12 @@ let pr_ne_evar_set ?(flags=current_combined()) hd tl sigma l = (* Printer function for sets of Assumptions.assumptions. It is used primarily by the Print Assumptions command. *) +let { Goptions.get = print_all_assumptions } = + Goptions.declare_bool_option_and_ref + ~key:["Printing";"All";"Assumptions"] + ~value:false + () + type axiom = | Constant of Constant.t | Positive of MutInd.t @@ -668,10 +674,29 @@ end module ContextObjectSet = Set.Make (OrderedContextObject) module ContextObjectMap = Map.Make (OrderedContextObject) -let pr_assumptionset ?(flags=current_combined()) env sigma s = +type theory_assumptions = { + has_impredicative_set : bool; + has_rewrite_rules : bool; + has_type_in_type : bool; +} + +let pr_assumptionset ?(flags=current_combined()) env sigma theory_info s = + let print_all = print_all_assumptions () in + let dominated_by_env ax = + match ax with + | IndicesNotMattering _ -> not print_all && not (indices_matter env) + | _ -> false + in + let s = ContextObjectMap.filter (fun k _v -> match k with + | Axiom (ax, _) -> not (dominated_by_env ax) + | _ -> true) s + in + let show_theory_impredicative_set = (print_all && theory_info.has_impredicative_set) || is_impredicative_set env in + let show_theory_rewrite_rules = (print_all && theory_info.has_rewrite_rules) || rewrite_rules_allowed env in + let show_theory_type_in_type = (print_all && theory_info.has_type_in_type) || type_in_type env in if ContextObjectMap.is_empty s && - not (rewrite_rules_allowed env) && - not (is_impredicative_set env) then + not show_theory_rewrite_rules && + not show_theory_impredicative_set then str "Closed under the global context" else let safe_pr_constant env kn = @@ -751,17 +776,17 @@ let pr_assumptionset ?(flags=current_combined()) env sigma s = ContextObjectMap.fold fold s ([], [], [], []) in let theory = - if is_impredicative_set env then + if show_theory_impredicative_set then [str "Set is impredicative"] else [] in let theory = - if rewrite_rules_allowed env then + if show_theory_rewrite_rules then str "Rewrite rules are allowed (subject reduction might be broken)" :: theory else theory in let theory = - if type_in_type env then + if show_theory_type_in_type then str "Type hierarchy is collapsed (logic is inconsistent)" :: theory else theory in diff --git a/printing/printer.mli b/printing/printer.mli index 5d5dca50608f..b855f8a1e3dc 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -226,6 +226,9 @@ val pr_ne_evar_set : ?flags:PrintingFlags.t -> Evar.Set.t -> Pp.t (** Declarations for the "Print Assumption" command *) + +val print_all_assumptions : unit -> bool + type axiom = | Constant of Constant.t (* An axiom or a constant. *) | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *) @@ -244,8 +247,14 @@ module ContextObjectSet : CSet.ExtS with type elt = context_object module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet +type theory_assumptions = { + has_impredicative_set : bool; + has_rewrite_rules : bool; + has_type_in_type : bool; +} + val pr_assumptionset : ?flags:PrintingFlags.t -> - env -> evar_map -> types ContextObjectMap.t -> Pp.t + env -> evar_map -> theory_assumptions -> types ContextObjectMap.t -> Pp.t val pr_typing_flags : Declarations.typing_flags -> Pp.t diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index fadfbaa2f3c8..f6df05e3cc9d 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -91,11 +91,32 @@ let build_dependent_inductive ind (mib,mip) = Context.Rel.instance_list mkRel mip.mind_nrealdecls mib.mind_params_ctxt @ Context.Rel.instance_list mkRel 0 realargs) +(* For a template polymorphic inductive, generate an instance to + substitute into the contexts copied from the inductive declaration. + Using the default template levels (e.g. eq.u0) would make the type of + the scheme mention global template universes, so that each use of the + scheme would in turn constrain them (see the bad-template-constraint + warning and #22220). We thus use fresh levels, which become universes + of the scheme; the accompanying context set must be declared by the + caller. Qualities are kept at their (all-QType) defaults since the + scheme is monomorphic. This instance is only used for substitution + into the copied contexts: occurrences of the inductive in the scheme + itself keep an empty instance, as required for template inductives. + Since the schemes of an inductive type no longer share universes, a + scheme applying a previously declared scheme also needs constraints + relating its universes to those of the latter (see + [enforce_scheme_param_univs]). *) let maybe_template_instance (mib, mip) u = match mib.mind_template with -| None -> u +| None -> u, UnivGen.empty_sort_context | Some templ -> let () = assert (UVars.Instance.is_empty u) in - templ.template_defaults + let qdefaults, _ = UVars.Instance.to_array templ.template_defaults in + let _, ulen = UVars.AbstractContext.size templ.template_context in + let uinst = Array.init ulen (fun _ -> UnivGen.fresh_level ()) in + let inst = UVars.Instance.of_array (qdefaults, uinst) in + let us = Array.fold_right Univ.Level.Set.add uinst Univ.Level.Set.empty in + let csts = UVars.AbstractContext.instantiate inst templ.template_context in + inst, ((Sorts.QVar.Set.empty, us), csts) let named_hd env t na = named_hd env (Evd.from_env env) (EConstr.of_constr t) na let name_assumption env = function @@ -145,7 +166,7 @@ let error msg = user_err Pp.(str msg) let get_sym_eq_data env (ind,u) = let (mib,mip as specif) = lookup_mind_specif env ind in - let u = maybe_template_instance specif u in + let u, ctx = maybe_template_instance specif u in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; @@ -167,7 +188,7 @@ let get_sym_eq_data env (ind,u) = if not (List.equal Constr.equal params2 constrargs) then error "Constructors arguments must repeat the parameters."; (* nrealargs_ctxt and nrealargs are the same here *) - (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1) + (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1,ctx) (**********************************************************************) (* Check if an inductive type [ind] has the form *) @@ -181,7 +202,7 @@ let get_sym_eq_data env (ind,u) = let get_non_sym_eq_data env (ind,u) = let (mib,mip as specif) = lookup_mind_specif env ind in - let u = maybe_template_instance specif u in + let u, ctx = maybe_template_instance specif u in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; @@ -196,7 +217,7 @@ let get_non_sym_eq_data env (ind,u) = let _,constrargs = List.chop mib.mind_nparams constrargs in let constrargs = List.map (Vars.subst_instance_constr u) constrargs in let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in - (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs) + (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs,ctx) (**********************************************************************) (* Build the symmetry lemma associated to an inductive type *) @@ -214,8 +235,9 @@ let get_non_sym_eq_data env (ind,u) = let build_sym_scheme env _handle ind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in - let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' = get_sym_eq_data env indu in + let ctx = UnivGen.sort_context_union ctx ctx' in let cstr n = mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in let varH,_ = fresh env (default_id_of_ind ind mip) Id.Set.empty in @@ -267,16 +289,49 @@ let sym_scheme_kind = (* *) (**********************************************************************) -let const_of_scheme kind env handle ind ctx = +(* The universes standing for the template universes of the inductive + type are local to each scheme (see [maybe_template_instance]), so + the parameters of two schemes of the same inductive type live at a + priori unrelated universes. Applying the constant [c] of a + previously declared scheme to the parameters of the scheme being + built thus requires the sorts of the parameters of the latter to fit + in the sorts of the corresponding binders of the type of [c]. The + two parameter contexts have the same shape, except that the let-ins + of [paramsctxt] do not appear in the kernel-inferred type of [c]. *) +let enforce_scheme_param_univs env paramsctxt c ctx = + let univ_of_param t = + let _, s = decompose_prod_decls t in + if isSort s then Some (Sorts.univ_of_sort (destSort s)) else None + in + let rec fold ctx params t = match params with + | [] -> ctx + | LocalDef _ :: params -> fold ctx params t + | LocalAssum (_, ty) :: params -> + let _, cty, t = destProd t in + let ctx = match univ_of_param ty, univ_of_param cty with + | Some u, Some cu -> + (* trivial constraints, i.e. between global universes shared by + the two schemes, are dropped by enforce_leq *) + let qus, (qcst, ucst) = ctx in + qus, (qcst, UnivSubst.enforce_leq u cu ucst) + | _ -> ctx + in + fold ctx params t + in + fold ctx (List.rev paramsctxt) (Typeops.type_of_constant_in env (destConst c)) + +let const_of_scheme kind env handle ind paramsctxt ctx = let sym_scheme = match local_lookup_scheme handle kind ind with Some cst -> cst | None -> assert false in - with_context_set ctx (UnivGen.fresh_global_instance env sym_scheme) + let c, ctx = with_context_set ctx (UnivGen.fresh_global_instance env sym_scheme) in + c, enforce_scheme_param_univs env paramsctxt c ctx let build_sym_involutive_scheme env handle ind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in - let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' = get_sym_eq_data env indu in + let ctx = UnivGen.sort_context_union ctx ctx' in let eq,eqrefl,ctx = get_rocq_eq env ctx in - let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in + let sym, ctx = const_of_scheme sym_scheme_kind env handle ind paramsctxt ctx in let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.instance mkRel n paramsctxt) in let indr = UVars.subst_instance_relevance u mip.mind_relevance in let varH,_ = fresh env (default_id_of_ind ind mip) Id.Set.empty in @@ -384,10 +439,11 @@ let sym_involutive_scheme_kind = let build_l2r_rew_scheme dep env handle ind kind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in - let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' = get_sym_eq_data env indu in - let sym, ctx = const_of_scheme sym_scheme_kind env handle ind ctx in - let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env handle ind ctx in + let ctx = UnivGen.sort_context_union ctx ctx' in + let sym, ctx = const_of_scheme sym_scheme_kind env handle ind paramsctxt ctx in + let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env handle ind paramsctxt ctx in let eq,eqrefl,ctx = get_rocq_eq env ctx in let cstr n p = mkApp (mkConstructUi(indu,1), @@ -504,8 +560,9 @@ let build_l2r_rew_scheme dep env handle ind kind = let build_l2r_forward_rew_scheme dep env ind kind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in - let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = + let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1,ctx' = get_sym_eq_data env indu in + let ctx = UnivGen.sort_context_union ctx ctx' in let cstr n p = mkApp (mkConstructUi(indu,1), Array.concat [Context.Rel.instance mkRel n paramsctxt1; @@ -600,8 +657,9 @@ let build_l2r_forward_rew_scheme dep env ind kind = let build_r2l_forward_rew_scheme dep env ind kind = let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in - let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = + let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs,ctx') = get_non_sym_eq_data env indu in + let ctx = UnivGen.sort_context_union ctx ctx' in let cstr n = mkApp (mkConstructUi(indu,1),Context.Rel.instance mkRel n mib.mind_params_ctxt) in let constrargs_cstr = constrargs@[cstr 0] in @@ -810,7 +868,8 @@ let build_congr env (eq,refl,ctx) ind = let (ind,u as indu), ctx = with_context_set ctx (UnivGen.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in - let u = maybe_template_instance (mib, mip) u in + let u, ctx' = maybe_template_instance (mib, mip) u in + let ctx = UnivGen.sort_context_union ctx ctx' in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; if not (Int.equal mip.mind_nrealargs 1) then diff --git a/test-suite/bugs/bug_21816.v b/test-suite/bugs/bug_21816.v new file mode 100644 index 000000000000..3c8dfc2ae422 --- /dev/null +++ b/test-suite/bugs/bug_21816.v @@ -0,0 +1,21 @@ +Axiom R : Set. + +Module Type Typ. + Parameter Inline(10) t : Type. +End Typ. + +Module Make_UDTF (M:Typ). + Include M. +End Make_UDTF. + +Module R_as_UBE. + Definition t := R. +End R_as_UBE. + +Module FOO := Make_UDTF R_as_UBE. + +Module BAR. + Include FOO. +End BAR. + +Definition boom := BAR.t. diff --git a/test-suite/bugs/bug_22220.v b/test-suite/bugs/bug_22220.v new file mode 100644 index 000000000000..d617f6b83721 --- /dev/null +++ b/test-suite/bugs/bug_22220.v @@ -0,0 +1,42 @@ +(* Schemes over template polymorphic inductives (Scheme Rewriting) should + not mention the global template universes in their types, so that using + them does not constrain the template universes. + See https://github.com/rocq-prover/rocq/issues/22220 *) +Set Warnings "+bad-template-constraint". + +(* Eta-expansion constrains the universe of the first argument; this must + not touch eq.u0. *) +Check (fun x => @eq_sym x). +Check (fun x => @eq_sym_involutive x). +Check (fun x => @eq_rew x). +Check (fun x => @eq_rew_dep x). +Check (fun x => @eq_rew_fwd_dep x). +Check (fun x => @eq_rew_r x). +Check (fun x => @eq_rew_r_dep x). +Check (fun x => @eq_rew_fwd_r_dep x). + +(* These were already fine and must stay so. *) +Check (fun x => @eq_ind x). +Check (fun x => @eq_rect x). +Check (fun x => @eq_trans x). +Check (fun x => @f_equal x). + +(* The schemes must still be usable at arbitrary universes. *) +Goal forall (A : Type) (x y : A), x = y -> y = x. +Proof. intros A x y H. exact (eq_sym H). Qed. + +(* Scheme generation itself must also work with the warning as error. *) +Inductive myeq (A:Type) (x:A) : A -> Prop := myeq_refl : myeq A x x. +Scheme Rewriting for myeq. +Check (fun x => @myeq_sym x). +Check (fun x => @myeq_sym_involutive x). +Check (fun x => @myeq_rew_r_dep x). + +(* Also for a Type-sorted equality: the uses of eq applied to a + Type-sorted inductive in the sym_involutive and rew_r_dep schemes + must not constrain eq.u0 either. *) +Inductive myeqT (A:Type) (x:A) : A -> Type := myeqT_refl : myeqT A x x. +Scheme Rewriting for myeqT. +Check (fun x => @myeqT_sym x). +Check (fun x => @myeqT_sym_involutive x). +Check (fun x => @myeqT_rew_r_dep x). diff --git a/test-suite/dune b/test-suite/dune index eacf93cb714c..44c8049dac43 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -10,7 +10,8 @@ (rule (targets test_suite_config.inc) (mode (promote (until-clean))) - (action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe %{bin:rocq})))) + (deps (package rocq-runtime)) + (action (with-stdout-to %{targets} (run tools/coq_config_to_make.exe rocq)))) (rule (targets summary.log) diff --git a/test-suite/misc/coqdep-require-filter-categories.sh b/test-suite/misc/coqdep-require-filter-categories.sh index 6866752fd47e..4ca500b9fd3f 100755 --- a/test-suite/misc/coqdep-require-filter-categories.sh +++ b/test-suite/misc/coqdep-require-filter-categories.sh @@ -7,7 +7,7 @@ cd misc/coqdep-require-filter-categories code=0 $coqdep -worker @ROCQWORKER@ -R . 'Bla' ./*.v > stdout 2> stderr || code=$? -diff stdout.ref stdout -diff stderr.ref stderr +diff -u stdout.ref stdout +diff -u stderr.ref stderr exit $code diff --git a/test-suite/misc/coqdep-require-filter-categories/fA.v b/test-suite/misc/coqdep-require-filter-categories/fA.v index cf54686cbfd9..b025b403e296 100644 --- a/test-suite/misc/coqdep-require-filter-categories/fA.v +++ b/test-suite/misc/coqdep-require-filter-categories/fA.v @@ -1 +1,2 @@ -Require Import Prelude(something(..)) nonexistent. +(* a + comment *) Require Import Prelude(something(..)) nonexistent. diff --git a/test-suite/misc/coqdep-require-filter-categories/stderr.ref b/test-suite/misc/coqdep-require-filter-categories/stderr.ref index c83fb7a445a5..0b19339d1271 100644 --- a/test-suite/misc/coqdep-require-filter-categories/stderr.ref +++ b/test-suite/misc/coqdep-require-filter-categories/stderr.ref @@ -1,3 +1,4 @@ -Warning: in file fA.v, library +File "fA.v", line 2, characters 50-61: +Warning: library nonexistent is required and has not been found in the loadpath! [module-not-found,filesystem,default] diff --git a/test-suite/misc/external-deps/file1.notfound.deps b/test-suite/misc/external-deps/file1.notfound.deps index 2b3d7ab40db0..56c16d6f5183 100644 --- a/test-suite/misc/external-deps/file1.notfound.deps +++ b/test-suite/misc/external-deps/file1.notfound.deps @@ -1,4 +1,5 @@ -Warning: in file misc/external-deps/file1.v, external file d1 is required +File "misc/external-deps/file1.v", line 2, characters 51-55: +Warning: external file d1 is required from root foo.bar and has not been found in the loadpath! [module-not-found,filesystem,default] misc/external-deps/file1.vo misc/external-deps/file1.glob misc/external-deps/file1.v.beautified misc/external-deps/file1.required_vo: misc/external-deps/file1.v @ROCQWORKER@ diff --git a/test-suite/misc/external-deps/file1.v b/test-suite/misc/external-deps/file1.v index 1e331d0723ab..c061121b6206 100644 --- a/test-suite/misc/external-deps/file1.v +++ b/test-suite/misc/external-deps/file1.v @@ -1 +1,2 @@ -Comments From foo.bar Extra Dependency "d1". +(* a + comment *) Comments From foo.bar Extra Dependency "d1". diff --git a/test-suite/misc/external-deps/file2.notfound.deps b/test-suite/misc/external-deps/file2.notfound.deps index 90cf56ec4a78..3b7fc1f7976e 100644 --- a/test-suite/misc/external-deps/file2.notfound.deps +++ b/test-suite/misc/external-deps/file2.notfound.deps @@ -1,4 +1,5 @@ -Warning: in file misc/external-deps/file2.v, external file d1 is required +File "misc/external-deps/file2.v", line 1, characters 30-34: +Warning: external file d1 is required from root foo.bar and has not been found in the loadpath! [module-not-found,filesystem,default] misc/external-deps/file2.vo misc/external-deps/file2.glob misc/external-deps/file2.v.beautified misc/external-deps/file2.required_vo: misc/external-deps/file2.v @ROCQWORKER@ diff --git a/test-suite/output/If.out b/test-suite/output/If.out index 5b5605ebd0d5..b2fed907d8f8 100644 --- a/test-suite/output/If.out +++ b/test-suite/output/If.out @@ -1,8 +1,8 @@ if true then 1 else 0 : nat File "./output/If.v", line 3, characters 6-24: -Warning: The "if then _" syntax for non boolean guard is deprecated. Use -"if is then _" instead. +Warning: The "if then _" syntax for non boolean guard is deprecated. +Use "if is O then _" instead. [non-boolean-if,deprecated-since-9.3,deprecated,default] Quickfix: Replace File "./output/If.v", line 3, characters 10-10 with is O diff --git a/test-suite/output/PrintAllAssumptions.out b/test-suite/output/PrintAllAssumptions.out new file mode 100644 index 000000000000..98cabd21001c --- /dev/null +++ b/test-suite/output/PrintAllAssumptions.out @@ -0,0 +1,3 @@ +Closed under the global context +Theory: +Set is impredicative diff --git a/test-suite/output/PrintAllAssumptions.v b/test-suite/output/PrintAllAssumptions.v new file mode 100644 index 000000000000..ee25263bc865 --- /dev/null +++ b/test-suite/output/PrintAllAssumptions.v @@ -0,0 +1,10 @@ +(** Test for Set Printing All Assumptions *) +Require Import TestSuite.impred_set_prereq. + +(** Without the flag, impredicative_set is not in the current env, + so Print Assumptions hides the theory dependency *) +Print Assumptions impred_def. + +(** With the flag, per-definition theory info is shown *) +Set Printing All Assumptions. +Print Assumptions impred_def. diff --git a/test-suite/output/bug_11608.out b/test-suite/output/bug_11608.out index 074a66154abe..3ee30d6d1e8d 100644 --- a/test-suite/output/bug_11608.out +++ b/test-suite/output/bug_11608.out @@ -1,5 +1,6 @@ File "./output/bug_11608.v", line 10, characters 4-40: Warning: This interactive proof is not started by the "Proof" command. +Default Proof Using "(Type)" will be ignored. [missing-proof-command,fragile,default] Quickfix: Replace File "./output/bug_11608.v", line 10, characters 4-4 with Proof. diff --git a/test-suite/output/indices_matter.out b/test-suite/output/indices_matter.out index eff79ca98662..e1e9f69d49d5 100644 --- a/test-suite/output/indices_matter.out +++ b/test-suite/output/indices_matter.out @@ -3,3 +3,6 @@ M.X relies on indices not mattering. Axioms: M.X relies on indices not mattering. Closed under the global context +Closed under the global context +Axioms: +M.X relies on indices not mattering. diff --git a/test-suite/output/indices_matter.v b/test-suite/output/indices_matter.v index 1a6393627f59..e08cac477aa4 100644 --- a/test-suite/output/indices_matter.v +++ b/test-suite/output/indices_matter.v @@ -10,3 +10,11 @@ Module SetIndicesMatter. Unset Indices Matter. Print Assumptions M.X. End SetIndicesMatter. + +(* Test Set Printing All Assumptions *) +Module PrintingAllAssumptions. + Unset Indices Matter. + Print Assumptions M.X. + Set Printing All Assumptions. + Print Assumptions M.X. +End PrintingAllAssumptions. diff --git a/test-suite/prerequisite/impred_set_prereq.v b/test-suite/prerequisite/impred_set_prereq.v new file mode 100644 index 000000000000..96a0638c7923 --- /dev/null +++ b/test-suite/prerequisite/impred_set_prereq.v @@ -0,0 +1,2 @@ +(* -*- coq-prog-args: ("-impredicative-set"); -*- *) +Definition impred_def : Set := forall X : Set, X -> X. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 200c09a5d1c3..87b5fb59418d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -29,8 +29,8 @@ MLLIBFILES := $(COQMF_MLLIBFILES) METAFILE := $(COQMF_METAFILE) ROCQPACKAGE := $(COQMF_ROCQPACKAGE) LEGACYSUPPORT := $(COQMF_LEGACY_SUPPORT) -HASROCQPATH := $(COQMF_HAS_ROCQPATH) -ROCQPATH := $(COQMF_ROCQPATH) +HAS_PACKAGE_LOGICAL_PATH := $(COQMF_HAS_PACKAGE_LOGICAL_PATH) +PACKAGE_LOGICAL_PATH := $(COQMF_PACKAGE_LOGICAL_PATH) CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) OTHERFLAGS := $(COQMF_OTHERFLAGS) @@ -596,8 +596,8 @@ install: META $(call findlib_remove) $(call findlib_install, META $(FINDLIBFILESTOINSTALL)) $(HIDE)if [ "$(ROCQPACKAGE)" ]; then \ - if [ "$(HASROCQPATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \ - root="$(subst .,/,$(ROCQPATH))"; \ + if [ "$(HAS_PACKAGE_LOGICAL_PATH)" != "true" ]; then echo "Error: $(METAFILE) has no top-level rocqpath field"; exit 1; fi; \ + root="$(subst .,/,$(PACKAGE_LOGICAL_PATH))"; \ for f in $$(cat .filestoinstall); do\ df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`"; rc="$$?";\ if [ "$$rc" != "0" -o -z "$$df" ]; then\ @@ -609,7 +609,7 @@ install: META case "$$df" in \ "$$root") rel="" ;; \ "$$root"/*) rel="$${df#$$root/}" ;; \ - *) echo SKIP "$$f" since it is outside rocqpath "$(ROCQPATH)"; continue ;; \ + *) echo SKIP "$$f" since it is outside rocqpath "$(PACKAGE_LOGICAL_PATH)"; continue ;; \ esac; \ else \ case "$$rel" in /*) rel="$${rel#/}" ;; esac; \ diff --git a/tools/coqdep/lib/common.ml b/tools/coqdep/lib/common.ml index dcbab8d983a2..92f8b3d893b9 100644 --- a/tools/coqdep/lib/common.ml +++ b/tools/coqdep/lib/common.ml @@ -8,6 +8,27 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* count newlines to get a nice error location instead of raw chars *) +let get_loc f { Lexer.loc_start = start; loc_end = end_ } = + let ch = open_in f in + let rec loop lnum bol read = + if read = start then lnum, bol + else match input_char ch with + | '\n' -> loop (lnum+1) (read+1) (read+1) + | _ -> loop lnum bol (read+1) + in + let lnum, bol = Fun.protect ~finally:(fun () -> close_in ch) (fun () -> loop 1 0 0) in + { Loc.fname = InFile { dirpath=None; file=f }; + line_nb = lnum; + bol_pos = bol; + bp = start; + ep = end_; + + (* not used by printing *) + line_nb_last = 0; + bol_pos_last = 0; + } + (** Rocq files specifies on the command line: - first string is the full filename, with only its extension removed - second string is the absolute version of the previous (via getcwd) @@ -45,9 +66,8 @@ type what = Library | External let str_of_what = function Library -> "library" | External -> "external file" let warning_module_notfound = - let warn (what, from, f, s) = + let warn (what, from, s) = let open Pp in - str "in file " ++ str f ++ str ", " ++ str (str_of_what what) ++ spc () ++ str (String.concat "." s) ++ str " is required" ++ pr_opt (fun pth -> str "from root " ++ str (String.concat "." pth)) from ++ str " and has not been found in the loadpath!" @@ -150,13 +170,7 @@ let coq_to_stdlib from strl = | l -> l in match from with | Some from -> Some (tr_qualid from), strl - | None -> None, List.map tr_qualid strl - -let with_in_channel ~fname f = - let chan = try open_in fname - with Sys_error msg -> Error.cannot_open fname msg - in - Util.try_finally f chan close_in chan + | None -> None, List.map (Util.on_snd tr_qualid) strl let with_in_descr ~fname f = let descr = @@ -177,8 +191,6 @@ module State = struct let loadpath x = x.loadpath end -exception SyntaxErrorInFile of string - (* recursive because of Load *) let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basename = (* Visited marks *) @@ -203,23 +215,20 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena let f = basename ^ ".v" in with_in_descr ~fname:f @@ fun chan -> (* For lexing efficiency purposes, we ignore the positions in this function. - This will force us to reparse the file in case of error to get a proper - location, but in practice such errors should be exceedingly rare with - rocqdep. This lexer is indeed basically able to handle random nonsense - thrown at it. *) + We can still get accurate character counts, we're just missing newline info. *) let buf = lexbuf_from_descr ~with_positions:false chan in let open Lexer in let rec loop () = match coq_action buf with | exception Fin_fichier -> DepSet.elements !dependencies - | exception Syntax_error _ -> + | exception Syntax_error loc -> (* The locations are garbage due to with_positions:false, ignore them *) - raise (SyntaxErrorInFile f) + Error.cannot_parse ~loc:(get_loc f loc) | tok -> match tok with | Require (from, strl) -> let from, strl = coq_to_stdlib from strl in - let decl str = + let decl (loc, str) = if should_visit_v_and_mark from str then begin let files = safe_assoc loadpath from f str in let files = match from, files with @@ -232,7 +241,7 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena add_dep (Dep_info.Dep.Require file_str)) files | None -> if not (Loadpath.is_in_coqlib loadpath ?from str) then - warning_module_notfound (Library, from, f, str) + warning_module_notfound ~loc:(get_loc f loc) (Library, from, str) end in List.iter decl strl; @@ -276,37 +285,18 @@ let rec find_dependencies ({State.vAccu; separator_hack; loadpath} as st) basena in List.iter decl l); loop () - | External(from,str) -> + | External(loc,from,str) -> begin match safe_assoc loadpath ~what:External (Some from) f [str] with | Some (file :: _) -> add_dep (Dep_info.Dep.Other (canonize ~separator_hack vAccu file)) | Some [] -> assert false | None -> if not (Loadpath.is_other_in_coqlib loadpath ~from [str]) then - warning_module_notfound (External, Some from, f, [str]) + warning_module_notfound ~loc:(get_loc f loc) (External, Some from, [str]) end; loop () in loop () -(* Reparse the file to get the error location *) -let get_parse_error f = - with_in_channel ~fname:f @@ fun chan -> - let buf = Lexing.from_channel chan in - let rec loop () = match Lexer.coq_action buf with - | _tok -> loop () - | exception Lexer.Syntax_error (i, j) -> (i, j) - | exception Lexer.Fin_fichier -> - (* may technically happen due to race conditions, return a dummy value *) - (0, 0) - in - loop () - -let find_dependencies st basename = - try find_dependencies st basename - with SyntaxErrorInFile f -> - let (i, j) = get_parse_error f in - Error.cannot_parse f (i, j) - let compute_deps st = let mk_dep name = Dep_info.make ~name ~deps:(find_dependencies st name) in List.rev st.vAccu.acc |> List.to_seq |> Seq.map mk_dep @@ -366,7 +356,7 @@ let sort {State.vAccu; separator_hack; loadpath} = match Lexer.coq_action lb with | Lexer.Require (from, sl) -> List.iter - (fun s -> + (fun (_,s) -> match safe_assoc loadpath from ~warn_clashes:false file s with | None -> () | Some l -> List.iter loop l) diff --git a/tools/coqdep/lib/error.ml b/tools/coqdep/lib/error.ml index 8f3c544be50d..f8e2fa10c61c 100644 --- a/tools/coqdep/lib/error.ml +++ b/tools/coqdep/lib/error.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -exception CannotParseFile of string * (int * int) +exception CannotParseFile exception CannotParseProjectFile of string * string exception CannotOpenFile of string * string @@ -16,9 +16,8 @@ exception CannotOpenProjectFile of string let () = CErrors.register_handler @@ function - | CannotParseFile (s,(i,j)) -> - Some Pp.(str "File \"" ++ str s ++ str "\"," ++ str "characters" ++ spc () - ++ int i ++ str "-" ++ int j ++ str ":" ++ spc () ++ str "Syntax error") + | CannotParseFile -> + Some Pp.(str "Syntax error") | CannotParseProjectFile (file, msg) -> Some Pp.(str "Project file" ++ spc () ++ str "\"" ++ str file ++ str "\":" ++ spc () @@ -33,7 +32,7 @@ let () = CErrors.register_handler @@ function | _ -> None -let cannot_parse s ij = raise @@ CannotParseFile (s, ij) +let cannot_parse ~loc = Loc.raise ~loc @@ CannotParseFile let cannot_open_project_file msg = raise @@ CannotOpenProjectFile msg let cannot_parse_project_file file msg = raise @@ CannotParseProjectFile (file, msg) let cannot_open s msg = raise @@ CannotOpenFile (s, msg) diff --git a/tools/coqdep/lib/error.mli b/tools/coqdep/lib/error.mli index 2cee33dd053c..3db02f928e56 100644 --- a/tools/coqdep/lib/error.mli +++ b/tools/coqdep/lib/error.mli @@ -8,12 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -exception CannotParseFile of string * (int * int) -exception CannotParseProjectFile of string * string -exception CannotOpenFile of string * string -exception CannotOpenProjectFile of string - -val cannot_parse : string -> int * int -> 'a +val cannot_parse : loc:Loc.t -> 'a val cannot_open_project_file : string -> 'a val cannot_parse_project_file : string -> string -> 'a val cannot_open : string -> string -> 'a diff --git a/tools/coqdep/lib/lexer.mli b/tools/coqdep/lib/lexer.mli index 21af680674e9..f8038649d770 100644 --- a/tools/coqdep/lib/lexer.mli +++ b/tools/coqdep/lib/lexer.mli @@ -12,13 +12,15 @@ type qualid = string list type load = Logical of string | Physical of string +type loc = { loc_start : int; loc_end : int } + type coq_token = - | Require of qualid option * qualid list + | Require of qualid option * (loc * qualid) list | Declare of string list | Load of load - | External of qualid * string + | External of loc * qualid * string exception Fin_fichier -exception Syntax_error of int * int +exception Syntax_error of loc val coq_action : Lexing.lexbuf -> coq_token diff --git a/tools/coqdep/lib/lexer.mll b/tools/coqdep/lib/lexer.mll index 38b37428437b..a47d78fbfec9 100644 --- a/tools/coqdep/lib/lexer.mll +++ b/tools/coqdep/lib/lexer.mll @@ -13,18 +13,20 @@ open Filename open Lexing + type loc = { loc_start : int; loc_end : int } + type qualid = string list type load = Logical of string | Physical of string type coq_token = - | Require of qualid option * qualid list + | Require of qualid option * (loc * qualid) list | Declare of string list | Load of load - | External of qualid * string + | External of loc * qualid * string exception Fin_fichier - exception Syntax_error of int*int + exception Syntax_error of loc let unquote_string s = String.sub s 1 (String.length s - 2) @@ -36,8 +38,18 @@ let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos; lexbuf.lex_curr_p <- lexbuf.lex_start_p + let loc_start lexbuf = lexbuf.lex_abs_pos + lexbuf.lex_start_pos + let loc_end lexbuf = lexbuf.lex_abs_pos + lexbuf.lex_curr_pos + + let loc lexbuf = { loc_start=loc_start lexbuf; loc_end=loc_end lexbuf} + let syntax_error lexbuf = - raise (Syntax_error (Lexing.lexeme_start lexbuf, Lexing.lexeme_end lexbuf)) + (* abs_pos is position of the start of the buffer in the file + start/curr_pos are positions in the buffer *) + raise (Syntax_error ({ + loc_start = loc_start lexbuf; + loc_end = loc_end lexbuf; + })) let check_valid lexbuf s = match Unicode.ident_refutation s with @@ -76,16 +88,10 @@ } let space = [' ' '\t' '\n' '\r'] -let lowercase = ['a'-'z'] -let uppercase = ['A'-'Z'] -let identchar = ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9'] -let caml_up_ident = uppercase identchar* -let caml_low_ident = lowercase identchar* (* This is an overapproximation, we check correctness afterwards *) let coq_ident = ['A'-'Z' 'a'-'z' '_' '\128'-'\255'] ['A'-'Z' 'a'-'z' '_' '\'' '0'-'9' '\128'-'\255']* let coq_field = '.' coq_ident -let coq_qual_id_rex = coq_ident coq_field+ let dot = '.' ( space+ | eof) @@ -148,8 +154,9 @@ and extra_dep_rule from = parse | eof { syntax_error lexbuf } | '"' ([^ '"']+ as f) '"' (*'"'*) - { skip_to_dot lexbuf; - External (from,f) } + { let loc = loc lexbuf in + skip_to_dot lexbuf; + External (loc,from,f) } and require_modifiers from = parse | "(*" @@ -224,8 +231,10 @@ and require_file from = parse | space+ { require_file from lexbuf } | coq_ident - { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in - let qid = coq_qual_id_list [name] lexbuf in + { let loc_start = loc_start lexbuf in + let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in + let loc_end = loc_end lexbuf in + let qid = coq_qual_id_list [{loc_start;loc_end},name] lexbuf in parse_dot lexbuf; Require (from, qid) } | eof @@ -272,8 +281,10 @@ and coq_qual_id_list module_names = parse | space+ { coq_qual_id_list module_names lexbuf } | coq_ident - { let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in - coq_qual_id_list (name :: module_names) lexbuf + { let loc_start = loc_start lexbuf in + let name = coq_qual_id_tail [get_ident lexbuf] lexbuf in + let loc_end = loc_end lexbuf in + coq_qual_id_list (({loc_start;loc_end},name) :: module_names) lexbuf } | eof { syntax_error lexbuf } diff --git a/tools/coqdep/lib/rocqdep_main.ml b/tools/coqdep/lib/rocqdep_main.ml index 4f2c04a698e1..6282aa3c9daa 100644 --- a/tools/coqdep/lib/rocqdep_main.ml +++ b/tools/coqdep/lib/rocqdep_main.ml @@ -56,5 +56,7 @@ let main args = try coqdep args with exn -> - Format.eprintf "*** Error: @[%a@]@\n%!" Pp.pp_with (CErrors.print exn); + let exn = Exninfo.capture exn in + let loc = Loc.get_loc (snd exn) in + Feedback.msg_notice ?loc Pp.(str "Error: " ++ CErrors.iprint exn); exit 1 diff --git a/tools/dune_rule_gen/gen_rules.ml b/tools/dune_rule_gen/gen_rules.ml index 069caa5b51f4..f9e1b4ad7562 100644 --- a/tools/dune_rule_gen/gen_rules.ml +++ b/tools/dune_rule_gen/gen_rules.ml @@ -124,14 +124,9 @@ let main () = Format.pp_print_flush fmt (); () -let pr_feedback (fb : Feedback.feedback) = - match fb.contents with - | Message (_,_,_,msg) -> Format.eprintf "%a" Pp.pp_with msg - | _ -> () [@@warning "-4"] - let () = Printexc.record_backtrace true; - let _ : int = Feedback.add_feeder pr_feedback in + let _ : int = Feedback.add_feeder (Feedback.console_feedback_listener Format.err_formatter) in try main () with exn -> Format.eprintf "[gen_rules] Fatal error:@ @[<2>%a@]@\n%!" Pp.pp_with (CErrors.print exn); diff --git a/tools/rocqmakefile.ml b/tools/rocqmakefile.ml index 3acda768d96d..c943d773e357 100644 --- a/tools/rocqmakefile.ml +++ b/tools/rocqmakefile.ml @@ -435,8 +435,8 @@ let generate_conf_files oc p = | Some _, Present x -> read_meta_rocqpath x | _ -> None in - fprintf oc "COQMF_HAS_ROCQPATH = %s\n" (if Option.has_some rocqpath then "true" else "false"); - fprintf oc "COQMF_ROCQPATH = %s\n" (Option.default "" rocqpath) + fprintf oc "COQMF_HAS_PACKAGE_LOGICAL_PATH = %s\n" (if Option.has_some rocqpath then "true" else "false"); + fprintf oc "COQMF_PACKAGE_LOGICAL_PATH = %s\n" (Option.default "" rocqpath) let rec all_start_with prefix = function | [] -> true diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 313a5014e715..2e2058b9bbec 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -374,6 +374,13 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = (* Only keep the transitive dependencies *) let (_, graph, ax2ty) = traverse access grs in let open GlobRef in + let has_impredicative_set = ref false in + let has_rewrite_rules = ref false in + let has_type_in_type = ref false in + let collect_theory_flags (tf : Declarations.typing_flags) = + if tf.impredicative_set then has_impredicative_set := true; + if not tf.check_universes then has_type_in_type := true + in let fold obj contents accu = match obj with | VarRef id -> let decl = Global.lookup_named id in @@ -383,6 +390,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = else accu | ConstRef kn -> let cb = lookup_constant kn in + collect_theory_flags cb.const_typing_flags; + begin match cb.const_body with + | Symbol _ -> has_rewrite_rules := true + | _ -> () + end; let accu = if cb.const_typing_flags.check_guarded then accu else @@ -409,6 +421,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = accu | IndRef (m,_) | ConstructRef ((m,_),_) -> let mind = lookup_mind m in + collect_theory_flags mind.mind_typing_flags; let accu = if mind.mind_typing_flags.check_positive then accu else @@ -434,11 +447,17 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) access st grs = ContextObjectMap.add (Axiom (UIP m, l)) Constr.mkProp accu in let accu = - if not (Environ.indices_matter (Global.env ())) then accu - else if not (Array.exists (fun mip -> mip.mind_relies_on_indices_not_mattering) mind.mind_packets) then accu + if not (Array.exists (fun mip -> mip.mind_relies_on_indices_not_mattering) mind.mind_packets) then accu else let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in ContextObjectMap.add (Axiom (IndicesNotMattering m, l)) Constr.mkProp accu in accu - in GlobRef.Map_env.fold fold graph ContextObjectMap.empty + in + let map = GlobRef.Map_env.fold fold graph ContextObjectMap.empty in + let theory = { + has_impredicative_set = !has_impredicative_set; + has_rewrite_rules = !has_rewrite_rules; + has_type_in_type = !has_type_in_type; + } in + (theory, map) diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 9e80a9942ccb..5fa3ad65c6a7 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -31,4 +31,5 @@ val traverse : {!traverse} also applies. *) val assumptions : ?add_opaque:bool -> ?add_transparent:bool -> Global.indirect_accessor -> - TransparentState.t -> GlobRef.t list -> types ContextObjectMap.t + TransparentState.t -> GlobRef.t list -> + theory_assumptions * types ContextObjectMap.t diff --git a/vernac/comTactic.ml b/vernac/comTactic.ml index 79859d5b1281..81e746109c3f 100644 --- a/vernac/comTactic.ml +++ b/vernac/comTactic.ml @@ -41,31 +41,15 @@ let { Goptions.get = print_info_trace } = ~value:None () -let warn_end_tac = - CWarnings.create_warning ~name:"deprecated-end-tac" ~from:[Deprecation.Version.v9_2] () - -let pp_warn_end_tac = - let pptac end_tac = - let env = Global.env() in - let sigma = Evd.from_env env in - let pptac = Gentactic.print_glob env sigma end_tac in - Pp.(str ";" ++ spc() ++ pptac ++ str ".") - in - CWarnings.create_in warn_end_tac - ~quickfix:(fun ~loc end_tac -> [Quickfix.make ~loc (pptac end_tac)]) - Pp.(fun end_tac -> - fmt "Using \"...\" is deprecated, use \"%t\" instead" (fun () -> pptac end_tac)) - -let warn_end_tac ?loc end_tac = +let check_end_tac ?loc end_tac = match end_tac with | None -> CErrors.user_err ?loc Pp.(str "This \"...\" is useless, use \".\" instead.") - | Some end_tac -> - pp_warn_end_tac ?loc end_tac + | Some _ -> () let use_end_tac ~with_end_tac end_tac = if not with_end_tac.CAst.v then None else begin - warn_end_tac ?loc:with_end_tac.loc end_tac; + check_end_tac ?loc:with_end_tac.loc end_tac; Option.map Gentactic.interp end_tac end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f2a305d9d288..0d8ea9672857 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2364,9 +2364,9 @@ let vernac_print = (* Prints all the axioms and section variables used by a term *) let st = Conv_oracle.get_transp_state (Environ.oracle env) in let grs = List.map smart_global rs in - let nassums = + let (theory, nassums) = Assumptions.assumptions opaque_access st ~add_opaque:o ~add_transparent:t grs in - Printer.pr_assumptionset env sigma nassums + Printer.pr_assumptionset env sigma theory nassums | PrintStrategy r -> no_state @@ fun () -> print_strategy r | PrintRegistered -> no_state print_registered | PrintRegisteredSchemes -> no_state print_registered_schemes diff --git a/vernac/vernactypes.ml b/vernac/vernactypes.ml index de650bdabcf1..de4d2a8ea039 100644 --- a/vernac/vernactypes.ml +++ b/vernac/vernactypes.ml @@ -63,19 +63,27 @@ module Proof = struct | None -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).") | Some stack -> LStack.pop stack - let quickfix_missing_proof ~loc () = + let quickfix_missing_proof ~loc _ = (* quickfix is purely additive so the loc is 0 characters long, at the beginning of the command. *) let loc = { loc with Loc.ep = loc.Loc.bp } in [Quickfix.make ~loc Pp.(str "Proof." ++ fnl())] let warn_missing_proof = CWarnings.create ~name:"missing-proof-command" ~category:CWarnings.CoreCategories.fragile ~quickfix:quickfix_missing_proof - Pp.(fun () -> str "This interactive proof is not started by the \"Proof\" command.") + Pp.(fun default_using -> + str "This interactive proof is not started by the \"Proof\" command." ++ + (match default_using with + | None -> mt() + | Some using -> + spc() ++ str "Default Proof Using " ++ quote (Ppvernac.pr_using using) ++ str " will be ignored.")) let check_late_init ?loc p = if Option.has_some @@ Declare.Proof.has_late_init p then p else begin - warn_missing_proof ?loc (); + let missing_using = + if Global.sections_are_opened() then Proof_using.get_default_proof_using() else None + in + warn_missing_proof ?loc missing_using; Declare.Proof.finish_late_init p Implicit end