aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile/timing
Commit message (Collapse)AuthorAge
* Convert timing tools to run with both python2 and python3Gravatar Jasper Hugunin2018-07-04
|
* [ci] Fix another issue with the timing testsGravatar Jason Gross2018-04-26
| | | | | There was recently a spurious failure on AppVeyor (I've forgotten which PR). This commit fixes that particular failure.
* Improve shell scriptsGravatar zapashcanon2018-04-05
|
* Update coq_makefile timing testGravatar Jason Gross2018-04-02
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This fixes #5675 (in yet another way). The issue was that `$` (end of string regex) was not properly escaped in `"`s. This handles the issue that is displayed in ``` cat A.v.timing.diff After | Code | Before || Change | % Change --------------------------------------------------------------------------------------------------- 0m01.44s | Total | 0m01.56s || -0m00.12s | -7.92% --------------------------------------------------------------------------------------------------- 0m00.609s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m00.627s || -0m00.01s | -2.87% 0m00.527s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.552s || -0m00.02s | -4.52% 0m00.304s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.379s || -0m00.07s | -19.78% N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.006s || -0m00.00s | -100.00% 0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A --- A.v.timing.diff.desired.processed 2018-03-23 22:22:19.000000000 +0000 +++ A.v.timing.diff.processed 2018-03-23 22:22:19.000000000 +0000 @@ -1,4 +1,4 @@ - N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | N/A + N/A | Chars 27 - 68 [Declare~Reduction~comp~:=~nati] | ms || -ms | -% ------ ------ After | Code | Before || Change | % Change ``` where, because `Declare Reduction` takes 0.006s rather than 0s, the % change shows up as -100% rather than N/A.
* [test-suite] Move sed scripts into bash arraysGravatar Jason Gross2018-02-24
| | | | As per https://github.com/coq/coq/pull/6756/files#r168028764
* Fix issue with spurious timing test failuresGravatar Jason Gross2018-02-13
| | | | | | | When none of the numbers get over 100, the width of the table was different. See https://github.com/coq/coq/pull/6736#issuecomment-365386802
* Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Maxime Dénès2018-01-08
|\
* | Trim more trailing whitespace in coq-makefile timing testGravatar Jason Gross2017-12-31
| | | | | | | | | | | | | | Should help with https://github.com/coq/coq/issues/5675#issuecomment-353604702 Also replace a tab with spaces
| * Add TIMING_SORT_BY and --sort-by to timing scriptsGravatar Jason Gross2017-12-27
|/ | | | | This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292
* Do dependencies in 1 command per file class.Gravatar Gaëtan Gilbert2017-12-15
|
* Add test-suite tests for timing scriptsGravatar Jason Gross2017-11-22
| | | | | | | | | | | | | | | | | | | | | 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)
* Have the coq_makefile timing test-suite print moreGravatar Jason Gross2017-11-17
| | | | | | This should help debug things like https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they ever show up again.
* Handle ∞ in coq-makefile timing test-suiteGravatar Jason Gross2017-10-19
| | | | This should (hopefully) fix #5675.
* Add timing scriptsGravatar Jason Gross2017-07-11
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 09:02:26 +0000