coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-09-21	Make print-pretty-timed robust against non-output-sync logs	Jason Gross
	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
2020-05-21	Fix an uncaught python exception in timing	Jason Gross
	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
2020-05-20	Print a newline at the end of timing tables	Jason Gross
	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.
2020-04-24	Add memory stats to tables by default	Jason Gross
	The Python scripts now support `--no-include-mem` to turn it off, and also support `--sort-by-mem`. Closes #11575
2020-02-05	Add --fuzz, --real, --user to timing scripts	Jason Gross
	- 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
2019-03-31	[pretty-timing scripts] Don't barf on non-utf-8	Jason Gross
	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.
2019-03-31	[pretty-print py]Don't print sys.stdout;better utf	Jason Gross
	This should fix #9705 I'm kind-of cargo-cult coding here, from things like https://docs.python.org/3/library/sys.html#sys.displayhook and https://github.com/coq/coq/issues/9705#issuecomment-471996313, but hopefully this fixes the issue without breaking anything. (I am really a novice when it comes to the str/bytes distinction in python3.)
2019-03-04	remove unused import of os	Frédéric Chapoton
	found by lgtm https://lgtm.com/projects/g/coq/coq/
2018-07-11	Merge PR #8002: make-both-single-timing-files: fix --sort-by=diff	Jason Gross

2018-07-07	make diff sort by difference, not absolute difference	Ralf Jung

2018-07-07	make-both-single-timing-files: fix --sort-by=diff	Ralf Jung

2018-07-07	Output UTF-8 explicitly in timing tools	Jasper Hugunin

2018-07-04	Convert timing tools to run with both python2 and python3	Jasper Hugunin

2017-12-27	Add TIMING_SORT_BY and --sort-by to timing scripts	Jason Gross
	This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
2017-11-22	Update TimeFileMaker.py to correctly sort timing diffs	Jason Gross
	Previously, it was reverse-ordering timing diffs.
2017-10-06	TimeFileMaker.py: Allow trailing spaces	Jason Gross
	This allows the timing aggregation scripts to handle logs from Travis, which, for some reason, seems to insert trailing spaces.
2017-07-11	Add timing scripts	Jason Gross
	This commit adds timing scripts from https://github.com/JasonGross/coq-scripts/tree/master/timing into the tools folder, and integrates them into coq_makefile and Coq's makefile. The main added makefile targets are: - the `TIMING` variable - when non-empty, this creates for each built `.v` file a `.v.timing` variable (or `.v.before-timing` or `.v.after-timing` for `TIMING=before` and `TIMING=after`, respectively) - `pretty-timed TGTS=...` - runs `make $(TGTS)` and prints a table of sorted timings at the end, saving it to `time-of-build-pretty.log` - `make-pretty-timed-before TGTS=...`, `make-pretty-timed-after TGTS=...` - runs `make $(TGTS)`, and saves the timing data to the file `time-of-build-before.log` or `time-of-build-after.log`, respectively - `print-pretty-timed-diff` - prints a table with the difference between the logs recorded by `make-pretty-timed-before` and `make-pretty-timed-after`, saving the table to `time-of-build-both.log` - `print-pretty-single-time-diff BEFORE=... AFTER=...` - this prints a table with the differences between two `.v.timing` files, and saves the output to `time-of-build-pretty.log` - `.v.timing.diff` - this saves the result of `print-pretty-single-time-diff` for each target to the `.v.timing.diff` file - `all.timing.diff` (`world.timing.diff` and `coq.timing.diff` in Coq's own Makefile) - makes all `.v.timing.diff` targets N.B. We need to make `make pretty-timed` fail if `make` fails. To do this, we need to get around the fact that pipes swallow exit codes. There are a few solutions in https://stackoverflow.com/questions/23079651/equivalent-of-pipefail-in-gnu-make; we choose the temporary file rather than requiring the shell of the makefile to be bash.