[Termtools] time limits

[Claude Marché]

About time limits:

The rules for this year state that "the time limit is likely to be
between 1 and 5 minutes" 

I think it is important that tools are not tuned to a fixed time
limit, but should adapt their strategy to the time limit given as
argument. Think that your tools are available to everyone, and one may
want to use your tools on a particular problem for a much longer
time. So if jambox does not behave well with 120 s: it is its fault.

Time limit 120s is indeed the CPU time limit, and the wall clock time
limit is set to 1.5 times this limit, that is 3 minutes. Time
consumption are computed as accurately as I could, that is they
clearly wrong sometimes: sorry, but I am unable to measure them
correctly with tools that spawn subprocesses, ans run on
multi-processor machines.

Time limit for checkme is fixed by my engine to 5 times the time limit
for the runme, so it is 10 minutes CPU and 15 minutes wall clock. It
explains why the proof requiring 20 minutes or more are rejected. I
see this as a good motivation to make generated Coq scripts run faster!

-- 
Claude Marché                          | tel: +33 1 72 92 59 69           
INRIA Futurs - ProVal                  | mobile: +33 6 33 14 57 93 
Parc Orsay Université - ZAC des Vignes | fax: +33 1 74 85 42 29   
3, rue Jacques Monod - Bâtiment N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |