diff options
| author | glondu | 2010-04-10 19:06:58 +0000 |
|---|---|---|
| committer | glondu | 2010-04-10 19:06:58 +0000 |
| commit | e2196880cfb406b56c829c7ed552107fa9dcb8b7 (patch) | |
| tree | c39d8e63fd7aa77aa753f76095579dd8d87a43a2 /dev | |
| parent | 1e3da6528560c8df6458ac2ec32e0971babbbdee (diff) | |
Makefile for the test-suite
Using a Makefile for tests allows (easily) running them in parallel,
running and/or benching a single one, adding depedencies between them,
and running them with a version of Coq different than the one compiled
with the current source tree. The new way to make statistics about
successes/failures is also more reliable (I found bugs in the previous
one).
Statistics (on AMD Phenom(tm) 9950 Quad-Core Processor 2.6 GHz):
- plain sh script: ~ 3 min
- make -j6: ~ 1 min
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12921 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions