| Age | Commit message (Collapse) | Author |
|---|
|
Also pass `--output-sync` on the CI, as suggested in
https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect
against this failure mode.
Fixes #13062
|
|
Previously, when either the 'before' or 'after' had no files, we'd get
an uncaught exception:
```
Traceback (most recent call last):
File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in <module>
table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem)
File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string
right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values())
ValueError: max() arg is an empty sequence
```
Fixes #12387
|
|
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.
|
|
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.
Closes #11575
|
|
- 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
|
|
Reviewed-by: ppedrot
|
|
Closes #10491
We re-add the header in doc/tools/coqrst/notations/fontsupport.py
which was removed by accident in 1a9c769ed363ee2f2784e7252af72e6c1e2fbcc6
The fontsupport script itself has been kept for reference, however it
is not involved by any build target as of today.
|
|
This should have been running already, but it was forgotten in #9872
|
|
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
|
|
|
|
|
|
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)
|
