From 6799ad6240fa4d233f698c3cfa0bd5417f471bba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Dec 2019 15:14:24 -0500 Subject: Add --fuzz, --real, --user to timing scripts - Add a `--fuzz` option to `make-both-single-timing-files.py` Passing `--fuzz=N` allows differences in character locations of up to `N` characters when matching lines in per-line timing diffs. The corresponding variable for `coq_makefile` is `TIMING_FUZZ=N`. See also the discussion at https://github.com/coq/coq/pull/11076#pullrequestreview-324791139 - Allow passing `--real` to per-file timing scripts and `--user` to per-line timing script. This allows easily comparing real times instead of user ones (or vice versa). - Support `TIMING_SORT_BY` and `TIMING_FUZZ` in Coq's own build - We also now use argparse rather than a hand-rolled argument parser; there were getting to be too many combinations of options. - Fix the ordering of columns in Coq's build system; this is the equivalent of #8167 for Coq's build system. Fixes #11301 Supersedes / closes #11022 Supersedes / closes #11230 --- .../11302-better-timing-scripts-options.rst | 35 +++++++++++++++++ doc/sphinx/practical-tools/utilities.rst | 44 ++++++++++++++++++++-- 2 files changed, 76 insertions(+), 3 deletions(-) create mode 100644 doc/changelog/08-tools/11302-better-timing-scripts-options.rst (limited to 'doc') 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 + `_, 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 + `_, 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 + `_, 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 `_ + fixes `#11301 `_, by Jason + Gross). diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..64a4716188 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 picks up 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,16 @@ 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 and supports ``TIMING_REAL=1`` to specify that real times + rather than user times should be used. + .. example:: For example, the output table from @@ -349,7 +365,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 +380,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 match. Passing + ``TIMING_FUZZ=N`` relaxes this constraint by allowing the + character offsets to differ by up to ``N`` characters, 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: -- cgit v1.2.3 From 53f6560f766fdbb7176eb7247c712c690f4a6f1f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 6 Feb 2020 23:14:33 -0500 Subject: Apply suggestions from code review Co-Authored-By: Jim Fehrle --- doc/sphinx/practical-tools/utilities.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 64a4716188..24b766b204 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -264,7 +264,7 @@ file timing data: ``run make cleanall``. .. note:: - By default the table picks up user times. If the build log + 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. @@ -387,7 +387,7 @@ line timing data: .. note:: By default, two lines are only considered the same if the - character offsets and initial code strings match. Passing + character offsets and initial code strings are identical. Passing ``TIMING_FUZZ=N`` relaxes this constraint by allowing the character offsets to differ by up to ``N`` characters, as long as the total number of characters and initial code strings -- cgit v1.2.3 From 82ab894460fb25d85acf8c4ce0d177ecc4dbfd86 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 11 Feb 2020 17:07:39 -0500 Subject: Update doc/sphinx/practical-tools/utilities.rst --- doc/sphinx/practical-tools/utilities.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 24b766b204..626a658b6c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -389,7 +389,7 @@ line timing data: 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 offsets to differ by up to ``N`` characters, as long + 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 -- cgit v1.2.3 From f9928b83a2e2eda7bbb9cd7fac0ea6e1ef1be30f Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 14 Feb 2020 17:26:49 -0500 Subject: Apply suggestions from code review Co-Authored-By: Jim Fehrle --- doc/sphinx/practical-tools/utilities.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 626a658b6c..23b7dcfeba 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -323,8 +323,7 @@ file timing data: .. note:: Just like ``pretty-timed``, this table defaults to using user - times and supports ``TIMING_REAL=1`` to specify that real times - rather than user times should be used. + times. Pass ``TIMING_REAL=1`` to ``make`` on the command line to show real times instead. .. example:: -- cgit v1.2.3