The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Hello,
With the questions about benchmarking and also space and time 
consumption, it is hard to
resist making the following suggestion: it might be really very useful 
for writing tactics
if Coq could have an internal time measurement system. That is to say it 
would be good to
have a counter that says how long it takes to run, but such that the 
counter is in the software rather
than dependent on hardware: the same computation should give the same 
time value on any different
machine. Then you could envision an Ltac which says, ``try ... for time 
T and fail if it doesn't work in time T''.
The reason that this would be interesting is that somebody (maybe 
Raffali?) said that for automation,
what is important is tactics that fail rapidly. One often encounters 
tactics which
have the property that when they are applied in the right situation they 
produce the answer relatively
quickly, but when they are not appropriate they take a long time to fail 
(e.g. try assumption in an enormous
context on a complicated goal, when there is no assumption that works 
but maybe several that look sort of
like they might work). Rewriting is another good example: if you try 
rewriting with a rule which doesn't apply,
sometimes the machine sits there for quite a while before deciding that 
it doesn't work. This is of course a
disaster for auto-rewrite. On the other hand, if you had an internal 
timing mechanism then you could
do ``auto-rewrite with .., .., .., .., timeout = 100'' and it would try 
rewriting with the given tactics, failing
when they time out. This might considerably improve the utility of 
things like auto-rewrite (or other similar tactics
that one could write).
---Carlos