coq/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting, branch master The formal proof system Print a newline at the end of timing tables 2020-05-20T19:23:14+00:00 Jason Gross 2020-05-19T20:09:47+00:00 0f8de9b967fe82ef8e9eef5e258d9ef96788929e This, for example, improves the CI display, so that `$ echo 'end:coq.test'` does not appear on the same line as the end of the timing table. 
This, for example, improves the CI display, so that `$ echo
'end:coq.test'` does not appear on the same line as the end of the
timing table.
Add memory stats to tables by default 2020-04-24T21:22:33+00:00 Jason Gross 2020-02-14T21:57:13+00:00 d8d0e1164b81d0968c31373de58f8c74bd47119b The Python scripts now support `--no-include-mem` to turn it off, and also support `--sort-by-mem`. Closes #11575 
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.

Closes #11575
Add --fuzz, --real, --user to timing scripts 2020-02-05T21:55:28+00:00 Jason Gross 2019-12-17T20:14:24+00:00 6799ad6240fa4d233f698c3cfa0bd5417f471bba - 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 
- 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
Convert timing tools to run with both python2 and python3 2018-07-04T21:12:17+00:00 Jasper Hugunin 2018-07-04T18:23:13+00:00 c47a7e4f27baa2203da748ca9f927f9bc17ccd8d 






Add test-suite tests for timing scripts
2017-11-22T21:20:00+00:00

Jason Gross

2017-11-22T17:27:34+00:00

e87c3f9da4dbc3b876e2662c122c17141b7feae5

These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).

They are meant to serve as human-readable sanity checks of output
format.

Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).

N.B. The test-suite removes all *.log files, so we use *.log.in.

N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.

N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)





These work on precomputed build logs (in this case, from a recent
partial build of fiat-crypto).

They are meant to serve as human-readable sanity checks of output
format.

Separate out the sane bits of template/init.sh from the ones messing
with directory structure (which are fragile and make assumptions about
where the calling script is sourcing it from).

N.B. The test-suite removes all *.log files, so we use *.log.in.

N.B. We set COQLIB in precomputed-time-tests/run.sh, not the Makefile,
because coqc, on Windows, doesn't handle cygwin paths passed via
-coqlib, and `pwd` gives cygwin paths.

N.B. We have .gitattributes to satisfy the linter (as per
https://github.com/coq/coq/pull/6149#issuecomment-346410990)