The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.ens-cachan.fr>]

Hi, I'm generating big Coq proofs automatically,
which use 'fix' a lot across Remarks with transparent
proofs.  To state what's happening to me, Coq seems
to get stuck at the end of a Remark called rem_2421
at line 32969 --- numbers to give an idea of size.
Arrived here, it seems to process the closing 'Defined'
indefinitely.  I have been waiting for 11 minutes
already.  This already happened earlier in the same file,
but is getting more and more of a problem as Coq
advances in it (it is stuck at roughly 5% of the file).
        I strongly suspect that Coq is lost checking
for the guard conditions in the terms.  After all,
my Coq process is 57360 Kb big at this point, is
only 8136 Kb at startup, and the rest (~ 50 Mb) is
roughly just one big lambda-term.

        Is this a known problem with fix?

        Is there a way to speed it up, apart
from changing my Coq proof generation algorithm?
(An option that I've now almost exhausted.)

        I can provide the example at will, but
emailing it would be a breach of etiquette.  Of
course I cannot make any smaller example: size seems
precisely to be the problem.

        Best,


        -- Jean Goubault-Larrecq
        (LSV/ENS Cachan & CNRS UMR 8643 & INRIA projet SECSI).