| Age | Commit message (Collapse) | Author |
|---|
|
|
|
The Python scripts now support `--no-include-mem` to turn it off, and
also support `--sort-by-mem`.
Closes #11575
|
|
We fix
```
Makefile.build:222: warning: undefined variable '*'
```
by not passing a time format including a Makefile variable when not
inside a target (and whether or not the command succeeds should not
depend on the particular format in any case, and all we are testing for
is whether or not the command exists and supports `-f`).
|
|
|
|
Fixes #8158
|
|
There was recently a spurious failure on AppVeyor (I've forgotten which
PR). This commit fixes that particular failure.
|
|
|
|
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.
|
|
As per https://github.com/coq/coq/pull/6756/files#r168028764
|
|
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
|
|
|
|
Should help with
https://github.com/coq/coq/issues/5675#issuecomment-353604702
Also replace a tab with spaces
|
|
This should help with #5675, in particular with
https://github.com/coq/coq/issues/5675#issuecomment-349716292
|
|
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)
|
|
This should help debug things like
https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they
ever show up again.
|
|
This should (hopefully) fix #5675.
|
|
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.
|
