diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-05-11 12:30:15 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-06-05 22:09:40 -0400 |
| commit | 51b32595081d279624c8ec162f9ed686ed660d9b (patch) | |
| tree | 5f66e017b653d2fc6e83acf627b08a4e1df328dd /tools/coqc.ml | |
| parent | b9b8e5d4305b7a37b1cae364756834fd60d58fb6 (diff) | |
Remove a spurious tclFINALLY when not profiling
Implement the suggestion of @mattam82 to check whether or not we're
profiling before inserting the tclFINALLY.
Timing stats:
Using:
```bash
make clean && git clean -xfd && ./configure -local -with-doc no -coqide no && /usr/bin/time -f "all coq (real: %e, user: %U, sys: %S, mem: %M ko)" make STDTIME='/usr/bin/time -f "$* (real: %e, user: %U, sys: %S, mem: %M ko)"' TIMED=1 -j4 2>&1
```
Without LtacProf (4c078b0362542908eb2fe1d63f0d867b339953fd), two runs:
```
real: 147.96, user: 467.93, sys: 30.80, mem: 820468 ko
real: 148.04, user: 467.92, sys: 30.49, mem: 820680 ko
```
With LtacProf, two runs:
```
real: 148.32, user: 469.09, sys: 30.57, mem: 818588 ko
real: 148.38, user: 469.71, sys: 30.56, mem: 816720 ko
```
Overall overhead on building Coq: about 0.24%
Differences in the slowest files:
```
After | File Name | Before || Change
---------------------------------------------------------------------------
7m07.32s | Total | 7m05.16s || +0m02.15s
---------------------------------------------------------------------------
0m44.90s | Numbers/Rational/BigQ/QMake | 0m44.11s || +0m00.78s
0m15.94s | plugins/setoid_ring/Ncring_polynom | 0m15.72s || +0m00.21s
0m14.04s | Numbers/Cyclic/DoubleCyclic/DoubleCyclic | 0m14.05s || -0m00.01s
0m10.65s | Numbers/Cyclic/DoubleCyclic/DoubleSqrt | 0m10.45s || +0m00.20s
0m09.57s | FSets/FMapAVL | 0m09.53s || +0m00.04s
0m09.51s | MSets/MSetRBT | 0m09.45s || +0m00.06s
0m07.00s | Numbers/Cyclic/DoubleCyclic/DoubleDiv | 0m07.05s || -0m00.04s
0m06.88s | Numbers/Cyclic/Int31/Cyclic31 | 0m06.94s || -0m00.06s
0m05.82s | plugins/setoid_ring/Field_theory | 0m05.87s || -0m00.04s
0m05.74s | FSets/FMapFullAVL | 0m05.71s || +0m00.03s
0m05.37s | Reals/Ratan | 0m05.42s || -0m00.04s
0m05.36s | plugins/setoid_ring/Ring_polynom | 0m05.37s || -0m00.00s
0m05.09s | plugins/micromega/EnvRing | 0m04.96s || +0m00.12s
```
Diffstat (limited to 'tools/coqc.ml')
0 files changed, 0 insertions, 0 deletions