diff options
| author | Jason Gross | 2019-12-17 15:14:24 -0500 |
|---|---|---|
| committer | Jason Gross | 2020-02-05 16:55:28 -0500 |
| commit | 6799ad6240fa4d233f698c3cfa0bd5417f471bba (patch) | |
| tree | 1653b06a6ee2e712ed4fc57eae4b0f08a9da3bca /.gitignore | |
| parent | c2f0b3c6c6942d8821ce05759b6940bd77435602 (diff) | |
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
Diffstat (limited to '.gitignore')
| -rw-r--r-- | .gitignore | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/.gitignore b/.gitignore index b99d2a0d45..489e6211a7 100644 --- a/.gitignore +++ b/.gitignore @@ -64,12 +64,9 @@ plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so coqdoc.sty coqdoc.css -time-of-build.log -time-of-build-pretty.log -time-of-build-before.log -time-of-build-after.log -time-of-build-pretty.log2 -time-of-build-pretty.log3 +time-of-build*.log +time-of-build*.log2 +time-of-build*.log3 .csdp.cache test-suite/.lia.cache test-suite/.nra.cache |