diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 43 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 8 |
4 files changed, 59 insertions, 7 deletions
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 3d1fc6d4b9..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: 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 |