diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/README.md | 2 | ||||
| -rw-r--r-- | doc/changelog/02-specification-language/11600-uniform-syntax.rst | 4 | ||||
| -rw-r--r-- | doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst | 8 | ||||
| -rw-r--r-- | doc/changelog/08-tools/11302-better-timing-scripts-options.rst | 35 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/11350-list.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 50 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 | ||||
| -rw-r--r-- | doc/stdlib/dune | 4 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 180 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 10 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 2 | ||||
| -rw-r--r-- | doc/tools/coqrst/notations/sphinx.py | 2 |
14 files changed, 212 insertions, 113 deletions
diff --git a/doc/README.md b/doc/README.md index ef3ccc2105..7fa6f5cf3d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -96,7 +96,7 @@ Alternatively, you can use some specific targets: - `make refman-{html,pdf}` to produce only one format of the reference manual -- `make stdlib` +- `make doc-stdlib` to produce all formats of the Coq standard library diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst new file mode 100644 index 0000000000..3fa3f80301 --- /dev/null +++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst @@ -0,0 +1,4 @@ +- **Added:** + New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which + parameters of an inductive are uniform. + (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert). diff --git a/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst new file mode 100644 index 0000000000..b105928b22 --- /dev/null +++ b/doc/changelog/03-notations/11530-master+fix11331-custom-entries-precedence.rst @@ -0,0 +1,8 @@ +- **Fixed:** + Bugs in dealing with precedences of notations in custom entries + (`#11530 <https://github.com/coq/coq/pull/11530>`_, + by Hugo Herbelin, fixing in particular + `#9517 <https://github.com/coq/coq/pull/9517>`_, + `#9519 <https://github.com/coq/coq/pull/9519>`_, + `#9521 <https://github.com/coq/coq/pull/9521>`_, + `#11331 <https://github.com/coq/coq/pull/11331>`_). diff --git a/doc/changelog/08-tools/11302-better-timing-scripts-options.rst b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst new file mode 100644 index 0000000000..3b20bbf75d --- /dev/null +++ b/doc/changelog/08-tools/11302-better-timing-scripts-options.rst @@ -0,0 +1,35 @@ +- **Added:** + The ``make-both-single-timing-files.py`` script now accepts a + ``--fuzz=N`` parameter on the command line which determines how many + characters two lines may be offset in the "before" and "after" + timing logs while still being considered the same line. When + invoking this script via the ``print-pretty-single-time-diff`` + target in a ``Makefile`` made by ``coq_makefile``, you can set this + argument by passing ``TIMING_FUZZ=N`` to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + The ``make-one-time-file.py`` and ``make-both-time-files.py`` + scripts now accept a ``--real`` parameter on the command line to + print real times rather than user times in the tables. The + ``make-both-single-timing-files.py`` script accepts a ``--user`` + parameter to use user times. When invoking these scripts via the + ``print-pretty-timed`` or ``print-pretty-timed-diff`` or + ``print-pretty-single-time-diff`` targets in a ``Makefile`` made by + ``coq_makefile``, you can set this argument by passing + ``TIMING_REAL=1`` (to pass ``--real``) or ``TIMING_REAL=0`` (to pass + ``--user``) to ``make`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Added:** + Coq's build system now supports both ``TIMING_FUZZ``, + ``TIMING_SORT_BY``, and ``TIMING_REAL`` just like a ``Makefile`` + made by ``coq_makefile`` (`#11302 + <https://github.com/coq/coq/pull/11302>`_, by Jason Gross). + +- **Fixed:** + The various timing targets for Coq's standard library now correctly + display and label the "before" and "after" columns, rather than + mixing them up (`#11302 <https://github.com/coq/coq/pull/11302>`_ + fixes `#11301 <https://github.com/coq/coq/issues/11301>`_, by Jason + Gross). diff --git a/doc/changelog/10-standard-library/11350-list.rst b/doc/changelog/10-standard-library/11350-list.rst new file mode 100644 index 0000000000..52c2517161 --- /dev/null +++ b/doc/changelog/10-standard-library/11350-list.rst @@ -0,0 +1,5 @@ +- **Added:** + ``remove'`` and ``count_occ'`` over lists, + alternatives to ``remove`` and ``count_occ`` based on ``filter`` + (`#11350 <https://github.com/coq/coq/pull/11350>`_, + by Yishuai Li). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 721c7a7a51..7ce4538a4d 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1063,8 +1063,17 @@ Parameterized inductive types | cons3 : A -> list3 -> list3. End list3. - Attributes ``uniform`` and ``nonuniform`` respectively enable and - disable uniform parameters for a single inductive declaration block. + For finer control, you can use a ``|`` between the uniform and + the non-uniform parameters: + + .. coqtop:: in reset + + Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop + := Acc_in : (forall y, R y x -> Acc y) -> Acc x. + + The flag can then be seen as deciding whether the ``|`` is at the + beginning (when the flag is unset) or at the end (when it is set) + of the parameters when not explicitly given. .. seealso:: Section :ref:`inductive-definitions` and the :tacn:`induction` tactic. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..179dff9959 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -255,14 +255,20 @@ file timing data: one, you can pass them via the variable ``TGTS``, e.g., ``make pretty-timed TGTS="a.vo b.vo"``. - .. :: + .. note:: This target requires ``python`` to build the table. .. note:: This target will *append* to the timing log; if you want a - fresh start, you must remove the ``filetime-of-build.log`` or + fresh start, you must remove the file ``time-of-build.log`` or ``run make cleanall``. + .. note:: + By default the table displays user times. If the build log + contains real times (which it does by default), passing + ``TIMING_REAL=1`` to ``make pretty-timed`` will use real times + rather than user times in the table. + .. example:: For example, the output of ``make pretty-timed`` may look like this: @@ -310,6 +316,15 @@ file timing data: (which are frequently noise); lexicographic sorting forces an order on files which take effectively no time to compile. + If you prefer a different sorting order, you can pass + ``TIMING_SORT_BY=absolute`` to sort by the total time taken, or + ``TIMING_SORT_BY=diff`` to sort by the signed difference in + time. + + .. note:: + Just like ``pretty-timed``, this table defaults to using user + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. + .. example:: For example, the output table from @@ -349,7 +364,7 @@ line timing data: :: - print-pretty-single-time-diff BEFORE=path/to/file.v.before-timing AFTER=path/to/file.v.after-timing + print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing this target will make a sorted table of the per-line timing differences between the timing logs in the ``BEFORE`` and ``AFTER`` files, display it, and @@ -364,6 +379,28 @@ line timing data: .. note:: This target requires python to build the table. + .. note:: + This target follows the same sorting order as the + ``print-pretty-timed-diff`` target, and supports the same + options for the ``TIMING_SORT_BY`` variable. + + .. note:: + By default, two lines are only considered the same if the + character offsets and initial code strings are identical. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character locations to differ by up to ``N``, as long + as the total number of characters and initial code strings + continue to match. This is useful when there are small changes + to a file, and you want to match later lines that have not + changed even though the character offsets have changed. + + .. note:: + By default the table picks up real times, under the assumption + that when comparing line-by-line, the real time is a more + accurate representation as it includes disk time and time spent + in the native compiler. Passing ``TIMING_REAL=0`` to ``make`` + will use user times rather than real times in the table. + .. example:: For example, running ``print-pretty-single-time-diff`` might give a table like this: @@ -545,7 +582,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +591,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 36a5916868..2fa4f1fa42 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality: :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). - These are defined in theories/Init/Logic.v. The "where" clauses define the + These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c388..a8d5ac610f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -798,7 +798,13 @@ associated to the custom entry ``expr``. The level can be omitted, as in Notation "[ e ]" := e (e custom expr). -in which case Coq tries to infer it. +in which case Coq infer it. If the sub-expression is at a border of +the notation (as e.g. ``x`` and ``y`` in ``x + y``), the level is +determined by the associativity. If the sub-expression is not at the +border of the notation (as e.g. ``e`` in ``"[ e ]``), the level is +inferred to be the highest level used for the entry. In particular, +this level depends on the highest level existing in the entry at the +time of use of the notation. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to diff --git a/doc/stdlib/dune b/doc/stdlib/dune index 828caecabc..093c7a62b2 100644 --- a/doc/stdlib/dune +++ b/doc/stdlib/dune @@ -5,7 +5,6 @@ (deps make-library-index index-list.html.template hidden-files (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib)) (action (chdir %{project_root} @@ -17,7 +16,6 @@ (deps ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg (source_tree %{project_root}/theories) - (source_tree %{project_root}/plugins) (source_tree %{project_root}/user-contrib) (:header %{project_root}/doc/common/styles/html/coqremote/header.html) (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) @@ -26,7 +24,7 @@ (action (progn (run mkdir -p html) - (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/plugins %{project_root}/user-contrib -name *.v)") + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -Q %{project_root}/user-contrib/Ltac2 Ltac2 $(find %{project_root}/theories %{project_root}/user-contrib -name *.v)") (run mv html/index.html html/genindex.html) (with-stdout-to _index.html diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index dbc3a42ee9..60d6039b0f 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1,90 +1,90 @@ -plugins/btauto/Algebra.v -plugins/btauto/Btauto.v -plugins/btauto/Reflect.v -plugins/derive/Derive.v -plugins/extraction/ExtrHaskellBasic.v -plugins/extraction/ExtrHaskellNatInt.v -plugins/extraction/ExtrHaskellNatInteger.v -plugins/extraction/ExtrHaskellNatNum.v -plugins/extraction/ExtrHaskellString.v -plugins/extraction/ExtrHaskellZInt.v -plugins/extraction/ExtrHaskellZInteger.v -plugins/extraction/ExtrHaskellZNum.v -plugins/extraction/ExtrOcamlBasic.v -plugins/extraction/ExtrOcamlBigIntConv.v -plugins/extraction/ExtrOcamlChar.v -plugins/extraction/ExtrOCamlInt63.v -plugins/extraction/ExtrOCamlFloats.v -plugins/extraction/ExtrOcamlIntConv.v -plugins/extraction/ExtrOcamlNatBigInt.v -plugins/extraction/ExtrOcamlNatInt.v -plugins/extraction/ExtrOcamlString.v -plugins/extraction/ExtrOcamlNativeString.v -plugins/extraction/ExtrOcamlZBigInt.v -plugins/extraction/ExtrOcamlZInt.v -plugins/extraction/Extraction.v -plugins/funind/FunInd.v -plugins/funind/Recdef.v -plugins/ltac/Ltac.v -plugins/micromega/Ztac.v -plugins/micromega/DeclConstant.v -plugins/micromega/Env.v -plugins/micromega/EnvRing.v -plugins/micromega/Fourier.v -plugins/micromega/Fourier_util.v -plugins/micromega/Lia.v -plugins/micromega/Lqa.v -plugins/micromega/Lra.v -plugins/micromega/MExtraction.v -plugins/micromega/OrderedRing.v -plugins/micromega/Psatz.v -plugins/micromega/QMicromega.v -plugins/micromega/RMicromega.v -plugins/micromega/Refl.v -plugins/micromega/RingMicromega.v -plugins/micromega/Tauto.v -plugins/micromega/VarMap.v -plugins/micromega/ZCoeff.v -plugins/micromega/ZMicromega.v -plugins/micromega/ZifyInst.v -plugins/micromega/ZifyBool.v -plugins/micromega/ZifyComparison.v -plugins/micromega/ZifyClasses.v -plugins/micromega/Zify.v -plugins/nsatz/Nsatz.v -plugins/omega/Omega.v -plugins/omega/OmegaLemmas.v -plugins/omega/OmegaPlugin.v -plugins/omega/OmegaTactic.v -plugins/omega/PreOmega.v -plugins/quote/Quote.v -plugins/romega/ROmega.v -plugins/romega/ReflOmegaCore.v -plugins/rtauto/Bintree.v -plugins/rtauto/Rtauto.v -plugins/setoid_ring/Algebra_syntax.v -plugins/setoid_ring/ArithRing.v -plugins/setoid_ring/BinList.v -plugins/setoid_ring/Cring.v -plugins/setoid_ring/Field.v -plugins/setoid_ring/Field_tac.v -plugins/setoid_ring/Field_theory.v -plugins/setoid_ring/InitialRing.v -plugins/setoid_ring/Integral_domain.v -plugins/setoid_ring/NArithRing.v -plugins/setoid_ring/Ncring.v -plugins/setoid_ring/Ncring_initial.v -plugins/setoid_ring/Ncring_polynom.v -plugins/setoid_ring/Ncring_tac.v -plugins/setoid_ring/RealField.v -plugins/setoid_ring/Ring.v -plugins/setoid_ring/Ring_base.v -plugins/setoid_ring/Ring_polynom.v -plugins/setoid_ring/Ring_tac.v -plugins/setoid_ring/Ring_theory.v -plugins/setoid_ring/Rings_Q.v -plugins/setoid_ring/Rings_R.v -plugins/setoid_ring/Rings_Z.v -plugins/setoid_ring/ZArithRing.v -plugins/ssr/ssrunder.v -plugins/ssr/ssrsetoid.v +theories/btauto/Algebra.v +theories/btauto/Btauto.v +theories/btauto/Reflect.v +theories/derive/Derive.v +theories/extraction/ExtrHaskellBasic.v +theories/extraction/ExtrHaskellNatInt.v +theories/extraction/ExtrHaskellNatInteger.v +theories/extraction/ExtrHaskellNatNum.v +theories/extraction/ExtrHaskellString.v +theories/extraction/ExtrHaskellZInt.v +theories/extraction/ExtrHaskellZInteger.v +theories/extraction/ExtrHaskellZNum.v +theories/extraction/ExtrOcamlBasic.v +theories/extraction/ExtrOcamlBigIntConv.v +theories/extraction/ExtrOcamlChar.v +theories/extraction/ExtrOCamlInt63.v +theories/extraction/ExtrOCamlFloats.v +theories/extraction/ExtrOcamlIntConv.v +theories/extraction/ExtrOcamlNatBigInt.v +theories/extraction/ExtrOcamlNatInt.v +theories/extraction/ExtrOcamlString.v +theories/extraction/ExtrOcamlNativeString.v +theories/extraction/ExtrOcamlZBigInt.v +theories/extraction/ExtrOcamlZInt.v +theories/extraction/Extraction.v +theories/funind/FunInd.v +theories/funind/Recdef.v +theories/ltac/Ltac.v +theories/micromega/Ztac.v +theories/micromega/DeclConstant.v +theories/micromega/Env.v +theories/micromega/EnvRing.v +theories/micromega/Fourier.v +theories/micromega/Fourier_util.v +theories/micromega/Lia.v +theories/micromega/Lqa.v +theories/micromega/Lra.v +theories/micromega/MExtraction.v +theories/micromega/OrderedRing.v +theories/micromega/Psatz.v +theories/micromega/QMicromega.v +theories/micromega/RMicromega.v +theories/micromega/Refl.v +theories/micromega/RingMicromega.v +theories/micromega/Tauto.v +theories/micromega/VarMap.v +theories/micromega/ZCoeff.v +theories/micromega/ZMicromega.v +theories/micromega/ZifyInst.v +theories/micromega/ZifyBool.v +theories/micromega/ZifyComparison.v +theories/micromega/ZifyClasses.v +theories/micromega/Zify.v +theories/nsatz/Nsatz.v +theories/omega/Omega.v +theories/omega/OmegaLemmas.v +theories/omega/OmegaPlugin.v +theories/omega/OmegaTactic.v +theories/omega/PreOmega.v +theories/quote/Quote.v +theories/romega/ROmega.v +theories/romega/ReflOmegaCore.v +theories/rtauto/Bintree.v +theories/rtauto/Rtauto.v +theories/setoid_ring/Algebra_syntax.v +theories/setoid_ring/ArithRing.v +theories/setoid_ring/BinList.v +theories/setoid_ring/Cring.v +theories/setoid_ring/Field.v +theories/setoid_ring/Field_tac.v +theories/setoid_ring/Field_theory.v +theories/setoid_ring/InitialRing.v +theories/setoid_ring/Integral_domain.v +theories/setoid_ring/NArithRing.v +theories/setoid_ring/Ncring.v +theories/setoid_ring/Ncring_initial.v +theories/setoid_ring/Ncring_polynom.v +theories/setoid_ring/Ncring_tac.v +theories/setoid_ring/RealField.v +theories/setoid_ring/Ring.v +theories/setoid_ring/Ring_base.v +theories/setoid_ring/Ring_polynom.v +theories/setoid_ring/Ring_tac.v +theories/setoid_ring/Ring_theory.v +theories/setoid_ring/Rings_Q.v +theories/setoid_ring/Rings_R.v +theories/setoid_ring/Rings_Z.v +theories/setoid_ring/ZArithRing.v +theories/ssr/ssrunder.v +theories/ssr/ssrsetoid.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index b2ddf36b65..51688e2d9e 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -619,11 +619,11 @@ through the <tt>Require Import</tt> command.</p> small scale reflection formalization technique </dt> <dd> - plugins/ssrmatching/ssrmatching.v - plugins/ssr/ssrclasses.v - plugins/ssr/ssreflect.v - plugins/ssr/ssrbool.v - plugins/ssr/ssrfun.v + theories/ssrmatching/ssrmatching.v + theories/ssr/ssrclasses.v + theories/ssr/ssreflect.v + theories/ssr/ssrbool.v + theories/ssr/ssrfun.v </dd> <dt> <b>Ltac2</b>: diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 732f15b78a..a51308f153 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,7 +8,7 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -LIBDIRS=`find theories/* plugins/* user-contrib/* -type d ! -name .coq-native` +LIBDIRS=`find theories/* user-contrib/* -type d ! -name .coq-native` for k in $LIBDIRS; do if [[ $k =~ "user-contrib" ]]; then diff --git a/doc/tools/coqrst/notations/sphinx.py b/doc/tools/coqrst/notations/sphinx.py index ab18d136b8..5659a64b84 100644 --- a/doc/tools/coqrst/notations/sphinx.py +++ b/doc/tools/coqrst/notations/sphinx.py @@ -80,9 +80,11 @@ class TacticNotationsToSphinxVisitor(TacticNotationsVisitor): while atom != "": if atom[0] == "'": node += nodes.raw("\\textquotesingle{}", "\\textquotesingle{}", format="latex") + node += nodes.raw("'", "'", format="html") atom = atom[1:] elif atom[0] == "`": node += nodes.raw("\\`{}", "\\`{}", format="latex") + node += nodes.raw("`", "`", format="html") atom = atom[1:] else: index_ap = atom.find("'") |