The Coq mailing list

[Christophe Dehlinger <dehlinger AT dpt-info.u-strasbg.fr>]

Hello everyone,

I'm currently working on a fairly large development in Coq. Compilation
delays are becoming an issue: compiling the whole specification takes
about 20 minutes so far. One of the main problems comes from tactic
Auto: while it is very useful when you do not want to delve into
the sometimes tedious details of simple proofs,
Auto is often quite slow, especially when many hints can be applied
to the current goal. The problem is that each time the
specification is compiled, Coq has to perform this Prolog-like resolution
for each subgoal solved with Auto. These resolution delays add up quite 
fast,
so much that I usually end up solving simple properties by hand in
order to avoid Auto and thus reduce compilation time.

Basically, what I would like Coq to do is to perform this resolution only 
once,
when the goal is originally solved in interactive mode.
One way to achieve this would be by designing a vernacular command that
would perform the same Prolog-like resolution as Auto but that does not
affect the goal,  and instead produces a script that solves the goal.
This script could then be played to solve the goal. The script
would mainly feature "Intro" and "Apply" tactics, which are compiled very 
fast.
Of course, the downside is that the whole lemma script would be
less readable and less adaptable; moreover this method is likely to be 
useless
when Auto is applied to several goals at the same time through the ";"
construct. But this would save much, much time when there is only a single
goal, which occurs very often (at least in my specification).

Maybe there is already a way to do this or something similar,
if so please let me know.

Christophe Dehlinger