aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitlab-ci.yml
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-06-07 13:33:42 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-07-11 05:32:44 -0400
commit62b8d99f1430a8a477d36be86d91aba8807659db (patch)
tree2731d35a4707a3a5dd274e295a1834613803897a /.gitlab-ci.yml
parentb65671f342265351a40c910c7b170c4e6924197d (diff)
Add timing scripts
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.
Diffstat (limited to '.gitlab-ci.yml')
-rw-r--r--.gitlab-ci.yml7
1 files changed, 6 insertions, 1 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index e1feabd06..95928d7bd 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -21,6 +21,8 @@ variables:
COMPILER_BLEEDING_EDGE: "4.04.1"
CAMLP5_VER_BLEEDING_EDGE: "6.17"
+ TEST_PACKAGES: "time python"
+
COQIDE_PACKAGES: "libgtk2.0-dev libgtksourceview2.0-dev"
#COQIDE_PACKAGES_32BIT: "libgtk2.0-dev:i386 libgtksourceview2.0-dev:i386"
COQIDE_OPAM: "lablgtk-extras"
@@ -193,6 +195,8 @@ test-suite:
<<: *test-suite-template
dependencies:
- build
+ variables:
+ EXTRA_PACKAGES: "$TEST_PACKAGES"
test-suite:32bit:
<<: *test-suite-template
@@ -200,7 +204,7 @@ test-suite:32bit:
- build:32bit
variables:
COMPILER: "$COMPILER_32BIT"
- EXTRA_PACKAGES: "gcc-multilib"
+ EXTRA_PACKAGES: "gcc-multilib $TEST_PACKAGES"
test-suite:bleeding-edge:
<<: *test-suite-template
@@ -209,6 +213,7 @@ test-suite:bleeding-edge:
variables:
COMPILER: "$COMPILER_BLEEDING_EDGE"
CAMLP5_VER: "$CAMLP5_VER_BLEEDING_EDGE"
+ EXTRA_PACKAGES: "$TEST_PACKAGES"
documentation:
<<: *documentation-template