diff options
46 files changed, 813 insertions, 679 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index ebeee0d4e4..39c801197b 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -592,6 +592,9 @@ validate:quick: library:ci-argosy: extends: .ci-template +library:ci-bbv: + extends: .ci-template + library:ci-bedrock2: extends: .ci-template-flambda artifacts: diff --git a/Makefile.ci b/Makefile.ci index f58dd9f37a..d4383fd409 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -11,6 +11,7 @@ CI_TARGETS= \ ci-aac_tactics \ ci-argosy \ + ci-bbv \ ci-bedrock2 \ ci-bignums \ ci-color \ diff --git a/configure.ml b/configure.ml index 55d71f6c2e..ee2e50ef86 100644 --- a/configure.ml +++ b/configure.ml @@ -923,7 +923,11 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s (** * CC runtime flags *) -let cflags_dflt = "-Wall -Wno-unused -g -O2 -std=c99 -fasm" +(* Note that Coq's VM requires at least C99-compliant floating-point + arithmetic; this should be ensured by OCaml's own C flags, which + set a minimum of [--std=gnu99] ; modern compilers by default assume + C11 or later, so no explicit [--std=] flags are added by OCaml *) +let cflags_dflt = "-Wall -Wno-unused -g -O2" let cflags_sse2 = "-msse2 -mfpmath=sse" diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 70e3fe5c69..c18e556da8 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -200,6 +200,13 @@ : "${coqprime_CI_ARCHIVEURL:=${coqprime_CI_GITURL}/archive}" ######################################################################## +# bbv +######################################################################## +: "${bbv_CI_REF:=master}" +: "${bbv_CI_GITURL:=https://github.com/mit-plv/bbv}" +: "${bbv_CI_ARCHIVEURL:=${bbv_CI_GITURL}/archive}" + +######################################################################## # bedrock2 ######################################################################## : "${bedrock2_CI_REF:=tested}" diff --git a/dev/ci/ci-bbv.sh b/dev/ci/ci-bbv.sh new file mode 100755 index 0000000000..6892cea3e4 --- /dev/null +++ b/dev/ci/ci-bbv.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download bbv + +( cd "${CI_BUILD_DIR}/bbv" && make && make install ) diff --git a/doc/changelog/03-notations/11848-nicer-decimal-printing.rst b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst new file mode 100644 index 0000000000..1d3a390f36 --- /dev/null +++ b/doc/changelog/03-notations/11848-nicer-decimal-printing.rst @@ -0,0 +1,5 @@ +- **Changed:** + Nicer printing for decimal constants in R and Q. + 1.5 is now printed 1.5 rather than 15e-1. + (`#11848 <https://github.com/coq/coq/pull/11848>`_, + by Pierre Roux). diff --git a/doc/changelog/03-notations/11859-warn-inexact-float.rst b/doc/changelog/03-notations/11859-warn-inexact-float.rst new file mode 100644 index 0000000000..224ffdbe9b --- /dev/null +++ b/doc/changelog/03-notations/11859-warn-inexact-float.rst @@ -0,0 +1,6 @@ +- **Added:** + In primitive floats, print a warning when parsing a decimal value + that is not exactly a binary64 floating-point number. + For instance, parsing 0.1 will print a warning whereas parsing 0.5 won't. + (`#11859 <https://github.com/coq/coq/pull/11859>`_, + by Pierre Roux). diff --git a/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst new file mode 100644 index 0000000000..e409c638bb --- /dev/null +++ b/doc/changelog/07-commands-and-options/11944-rm-searchabout-cmd.rst @@ -0,0 +1,3 @@ +- **Removed:** Removed SearchAbout command that was deprecated in 8.5. + Use :cmd:`Search` instead. + (`#11944 <https://github.com/coq/coq/pull/11944>`_, by Jim Fehrle). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5ca0d8b81f..7401aff48c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -383,6 +383,10 @@ Changes in 8.11+beta1 <https://github.com/coq/coq/issues/3890>`_ and `#4638 <https://github.com/coq/coq/issues/4638>`_ by Maxime Dénès, review by Gaëtan Gilbert). +- **Changed:** + :cmd:`Fail` does not catch critical errors (including "stack overflow") + anymore (`#10173 <https://github.com/coq/coq/pull/10173>`_, + by Gaëtan Gilbert). - **Removed:** Undocumented :n:`Instance : !@type` syntax (`#10185 <https://github.com/coq/coq/pull/10185>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 39f2ccec29..acdd4408ed 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1062,6 +1062,11 @@ Floating-point constants are parsed and pretty-printed as (17-digit) decimal constants. This ensures that the composition :math:`\text{parse} \circ \text{print}` amounts to the identity. +.. warn:: The constant @numeral is not a binary64 floating-point value. A closest value will be used and unambiguously printed @numeral. [inexact-float,parsing] + + Not all decimal constants are floating-point values. This warning + is generated when parsing such a constant (for instance ``0.1``). + .. example:: .. coqtop:: all diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5ff26520a..d61e5ddce7 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -637,470 +637,6 @@ See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the dependencies among the files part of a Coq project. -.. _coqdoc: - -Documenting |Coq| files with coqdoc ------------------------------------ - -coqdoc is a documentation tool for the proof assistant |Coq|, similar to -``javadoc`` or ``ocamldoc``. The task of coqdoc is - - -#. to produce a nice |Latex| and/or HTML document from |Coq| source files, - readable for a human and not only for the proof assistant; -#. to help the user navigate his own (or third-party) sources. - - - -Principles -~~~~~~~~~~ - -Documentation is inserted into |Coq| files as *special comments*. Thus -your files will compile as usual, whether you use coqdoc or not. coqdoc -presupposes that the given |Coq| files are well-formed (at least -lexically). Documentation starts with ``(**``, followed by a space, and -ends with ``*)``. The documentation format is inspired by Todd -A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with -some syntax-light controls, described below. coqdoc is robust: it -shouldn’t fail, whatever the input is. But remember: “garbage in, -garbage out”. - - -|Coq| material inside documentation. -++++++++++++++++++++++++++++++++++++ - -|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets -may be nested, the inner ones being understood as being part of the -quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun -x => u]``). Inside quotations, the code is pretty-printed in the same -way as it is in code parts. - -Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be -followed by a newline and the latter must follow a newline. - - -Pretty-printing. -++++++++++++++++ - -coqdoc uses different faces for identifiers and keywords. The pretty- -printing of |Coq| tokens (identifiers or symbols) can be controlled -using one of the following commands: - -:: - - - (** printing *token* %...LATEX...% #...html...# *) - - -or - -:: - - - (** printing *token* $...LATEX math...$ #...html...# *) - - -It gives the |Latex| and HTML texts to be produced for the given |Coq| -token. Either the |Latex| or the HTML rule may be omitted, causing the -default pretty-printing to be used for this token. - -The printing for one token can be removed with - -:: - - - (** remove printing *token* *) - - -Initially, the pretty-printing table contains the following mapping: - -===== === ==== ===== === ==== ==== === -`->` → `<-` ← `*` × -`<=` ≤ `>=` ≥ `=>` ⇒ -`<>` ≠ `<->` ↔ `|-` ⊢ -`\\/` ∨ `/\\` ∧ `~` ¬ -===== === ==== ===== === ==== ==== === - -Any of these can be overwritten or suppressed using the printing -commands. - -.. note:: - - The recognition of tokens is done by a (``ocaml``) lex - automaton and thus applies the longest-match rule. For instance, `->~` - is recognized as a single token, where |Coq| sees two tokens. It is the - responsibility of the user to insert space between tokens *or* to give - pretty-printing rules for the possible combinations, e.g. - - :: - - (** printing ->~ %\ensuremath{\rightarrow\lnot}% *) - - - -Sections -++++++++ - -Sections are introduced by 1 to 4 asterisks at the beginning of a line -followed by a space and the title of the section. One asterisk is a section, -two a subsection, etc. - -.. example:: - - :: - - (** * Well-founded relations - - In this section, we introduce... *) - - -Lists. -++++++ - -List items are introduced by a leading dash. coqdoc uses whitespace to -determine the depth of a new list item and which text belongs in which -list items. A list ends when a line of text starts at or before the -level of indenting of the list’s dash. A list item’s dash must always -be the first non-space character on its line (so, in particular, a -list can not begin on the first line of a comment - start it on the -second line instead). - -.. example:: - - :: - - We go by induction on [n]: - - If [n] is 0... - - If [n] is [S n'] we require... - - two paragraphs of reasoning, and two subcases: - - - In the first case... - - In the second case... - - So the theorem holds. - - - -Rules. -++++++ - -More than 4 leading dashes produce a horizontal rule. - - -Emphasis. -+++++++++ - -Text can be italicized by enclosing it in underscores. A non-identifier -character must precede the leading underscore and follow the trailing -underscore, so that uses of underscores in names aren’t mistaken for -emphasis. Usually, these are spaces or punctuation. - -:: - - This sentence contains some _emphasized text_. - - - -Escaping to |Latex| and HTML. -+++++++++++++++++++++++++++++++ - -Pure |Latex| or HTML material can be inserted using the following -escape sequences: - - -+ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode. - Simply discarded in HTML output. -+ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply - discarded in HTML output. -+ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in - |Latex| output. - -.. note:: - to simply output the characters ``$``, ``%`` and ``#`` and escaping - their escaping role, these characters must be doubled. - - -Verbatim -++++++++ - -Verbatim material is introduced by a leading ``<<`` and closed by ``>>`` -at the beginning of a line. - -.. example:: - - :: - - Here is the corresponding caml code: - << - let rec fact n = - if n <= 1 then 1 else n * fact (n-1) - >> - - - -Hyperlinks -++++++++++ - -Hyperlinks can be inserted into the HTML output, so that any -identifier is linked to the place of its definition. - -``coqc file.v`` automatically dumps localization information in -``file.glob`` or appends it to a file specified using the option ``--dump-glob -file``. Take care of erasing this global file, if any, when starting -the whole compilation process. - -Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look -for name resolutions in the file ``file`` (it will look in ``file.glob`` -by default). - -Identifiers from the |Coq| standard library are linked to the Coq website -`<http://coq.inria.fr/library/>`_. This behavior can be changed -using command line options ``--no-externals`` and ``--coqlib``; see below. - - -Hiding / Showing parts of the source. -+++++++++++++++++++++++++++++++++++++ - -Some parts of the source can be hidden using command line options ``-g`` -and ``-l`` (see below), or using such comments: - -:: - - - (* begin hide *) - *some Coq material* - (* end hide *) - - -Conversely, some parts of the source which would be hidden can be -shown using such comments: - -:: - - - (* begin show *) - *some Coq material* - (* end show *) - - -The latter cannot be used around some inner parts of a proof, but can -be used around a whole proof. - - -Usage -~~~~~ - -coqdoc is invoked on a shell command line as follows: -``coqdoc <options and files>``. -Any command line argument which is not an option is considered to be a -file (even if it starts with a ``-``). |Coq| files are identified by the -suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. - - -:HTML output: This is the default output format. One HTML file is created for - each |Coq| file given on the command line, together with a file - ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a - style sheet named ``style.css``. Such a file is distributed with coqdoc. -:|Latex| output: A single |Latex| file is created, on standard - output. It can be redirected to a file using the option ``-o``. The order of - files on the command line is kept in the final document. |Latex| - files given on the command line are copied ‘as is’ in the final - document . DVI and PostScript can be produced directly with the - options ``-dvi`` and ``-ps`` respectively. -:TEXmacs output: To translate the input files to TEXmacs format, - to be used by the TEXmacs |Coq| interface. - - - -Command line options -++++++++++++++++++++ - - -**Overall options** - - - :--HTML: Select a HTML output. - :--|Latex|: Select a |Latex| output. - :--dvi: Select a DVI output. - :--ps: Select a PostScript output. - :--texmacs: Select a TEXmacs output. - :--stdout: Write output to stdout. - :-o file, --output file: Redirect the output into the file ‘file’ - (meaningless with ``-html``). - :-d dir, --directory dir: Output files into directory ‘dir’ instead of - the current directory (option ``-d`` does not change the filename specified - with the option ``-o``, if any). - :--body-only: Suppress the header and trailer of the final document. - Thus, you can insert the resulting document into a larger one. - :-p string, --preamble string: Insert some material in the |Latex| - preamble, right before ``\begin{document}`` (meaningless with ``-html``). - :--vernac-file file,--tex-file file: Considers the file ‘file’ - respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. - :--files-from file: Read filenames to be processed from the file ‘file’ as if - they were given on the command line. Useful for program sources split - up into several directories. - :-q, --quiet: Be quiet. Do not print anything except errors. - :-h, --help: Give a short summary of the options and exit. - :-v, --version: Print the version and exit. - - - -**Index options** - - The default behavior is to build an index, for the HTML output only, - into ``index.html``. - - :--no-index: Do not output the index. - :--multi-index: Generate one page for each category and each letter in - the index, together with a top page ``index.html``. - :--index string: Make the filename of the index string instead of - “index”. Useful since “index.html” is special. - - - -**Table of contents option** - - :-toc, --table-of-contents: Insert a table of contents. For a |Latex| - output, it inserts a ``\tableofcontents`` at the beginning of the - document. For a HTML output, it builds a table of contents into - ``toc.html``. - :--toc-depth int: Only include headers up to depth ``int`` in the table of - contents. - - -**Hyperlink options** - - :--glob-from file: Make references using |Coq| globalizations from file - file. (Such globalizations are obtained with Coq option ``-dump-glob``). - :--no-externals: Do not insert links to the |Coq| standard library. - :--external url coqdir: Use given URL for linking references whose - name starts with prefix ``coqdir``. - :--coqlib url: Set base URL for the Coq standard library (default is - `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url - Coq``. - :-R dir coqdir: Recursively map physical directory dir to |Coq| logical - directory ``coqdir`` (similarly to |Coq| option ``-R``). - :-Q dir coqdir: Map physical directory dir to |Coq| logical - directory ``coqdir`` (similarly to |Coq| option ``-Q``). - - .. note:: - - options ``-R`` and ``-Q`` only have - effect on the files *following* them on the command line, so you will - probably need to put this option first. - - -**Title options** - - :-s , --short: Do not insert titles for the files. The default - behavior is to insert a title like “Library Foo” for each file. - :--lib-name string: Print “string Foo” instead of “Library Foo” in - titles. For example “Chapter” and “Module” are reasonable choices. - :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles. - :--lib-subtitles: Look for library subtitles. When enabled, the - beginning of each file is checked for a comment of the form: - - :: - - (** * ModuleName : text *) - - where ``ModuleName`` must be the name of the file. If it is present, the - text is used as a subtitle for the module in appropriate places. - :-t string, --title string: Set the document title. - - -**Contents options** - - :-g, --gallina: Do not print proofs. - :-l, --light: Light mode. Suppress proofs (as with ``-g``) and the following commands: - - + [Recursive] Tactic Definition - + Hint / Hints - + Require - + Transparent / Opaque - + Implicit Argument / Implicits - + Section / Variable / Hypothesis / End - - - - The behavior of options ``-g`` and ``-l`` can be locally overridden using the - ``(* begin show *) … (* end show *)`` environment (see above). - - There are a few options that control the parsing of comments: - - :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as - well. They are typeset inline. - :--plain-comments: Do not interpret comments, simply copy them as - plain-text. - :--interpolate: Use the globalization information to typeset - identifiers appearing in |Coq| escapings inside comments. - -**Language options** - - - The default behavior is to assume ASCII 7 bit input files. - - :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to - --inputenc latin1 --charset iso-8859-1. - :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset - utf-8 for HTML output. Also use Unicode replacements for a couple of - standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex| - UTF-8 support can be found - at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode - characters by |Latex|, extra packages which coqdoc does not provide - by default might be required, such as textgreek for some Greek letters - or ``stmaryrd`` for some mathematical symbols. If a Unicode character is - missing an interpretation in the utf8x input encoding, add - ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages - and declarations can be added with option ``-p``. - :--inputenc string: Give a |Latex| input encoding, as an option to |Latex| - package ``inputenc``. - :--charset string: Specify the HTML character set, to be inserted in - the HTML header. - - - -The coqdoc |Latex| style file -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -In case you choose to produce a document without the default |Latex| -preamble (by using option ``--no-preamble``), then you must insert into -your own preamble the command - -:: - - \usepackage{coqdoc} - -The package optionally takes the argument ``[color]`` to typeset -identifiers with colors (this requires the ``xcolor`` package). - -Then you may alter the rendering of the document by redefining some -macros: - -:coqdockw, coqdocid, …: The one-argument macros for typesetting - keywords and identifiers. Defaults are sans-serif for keywords and - italic for identifiers.For example, if you would like a slanted font - for keywords, you may insert - - :: - - \renewcommand{\coqdockw}[1]{\textsl{#1}} - - - anywhere between ``\usepackage{coqdoc}`` and ``\begin{document}``. - - -:coqdocmodule: - One-argument macro for typesetting the title of a ``.v`` - file. Default is - - :: - - \newcommand{\coqdocmodule}[1]{\section*{Module #1}} - - and you may redefine it using ``\renewcommand``. - Embedded Coq phrases inside |Latex| documents --------------------------------------------- diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index c33d62532e..b22c5286fe 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -321,18 +321,6 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. - .. cmdv:: SearchAbout - :name: SearchAbout - - .. deprecated:: 8.5 - - Up to |Coq| version 8.4, :cmd:`Search` had the behavior of current - :cmd:`SearchHead` and the behavior of current :cmd:`Search` was obtained with - command :cmd:`SearchAbout`. For compatibility, the deprecated name - :cmd:`SearchAbout` can still be used as a synonym of :cmd:`Search`. For - compatibility, the list of objects to search when using :cmd:`SearchAbout` - may also be enclosed by optional ``[ ]`` delimiters. - .. cmd:: SearchHead @term @@ -929,16 +917,17 @@ Quitting and debugging .. cmd:: Fail @command - For debugging scripts, sometimes it is desirable to know - whether a command or a tactic fails. If the given :n:`@command` - fails, the ``Fail`` statement succeeds, without changing the proof - state, and in interactive mode, the system - prints a message confirming the failure. - If the given :n:`@command` succeeds, the statement is an error, and - it prints a message indicating that the failure did not occur. + For debugging scripts, sometimes it is desirable to know whether a + command or a tactic fails. If the given :n:`@command` fails, then + :n:`Fail @command` succeeds (excepts in the case of + critical errors, like a "stack overflow"), without changing the + proof state, and in interactive mode, the system prints a message + confirming the failure. .. exn:: The command has not failed! - :undocumented: + + If the given :n:`@command` succeeds, then :n:`Fail @command` + fails with this error message. .. _controlling-display: diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst new file mode 100644 index 0000000000..cada680895 --- /dev/null +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -0,0 +1,463 @@ +.. _coqdoc: + +Documenting |Coq| files with coqdoc +----------------------------------- + +coqdoc is a documentation tool for the proof assistant |Coq|, similar to +``javadoc`` or ``ocamldoc``. The task of coqdoc is + + +#. to produce a nice |Latex| and/or HTML document from |Coq| source files, + readable for a human and not only for the proof assistant; +#. to help the user navigate his own (or third-party) sources. + + + +Principles +~~~~~~~~~~ + +Documentation is inserted into |Coq| files as *special comments*. Thus +your files will compile as usual, whether you use coqdoc or not. coqdoc +presupposes that the given |Coq| files are well-formed (at least +lexically). Documentation starts with ``(**``, followed by a space, and +ends with ``*)``. The documentation format is inspired by Todd +A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with +some syntax-light controls, described below. coqdoc is robust: it +shouldn’t fail, whatever the input is. But remember: “garbage in, +garbage out”. + + +|Coq| material inside documentation. +++++++++++++++++++++++++++++++++++++ + +|Coq| material is quoted between the delimiters ``[`` and ``]``. Square brackets +may be nested, the inner ones being understood as being part of the +quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun +x => u]``). Inside quotations, the code is pretty-printed in the same +way as it is in code parts. + +Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be +followed by a newline and the latter must follow a newline. + + +Pretty-printing. +++++++++++++++++ + +coqdoc uses different faces for identifiers and keywords. The pretty- +printing of |Coq| tokens (identifiers or symbols) can be controlled +using one of the following commands: + +:: + + + (** printing *token* %...LATEX...% #...html...# *) + + +or + +:: + + + (** printing *token* $...LATEX math...$ #...html...# *) + + +It gives the |Latex| and HTML texts to be produced for the given |Coq| +token. Either the |Latex| or the HTML rule may be omitted, causing the +default pretty-printing to be used for this token. + +The printing for one token can be removed with + +:: + + + (** remove printing *token* *) + + +Initially, the pretty-printing table contains the following mapping: + +===== === ==== ===== === ==== ==== === +`->` → `<-` ← `*` × +`<=` ≤ `>=` ≥ `=>` ⇒ +`<>` ≠ `<->` ↔ `|-` ⊢ +`\\/` ∨ `/\\` ∧ `~` ¬ +===== === ==== ===== === ==== ==== === + +Any of these can be overwritten or suppressed using the printing +commands. + +.. note:: + + The recognition of tokens is done by a (``ocaml``) lex + automaton and thus applies the longest-match rule. For instance, `->~` + is recognized as a single token, where |Coq| sees two tokens. It is the + responsibility of the user to insert space between tokens *or* to give + pretty-printing rules for the possible combinations, e.g. + + :: + + (** printing ->~ %\ensuremath{\rightarrow\lnot}% *) + + + +Sections +++++++++ + +Sections are introduced by 1 to 4 asterisks at the beginning of a line +followed by a space and the title of the section. One asterisk is a section, +two a subsection, etc. + +.. example:: + + :: + + (** * Well-founded relations + + In this section, we introduce... *) + + +Lists. +++++++ + +List items are introduced by a leading dash. coqdoc uses whitespace to +determine the depth of a new list item and which text belongs in which +list items. A list ends when a line of text starts at or before the +level of indenting of the list’s dash. A list item’s dash must always +be the first non-space character on its line (so, in particular, a +list can not begin on the first line of a comment - start it on the +second line instead). + +.. example:: + + :: + + We go by induction on [n]: + - If [n] is 0... + - If [n] is [S n'] we require... + + two paragraphs of reasoning, and two subcases: + + - In the first case... + - In the second case... + + So the theorem holds. + + + +Rules. +++++++ + +More than 4 leading dashes produce a horizontal rule. + + +Emphasis. ++++++++++ + +Text can be italicized by enclosing it in underscores. A non-identifier +character must precede the leading underscore and follow the trailing +underscore, so that uses of underscores in names aren’t mistaken for +emphasis. Usually, these are spaces or punctuation. + +:: + + This sentence contains some _emphasized text_. + + + +Escaping to |Latex| and HTML. ++++++++++++++++++++++++++++++++ + +Pure |Latex| or HTML material can be inserted using the following +escape sequences: + + ++ ``$...LATEX stuff...$`` inserts some |Latex| material in math mode. + Simply discarded in HTML output. ++ ``%...LATEX stuff...%`` inserts some |Latex| material. Simply + discarded in HTML output. ++ ``#...HTML stuff...#`` inserts some HTML material. Simply discarded in + |Latex| output. + +.. note:: + to simply output the characters ``$``, ``%`` and ``#`` and escaping + their escaping role, these characters must be doubled. + + +Verbatim +++++++++ + +Verbatim material is introduced by a leading ``<<`` and closed by ``>>`` +at the beginning of a line. + +.. example:: + + :: + + Here is the corresponding caml code: + << + let rec fact n = + if n <= 1 then 1 else n * fact (n-1) + >> + + + +Hyperlinks +++++++++++ + +Hyperlinks can be inserted into the HTML output, so that any +identifier is linked to the place of its definition. + +``coqc file.v`` automatically dumps localization information in +``file.glob`` or appends it to a file specified using the option ``--dump-glob +file``. Take care of erasing this global file, if any, when starting +the whole compilation process. + +Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look +for name resolutions in the file ``file`` (it will look in ``file.glob`` +by default). + +Identifiers from the |Coq| standard library are linked to the Coq website +`<http://coq.inria.fr/library/>`_. This behavior can be changed +using command line options ``--no-externals`` and ``--coqlib``; see below. + + +Hiding / Showing parts of the source. ++++++++++++++++++++++++++++++++++++++ + +Some parts of the source can be hidden using command line options ``-g`` +and ``-l`` (see below), or using such comments: + +:: + + + (* begin hide *) + *some Coq material* + (* end hide *) + + +Conversely, some parts of the source which would be hidden can be +shown using such comments: + +:: + + + (* begin show *) + *some Coq material* + (* end show *) + + +The latter cannot be used around some inner parts of a proof, but can +be used around a whole proof. + + +Usage +~~~~~ + +coqdoc is invoked on a shell command line as follows: +``coqdoc <options and files>``. +Any command line argument which is not an option is considered to be a +file (even if it starts with a ``-``). |Coq| files are identified by the +suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. + + +:HTML output: This is the default output format. One HTML file is created for + each |Coq| file given on the command line, together with a file + ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a + style sheet named ``style.css``. Such a file is distributed with coqdoc. +:|Latex| output: A single |Latex| file is created, on standard + output. It can be redirected to a file using the option ``-o``. The order of + files on the command line is kept in the final document. |Latex| + files given on the command line are copied ‘as is’ in the final + document . DVI and PostScript can be produced directly with the + options ``-dvi`` and ``-ps`` respectively. +:TEXmacs output: To translate the input files to TEXmacs format, + to be used by the TEXmacs |Coq| interface. + + + +Command line options +++++++++++++++++++++ + + +**Overall options** + + + :--HTML: Select a HTML output. + :--|Latex|: Select a |Latex| output. + :--dvi: Select a DVI output. + :--ps: Select a PostScript output. + :--texmacs: Select a TEXmacs output. + :--stdout: Write output to stdout. + :-o file, --output file: Redirect the output into the file ‘file’ + (meaningless with ``-html``). + :-d dir, --directory dir: Output files into directory ‘dir’ instead of + the current directory (option ``-d`` does not change the filename specified + with the option ``-o``, if any). + :--body-only: Suppress the header and trailer of the final document. + Thus, you can insert the resulting document into a larger one. + :-p string, --preamble string: Insert some material in the |Latex| + preamble, right before ``\begin{document}`` (meaningless with ``-html``). + :--vernac-file file,--tex-file file: Considers the file ‘file’ + respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. + :--files-from file: Read filenames to be processed from the file ‘file’ as if + they were given on the command line. Useful for program sources split + up into several directories. + :-q, --quiet: Be quiet. Do not print anything except errors. + :-h, --help: Give a short summary of the options and exit. + :-v, --version: Print the version and exit. + + + +**Index options** + + The default behavior is to build an index, for the HTML output only, + into ``index.html``. + + :--no-index: Do not output the index. + :--multi-index: Generate one page for each category and each letter in + the index, together with a top page ``index.html``. + :--index string: Make the filename of the index string instead of + “index”. Useful since “index.html” is special. + + + +**Table of contents option** + + :-toc, --table-of-contents: Insert a table of contents. For a |Latex| + output, it inserts a ``\tableofcontents`` at the beginning of the + document. For a HTML output, it builds a table of contents into + ``toc.html``. + :--toc-depth int: Only include headers up to depth ``int`` in the table of + contents. + + +**Hyperlink options** + + :--glob-from file: Make references using |Coq| globalizations from file + file. (Such globalizations are obtained with Coq option ``-dump-glob``). + :--no-externals: Do not insert links to the |Coq| standard library. + :--external url coqdir: Use given URL for linking references whose + name starts with prefix ``coqdir``. + :--coqlib url: Set base URL for the Coq standard library (default is + `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url + Coq``. + :-R dir coqdir: Recursively map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-R``). + :-Q dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-Q``). + + .. note:: + + options ``-R`` and ``-Q`` only have + effect on the files *following* them on the command line, so you will + probably need to put this option first. + + +**Title options** + + :-s , --short: Do not insert titles for the files. The default + behavior is to insert a title like “Library Foo” for each file. + :--lib-name string: Print “string Foo” instead of “Library Foo” in + titles. For example “Chapter” and “Module” are reasonable choices. + :--no-lib-name: Print just “Foo” instead of “Library Foo” in titles. + :--lib-subtitles: Look for library subtitles. When enabled, the + beginning of each file is checked for a comment of the form: + + :: + + (** * ModuleName : text *) + + where ``ModuleName`` must be the name of the file. If it is present, the + text is used as a subtitle for the module in appropriate places. + :-t string, --title string: Set the document title. + + +**Contents options** + + :-g, --gallina: Do not print proofs. + :-l, --light: Light mode. Suppress proofs (as with ``-g``) and the following commands: + + + [Recursive] Tactic Definition + + Hint / Hints + + Require + + Transparent / Opaque + + Implicit Argument / Implicits + + Section / Variable / Hypothesis / End + + + + The behavior of options ``-g`` and ``-l`` can be locally overridden using the + ``(* begin show *) … (* end show *)`` environment (see above). + + There are a few options that control the parsing of comments: + + :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as + well. They are typeset inline. + :--plain-comments: Do not interpret comments, simply copy them as + plain-text. + :--interpolate: Use the globalization information to typeset + identifiers appearing in |Coq| escapings inside comments. + +**Language options** + + + The default behavior is to assume ASCII 7 bit input files. + + :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to + --inputenc latin1 --charset iso-8859-1. + :-utf8, --utf8: Set --inputenc utf8x for |Latex| output and--charset + utf-8 for HTML output. Also use Unicode replacements for a couple of + standard plain ASCII notations such as → for ``->`` and ∀ for ``forall``. |Latex| + UTF-8 support can be found + at `<http://www.ctan.org/pkg/unicode>`_. For the interpretation of Unicode + characters by |Latex|, extra packages which coqdoc does not provide + by default might be required, such as textgreek for some Greek letters + or ``stmaryrd`` for some mathematical symbols. If a Unicode character is + missing an interpretation in the utf8x input encoding, add + ``\DeclareUnicodeCharacter{code}{LATEX-interpretation}``. Packages + and declarations can be added with option ``-p``. + :--inputenc string: Give a |Latex| input encoding, as an option to |Latex| + package ``inputenc``. + :--charset string: Specify the HTML character set, to be inserted in + the HTML header. + + + +The coqdoc |Latex| style file +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +In case you choose to produce a document without the default |Latex| +preamble (by using option ``--no-preamble``), then you must insert into +your own preamble the command + +:: + + \usepackage{coqdoc} + +The package optionally takes the argument ``[color]`` to typeset +identifiers with colors (this requires the ``xcolor`` package). + +Then you may alter the rendering of the document by redefining some +macros: + +:coqdockw, coqdocid, …: The one-argument macros for typesetting + keywords and identifiers. Defaults are sans-serif for keywords and + italic for identifiers.For example, if you would like a slanted font + for keywords, you may insert + + :: + + \renewcommand{\coqdockw}[1]{\textsl{#1}} + + + anywhere between ``\usepackage{coqdoc}`` and ``\begin{document}``. + + +:coqdocmodule: + One-argument macro for typesetting the title of a ``.v`` + file. Default is + + :: + + \newcommand{\coqdocmodule}[1]{\section*{Module #1}} + + and you may redefine it using ``\renewcommand``. diff --git a/doc/sphinx/using/tools/index.rst b/doc/sphinx/using/tools/index.rst index 4381c4d63d..dfe38dfce9 100644 --- a/doc/sphinx/using/tools/index.rst +++ b/doc/sphinx/using/tools/index.rst @@ -16,5 +16,6 @@ on the `Coq website <https://coq.inria.fr/user-interfaces.html>`_. ../../practical-tools/coq-commands ../../practical-tools/utilities + coqdoc ../../practical-tools/coqide ../../addendum/parallel-proof-processing diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index a51308f153..cb93a4c8cc 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -36,7 +36,8 @@ for k in $LIBDIRS; do fi else if [ $h = 0 ]; then - echo Warning: $k/$b.v will be hidden from the index + # Skipping file from the index + : else echo Error: none of $FILE and $HIDDEN mention $k/$b.v exit 1 diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 88a5217652..60b845c4be 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1125,10 +1125,6 @@ query_command: [ | WITH "SearchRewrite" constr_pattern in_or_out_modules | REPLACE "Search" searchabout_query searchabout_queries "." | WITH "Search" searchabout_query searchabout_queries -| REPLACE "SearchAbout" searchabout_query searchabout_queries "." -| WITH "SearchAbout" searchabout_query searchabout_queries -| REPLACE "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." -| WITH "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules ] vernac_toplevel: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 7032b238a6..272d17bb35 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1244,8 +1244,6 @@ query_command: [ | "SearchPattern" constr_pattern in_or_out_modules "." | "SearchRewrite" constr_pattern in_or_out_modules "." | "Search" searchabout_query searchabout_queries "." -| "SearchAbout" searchabout_query searchabout_queries "." -| "SearchAbout" "[" LIST1 searchabout_query "]" in_or_out_modules "." ] printable: [ diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index b600450675..0c9d7a853b 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -918,8 +918,6 @@ command: [ | "SearchPattern" one_term OPT ne_in_or_out_modules | "SearchRewrite" one_term OPT ne_in_or_out_modules | "Search" searchabout_query OPT searchabout_queries -| "SearchAbout" searchabout_query OPT searchabout_queries -| "SearchAbout" "[" LIST1 searchabout_query "]" OPT ne_in_or_out_modules | "Time" command | "Redirect" string command | "Timeout" num command diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index c5883cef0d..711986c2b2 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -207,7 +207,6 @@ let state_preserving = [ "Recursive Extraction Library"; "Search"; - "SearchAbout (* deprecated *)"; "SearchHead"; "SearchPattern"; "SearchRewrite"; diff --git a/ide/microPG.ml b/ide/microPG.ml index 46d3316ef6..5a4871b70a 100644 --- a/ide/microPG.ml +++ b/ide/microPG.ml @@ -289,7 +289,6 @@ let pg = insert pg "Proof General" [mC,_c,"c"; mC,_a,"a"] [ mkE _p "p" "Print" (Callback (fun gui -> command gui "Print")); mkE _c "c" "Check" (Callback (fun gui -> command gui "Check")); mkE _b "b" "About" (Callback (fun gui -> command gui "About")); - mkE _a "a" "Search About" (Callback (fun gui -> command gui "SearchAbout")); mkE _o "o" "Search Pattern" (Callback (fun gui->command gui "SearchPattern")); mkE _l "l" "Locate" (Callback (fun gui -> command gui "Locate")); mkE _Return "RET" "match template" (Action("Templates","match")); diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h deleted file mode 100644 index 38eda4d11f..0000000000 --- a/kernel/byterun/coq_gc.h +++ /dev/null @@ -1,59 +0,0 @@ -/***********************************************************************/ -/* */ -/* Coq Compiler */ -/* */ -/* Benjamin Gregoire, projets Logical and Cristal */ -/* INRIA Rocquencourt */ -/* */ -/* */ -/***********************************************************************/ - -#ifndef _COQ_CAML_GC_ -#define _COQ_CAML_GC_ -#include <caml/mlvalues.h> -#include <caml/alloc.h> -#include <caml/memory.h> - -typedef void (*scanning_action) (value, value *); - - -CAMLextern char *young_ptr; -CAMLextern char *young_limit; -CAMLextern void (*scan_roots_hook) (scanning_action); -CAMLextern void minor_collection (void); - -#define Caml_white (0 << 8) -#define Caml_black (3 << 8) - -#ifdef HAS_OCP_MEMPROF - -/* This code is necessary to make the OCamlPro memory profiling branch of - OCaml compile. */ - -#define Make_header(wosize, tag, color) \ - caml_make_header(wosize, tag, color) - -#else - -#define Make_header(wosize, tag, color) \ - (((header_t) (((header_t) (wosize) << 10) \ - + (color) \ - + (tag_t) (tag))) \ - ) -#endif - -#define Alloc_small(result, wosize, tag) do{ \ - young_ptr -= Bhsize_wosize (wosize); \ - if (young_ptr < young_limit){ \ - young_ptr += Bhsize_wosize (wosize); \ - Setup_for_gc; \ - minor_collection (); \ - Restore_after_gc; \ - young_ptr -= Bhsize_wosize (wosize); \ - } \ - Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ - (result) = Val_hp (young_ptr); \ - }while(0) - - -#endif /*_COQ_CAML_GC_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 606cce0127..7588c1ce07 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,17 +16,37 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <math.h> + +#define CAML_INTERNALS #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> -#include <math.h> -#include "coq_gc.h" + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" #include "coq_float64.h" +#if OCAML_VERSION < 41000 +extern void caml_minor_collection(void); + +#undef Alloc_small +#define Alloc_small(result, wosize, tag) do{ \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + if (caml_young_ptr < caml_young_limit) { \ + caml_young_ptr += Bhsize_wosize(wosize); \ + Setup_for_gc; \ + caml_minor_collection(); \ + Restore_after_gc; \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + } \ + Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \ + (result) = Val_hp(caml_young_ptr); \ + }while(0) +#endif + #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" #else diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 91d6773b1f..6233675c66 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,9 +10,12 @@ #include <stdio.h> #include <string.h> + +#define CAML_INTERNALS #include <caml/alloc.h> #include <caml/address_class.h> -#include "coq_gc.h" +#include <caml/roots.h> + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" diff --git a/kernel/float64.ml b/kernel/float64.ml index 299f53e8ab..53fc13b04b 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -21,12 +21,19 @@ let is_neg_infinity f = f = neg_infinity (* Printing a binary64 float in 17 decimal places and parsing it again will yield the same float. We assume [to_string_raw] is not given a - [nan] as input. *) + [nan] or an infinity as input. *) let to_string_raw f = Printf.sprintf "%.17g" f (* OCaml gives a sign to nan values which should not be displayed as - all NaNs are considered equal here *) -let to_string f = if is_nan f then "nan" else to_string_raw f + all NaNs are considered equal here. + OCaml prints infinities as "inf" (resp. "-inf") + but we want "infinity" (resp. "neg_infinity"). *) +let to_string f = + if is_nan f then "nan" + else if is_infinity f then "infinity" + else if is_neg_infinity f then "neg_infinity" + else to_string_raw f + let of_string = float_of_string (* Compiles a float to OCaml code *) diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index df6189f212..4b78e64d98 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -402,7 +402,7 @@ let rec interp_search_about args accu = match args with | [] -> accu | (flag, arg) :: rem -> fun gr env typ -> - let ans = Search.search_about_filter arg gr env typ in + let ans = Search.search_filter arg gr env typ in (if flag then ans else not ans) && interp_search_about rem accu gr env typ let interp_search_arg arg = diff --git a/plugins/syntax/float_syntax.ml b/plugins/syntax/float_syntax.ml index dadce9a9ea..e0a9906689 100644 --- a/plugins/syntax/float_syntax.ml +++ b/plugins/syntax/float_syntax.ml @@ -22,8 +22,56 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) (*** Parsing for float in digital notation ***) +let warn_inexact_float = + CWarnings.create ~name:"inexact-float" ~category:"parsing" + (fun (sn, f) -> + Pp.strbrk + (Printf.sprintf + "The constant %s is not a binary64 floating-point value. \ + A closest value will be used and unambiguously printed %s." + sn (Float64.to_string f))) + let interp_float ?loc n = - DAst.make ?loc (GFloat (Float64.of_string (NumTok.Signed.to_string n))) + let sn = NumTok.Signed.to_string n in + let f = Float64.of_string sn in + (* return true when f is not exactly equal to n, + this is only used to decide whether or not to display a warning + and does not play any actual role in the parsing *) + let inexact () = match Float64.classify f with + | Float64.(PInf | NInf | NaN) -> true + | Float64.(PZero | NZero) -> not (NumTok.Signed.is_zero n) + | Float64.(PNormal | NNormal | PSubn | NSubn) -> + let m, e = + let (_, i), f, e = NumTok.Signed.to_decimal_and_exponent n in + let i = NumTok.UnsignedNat.to_string i in + let f = match f with + | None -> "" | Some f -> NumTok.UnsignedNat.to_string f in + let e = match e with + | None -> "0" | Some e -> NumTok.SignedNat.to_string e in + Bigint.of_string (i ^ f), + (try int_of_string e with Failure _ -> 0) - String.length f in + let m', e' = + let m', e' = Float64.frshiftexp f in + let m' = Float64.normfr_mantissa m' in + let e' = Uint63.to_int_min e' 4096 - Float64.eshift - 53 in + Bigint.of_string (Uint63.to_string m'), + e' in + let c2, c5 = Bigint.(of_int 2, of_int 5) in + (* check m*5^e <> m'*2^e' *) + let check m e m' e' = + not (Bigint.(equal (mult m (pow c5 e)) (mult m' (pow c2 e')))) in + (* check m*5^e*2^e' <> m' *) + let check' m e e' m' = + not (Bigint.(equal (mult (mult m (pow c5 e)) (pow c2 e')) m')) in + (* we now have to check m*10^e <> m'*2^e' *) + if e >= 0 then + if e <= e' then check m e m' (e' - e) + else check' m e (e - e') m' + else (* e < 0 *) + if e' <= e then check m' (-e) m (e - e') + else check' m' (-e) (e' - e) m in + if inexact () then warn_inexact_float ?loc (sn, f); + DAst.make ?loc (GFloat f) (* Pretty printing is already handled in constrextern.ml *) diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index e0dc3d8989..c4e9c8b73d 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -134,7 +134,38 @@ let r_of_rawnum ?loc n = (* Printing R via scopes *) (**********************************************************************) -let rawnum_of_r c = match DAst.get c with +let rawnum_of_r c = + (* print i * 10^e, precondition: e <> 0 *) + let numTok_of_int_exp i e = + (* choose between 123e-2 and 1.23, this is purely heuristic + and doesn't play any soundness role *) + let choose_exponent = + if Bigint.is_strictly_pos e then + true (* don't print 12 * 10^2 as 1200 to distinguish them *) + else + let i = Bigint.to_string i in + let li = if i.[0] = '-' then String.length i - 1 else String.length i in + let e = Bigint.neg e in + let le = String.length (Bigint.to_string e) in + Bigint.(less_than (add (of_int li) (of_int le)) e) in + (* print 123 * 10^-2 as 123e-2 *) + let numTok_exponent () = NumTok.Signed.of_bigint_and_exponent i e in + (* print 123 * 10^-2 as 1.23, precondition e < 0 *) + let numTok_dot () = + let s, i = + if Bigint.is_pos_or_zero i then NumTok.SPlus, Bigint.to_string i + else NumTok.SMinus, Bigint.(to_string (neg i)) in + let ni = String.length i in + let e = - (Bigint.to_int e) in + assert (e > 0); + let i, f = + if e < ni then String.sub i 0 (ni - e), String.sub i (ni - e) e + else "0", String.make (e - ni) '0' ^ i in + let i = s, NumTok.UnsignedNat.of_string i in + let f = NumTok.UnsignedNat.of_string f in + NumTok.Signed.of_decimal_and_exponent i (Some f) None in + if choose_exponent then numTok_exponent () else numTok_dot () in + match DAst.get c with | GApp (r, [a]) when is_gr r glob_IZR -> let n = bigint_of_z a in NumTok.Signed.of_bigint n @@ -151,7 +182,7 @@ let rawnum_of_r c = match DAst.get c with let i = bigint_of_z l in let e = bignat_of_pos e in let e = if is_gr md glob_Rdiv then neg e else e in - NumTok.Signed.of_bigint_and_exponent i e + numTok_of_int_exp i e | _ -> raise Non_closed_number end | _ -> raise Non_closed_number diff --git a/test-suite/bugs/closed/HoTT_coq_010.v b/test-suite/bugs/closed/HoTT_coq_010.v index 42b1244fb5..caa7373f5e 100644 --- a/test-suite/bugs/closed/HoTT_coq_010.v +++ b/test-suite/bugs/closed/HoTT_coq_010.v @@ -1,3 +1,3 @@ -SearchAbout and. +Search and. (* Anomaly: Mismatched instance and context when building universe substitution. Please report. *) diff --git a/test-suite/bugs/closed/bug_3900.v b/test-suite/bugs/closed/bug_3900.v index 6be2161c2f..ddede74acc 100644 --- a/test-suite/bugs/closed/bug_3900.v +++ b/test-suite/bugs/closed/bug_3900.v @@ -9,5 +9,5 @@ Variable Pmor : forall s d : obj, morphism A (projT1 s) (projT1 d) -> Type. Class Foo (x : Type) := { _ : forall y, y }. Local Instance ishset_pmor {s d m} : Foo (Pmor s d m). Proof. -SearchAbout ((forall _ _, _) -> Foo _). +Search ((forall _ _, _) -> Foo _). Abort. diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out index cfd6633752..dd8189c56f 100644 --- a/test-suite/output/FloatExtraction.out +++ b/test-suite/output/FloatExtraction.out @@ -1,3 +1,17 @@ +File "stdin", line 25, characters 8-12: +Warning: The constant 0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed 0.01. [inexact-float,parsing] +File "stdin", line 25, characters 20-25: +Warning: The constant -0.01 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed -0.01. [inexact-float,parsing] +File "stdin", line 25, characters 27-35: +Warning: The constant 1.7e+308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 1.6999999999999999e+308. +[inexact-float,parsing] +File "stdin", line 25, characters 37-46: +Warning: The constant -1.7e-308 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-1.7000000000000002e-308. [inexact-float,parsing] (** val infinity : Float64.t **) diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out index 668a55977d..7941d2e647 100644 --- a/test-suite/output/FloatSyntax.out +++ b/test-suite/output/FloatSyntax.out @@ -4,8 +4,16 @@ : float (-2.5)%float : float +File "stdin", line 9, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123%float : float +File "stdin", line 10, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] (-2.5000000000000001e-123)%float : float (2 + 2)%float @@ -18,14 +26,34 @@ : float -2.5 : float +File "stdin", line 19, characters 6-13: +Warning: The constant 2.5e123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed 2.4999999999999999e+123. +[inexact-float,parsing] 2.4999999999999999e+123 : float +File "stdin", line 20, characters 7-16: +Warning: The constant -2.5e-123 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed +-2.5000000000000001e-123. [inexact-float,parsing] -2.5000000000000001e-123 : float 2 + 2 : float 2.5 + 2.5 : float +File "stdin", line 24, characters 6-11: +Warning: The constant 1e309 is not a binary64 floating-point value. A closest +value will be used and unambiguously printed infinity. +[inexact-float,parsing] +infinity + : float +File "stdin", line 25, characters 6-12: +Warning: The constant -1e309 is not a binary64 floating-point value. A +closest value will be used and unambiguously printed neg_infinity. +[inexact-float,parsing] +neg_infinity + : float 2 : nat 2%float diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v index 85f611352c..eca712db10 100644 --- a/test-suite/output/FloatSyntax.v +++ b/test-suite/output/FloatSyntax.v @@ -21,6 +21,9 @@ Check (-2.5e-123). Check (2 + 2). Check (2.5 + 2.5). +Check 1e309. +Check -1e309. + Open Scope nat_scope. Check 2. diff --git a/test-suite/output/QArithSyntax.out b/test-suite/output/QArithSyntax.out index 6bc04f1cef..fe6a1d25c6 100644 --- a/test-suite/output/QArithSyntax.out +++ b/test-suite/output/QArithSyntax.out @@ -1,14 +1,14 @@ -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 1020 = 1020 : 1020 = 1020 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index ebc272d9af..1685964b0f 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -2,21 +2,21 @@ : R (-31)%R : R -15e-1%R +1.5%R : R 15%R : R -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 -eq_refl : 102e-1 = 102e-1 - : 102e-1 = 102e-1 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 +eq_refl : 10.2 = 10.2 + : 10.2 = 10.2 eq_refl : 102e1 = 102e1 : 102e1 = 102e1 eq_refl : 102 = 102 : 102 = 102 -eq_refl : 102e-2 = 102e-2 - : 102e-2 = 102e-2 +eq_refl : 1.02 = 1.02 + : 1.02 = 1.02 eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 -eq_refl : -50e-2 = -50e-2 - : -50e-2 = -50e-2 +eq_refl : -0.50 = -0.50 + : -0.50 = -0.50 diff --git a/test-suite/success/search.v b/test-suite/success/search.v new file mode 100644 index 0000000000..92de43e052 --- /dev/null +++ b/test-suite/success/search.v @@ -0,0 +1,35 @@ + +(** Test of the different syntaxes of Search *) + +Search plus. +Search plus mult. +Search "plus_n". +Search plus "plus_n". +Search "*". +Search "*" "+". + +Search plus inside Peano. +Search plus mult inside Peano. +Search "plus_n" inside Peano. +Search plus "plus_n" inside Peano. +Search "*" inside Peano. +Search "*" "+" inside Peano. + +Search plus outside Peano Logic. +Search plus mult outside Peano Logic. +Search "plus_n" outside Peano Logic. +Search plus "plus_n" outside Peano Logic. +Search "*" outside Peano Logic. +Search "*" "+" outside Peano Logic. + +Search -"*" "+" outside Logic. +Search -"*"%nat "+"%nat outside Logic. + + +(** The example in the Reference Manual *) + +Require Import ZArith. + +Search Z.mul Z.add "distr". +Search "+"%Z "*"%Z "distr" -positive -Prop. +Search (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v deleted file mode 100644 index 9edfd82556..0000000000 --- a/test-suite/success/searchabout.v +++ /dev/null @@ -1,60 +0,0 @@ - -(** Test of the different syntaxes of SearchAbout, in particular - with and without the [ ... ] delimiters *) - -SearchAbout plus. -SearchAbout plus mult. -SearchAbout "plus_n". -SearchAbout plus "plus_n". -SearchAbout "*". -SearchAbout "*" "+". - -SearchAbout plus inside Peano. -SearchAbout plus mult inside Peano. -SearchAbout "plus_n" inside Peano. -SearchAbout plus "plus_n" inside Peano. -SearchAbout "*" inside Peano. -SearchAbout "*" "+" inside Peano. - -SearchAbout plus outside Peano Logic. -SearchAbout plus mult outside Peano Logic. -SearchAbout "plus_n" outside Peano Logic. -SearchAbout plus "plus_n" outside Peano Logic. -SearchAbout "*" outside Peano Logic. -SearchAbout "*" "+" outside Peano Logic. - -SearchAbout -"*" "+" outside Logic. -SearchAbout -"*"%nat "+"%nat outside Logic. - -SearchAbout [plus]. -SearchAbout [plus mult]. -SearchAbout ["plus_n"]. -SearchAbout [plus "plus_n"]. -SearchAbout ["*"]. -SearchAbout ["*" "+"]. - -SearchAbout [plus] inside Peano. -SearchAbout [plus mult] inside Peano. -SearchAbout ["plus_n"] inside Peano. -SearchAbout [plus "plus_n"] inside Peano. -SearchAbout ["*"] inside Peano. -SearchAbout ["*" "+"] inside Peano. - -SearchAbout [plus] outside Peano Logic. -SearchAbout [plus mult] outside Peano Logic. -SearchAbout ["plus_n"] outside Peano Logic. -SearchAbout [plus "plus_n"] outside Peano Logic. -SearchAbout ["*"] outside Peano Logic. -SearchAbout ["*" "+"] outside Peano Logic. - -SearchAbout [-"*" "+"] outside Logic. -SearchAbout [-"*"%nat "+"%nat] outside Logic. - - -(** The example in the Reference Manual *) - -Require Import ZArith. - -SearchAbout Z.mul Z.add "distr". -SearchAbout "+"%Z "*"%Z "distr" -positive -Prop. -SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas. diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 10c3baa2cd..855db8bc3f 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -156,6 +156,37 @@ Definition nztail_int d := | Neg d => let (r, n) := nztail d in pair (Neg r) n end. +(** [del_head n d] removes [n] digits at beginning of [d] + or returns [zero] if [d] has less than [n] digits. *) + +Fixpoint del_head n d := + match n with + | O => d + | S n => + match d with + | Nil => zero + | D0 d | D1 d | D2 d | D3 d | D4 d | D5 d | D6 d | D7 d | D8 d | D9 d => + del_head n d + end + end. + +Definition del_head_int n d := + match d with + | Pos d => Pos (del_head n d) + | Neg d => Neg (del_head n d) + end. + +(** [del_tail n d] removes [n] digits at end of [d] + or returns [zero] if [d] has less than [n] digits. *) + +Fixpoint del_tail n d := rev (del_head n (rev d)). + +Definition del_tail_int n d := + match d with + | Pos d => Pos (del_tail n d) + | Neg d => Neg (del_tail n d) + end. + Module Little. (** Successor of little-endian numbers *) diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 6126d9c37d..71ba3e645d 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -43,5 +43,5 @@ Numeral Notation nat Nat.of_uint Nat.to_uint : nat_scope (abstract after 5001). (* Printing/Parsing of bytes *) Export Byte.ByteSyntaxNotations. -(* Default substrings not considered by queries like SearchAbout *) +(* Default substrings not considered by queries like Search *) Add Search Blacklist "_subproof" "_subterm" "Private_". diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index a7f338aec3..bd5225d9ef 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -44,13 +44,39 @@ Definition of_decimal (d:Decimal.decimal) : Q := end. Definition to_decimal (q:Q) : option Decimal.decimal := + (* choose between 123e-2 and 1.23, this is purely heuristic + and doesn't play any soundness role *) + let choose_exponent i ne := + let i := match i with Decimal.Pos i | Decimal.Neg i => i end in + let li := Decimal.nb_digits i in + let le := Decimal.nb_digits (Nat.to_uint ne) in + Nat.ltb (Nat.add li le) ne in + (* print 123 / 100 as 123e-2 *) + let decimal_exponent i ne := + let e := Z.to_int (Z.opp (Z.of_nat ne)) in + Decimal.DecimalExp i Decimal.Nil e in + (* print 123 / 100 as 1.23 *) + let decimal_dot i ne := + let ai := match i with Decimal.Pos i | Decimal.Neg i => i end in + let ni := Decimal.nb_digits ai in + if Nat.ltb ne ni then + let i := Decimal.del_tail_int ne i in + let f := Decimal.del_head (Nat.sub ni ne) ai in + Decimal.Decimal i f + else + let z := match i with + | Decimal.Pos _ => Decimal.Pos (Decimal.zero) + | Decimal.Neg _ => Decimal.Neg (Decimal.zero) end in + Decimal.Decimal z (Nat.iter (Nat.sub ne ni) Decimal.D0 ai) in let num := Z.to_int (Qnum q) in let (den, e_den) := Decimal.nztail (Pos.to_uint (Qden q)) in match den with | Decimal.D1 Decimal.Nil => - match Z.of_nat e_den with - | Z0 => Some (Decimal.Decimal num Decimal.Nil) - | e => Some (Decimal.DecimalExp num Decimal.Nil (Z.to_int (Z.opp e))) + match e_den with + | O => Some (Decimal.Decimal num Decimal.Nil) + | ne => + if choose_exponent num ne then Some (decimal_exponent num ne) + else Some (decimal_dot num ne) end | _ => None end. diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d2b0078a7c..862715753d 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -42,7 +42,7 @@ let is_keyword = "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes"; "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; - "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite"; + "Search"; "SearchHead"; "SearchPattern"; "SearchRewrite"; "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context"; "Notation"; "Reserved Notation"; "Tactic Notation"; "Delimit"; "Bind"; "Open"; "Scope"; "Inline"; diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index dd75693c5b..a8f1a49086 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -983,13 +983,6 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchRewrite c,g, l) } | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } - (* compatibility: SearchAbout *) - | IDENT "SearchAbout"; s = searchabout_query; l = searchabout_queries; "." -> - { fun g -> let (sl,m) = l in VernacSearch (SearchAbout (s::sl),g, m) } - (* compatibility: SearchAbout with "[ ... ]" *) - | IDENT "SearchAbout"; "["; sl = LIST1 searchabout_query; "]"; - l = in_or_out_modules; "." -> - { fun g -> VernacSearch (SearchAbout sl,g, l) } ] ] ; printable: diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index a3de88d4dc..054b60853f 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -142,7 +142,7 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search_about (b,c) = + let pr_search (b,c) = (if b then str "-" else mt()) ++ match c with | SearchSubPattern p -> @@ -158,10 +158,8 @@ open Pputils | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b - | SearchAbout sl -> - keyword "SearchAbout" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b let pr_option_ref_value = function | QualidRefValue id -> pr_qualid id diff --git a/vernac/search.ml b/vernac/search.ml index ceff8acc79..68a30b4231 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -23,8 +23,8 @@ module NamedDecl = Context.Named.Declaration type filter_function = GlobRef.t -> env -> constr -> bool type display_function = GlobRef.t -> env -> constr -> unit -(* This option restricts the output of [SearchPattern ...], -[SearchAbout ...], etc. to the names of the symbols matching the +(* This option restricts the output of [SearchPattern ...], etc. +to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) @@ -226,7 +226,7 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_about_filter query gr env typ = match query with +let search_filter query gr env typ = match query with | GlobSearchSubPattern pat -> Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) | GlobSearchString s -> @@ -283,14 +283,14 @@ let search_by_head ?pstate gopt pat mods pr_search = in generic_search ?pstate gopt iter -(** SearchAbout *) +(** Search *) -let search_about ?pstate gopt items mods pr_search = +let search ?pstate gopt items mods pr_search = let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && List.for_all - (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items && + (fun (b,i) -> eqb b (search_filter i ref env typ)) items && blacklist_filter ref env typ in let iter ref env typ = diff --git a/vernac/search.mli b/vernac/search.mli index 11dd0c6794..6dbbff3a8c 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -30,8 +30,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_about_filter : glob_search_about_item -> filter_function -(** Check whether a reference matches a SearchAbout query. *) +val search_filter : glob_search_about_item -> filter_function (** {6 Specialized search functions} @@ -45,7 +44,7 @@ val search_rewrite : ?pstate:Proof_global.t -> int option -> constr_pattern -> D -> display_function -> unit val search_pattern : ?pstate:Proof_global.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_about : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list +val search : ?pstate:Proof_global.t -> int option -> (bool * glob_search_about_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8641c67d9f..963b5f2084 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1773,10 +1773,6 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } -let warn_deprecated_search_about = - CWarnings.create ~name:"deprecated-search-about" ~category:"deprecated" - (fun () -> strbrk "The SearchAbout command is deprecated. Please use Search instead.") - let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in @@ -1809,12 +1805,8 @@ let vernac_search ~pstate ~atts s gopt r = (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchAbout sl -> - warn_deprecated_search_about (); - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> - Search.prioritize_search) pr_search | Search sl -> - (Search.search_about ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search); Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b7c6d3c490..d6e7a3947a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -69,7 +69,6 @@ type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | SearchAbout of (bool * search_about_item) list | Search of (bool * search_about_item) list type locatable = |