<feed xmlns='http://www.w3.org/2005/Atom'>
<title>coq/test-suite/coq-makefile/timing/before/_CoqProject, branch master</title>
<subtitle>The formal proof system</subtitle>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/'/>
<entry>
<title>Add timing scripts</title>
<updated>2017-07-11T09:32:44+00:00</updated>
<author>
<name>Jason Gross</name>
</author>
<published>2017-06-07T17:33:42+00:00</published>
<link rel='alternate' type='text/html' href='https://git.0x7felf.com/coq/commit/?id=62b8d99f1430a8a477d36be86d91aba8807659db'/>
<id>62b8d99f1430a8a477d36be86d91aba8807659db</id>
<content type='text'>
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.
</content>
<content type='xhtml'>
<div xmlns='http://www.w3.org/1999/xhtml'>
<pre>
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.
</pre>
</div>
</content>
</entry>
</feed>
