The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

We have a Coq development that extracts to about 20,000 lines of OCaml 
code.  For some reason, running [Recursive Extraction] on the main 
definition takes several hours, and I'm writing to see if anyone has any 
insight into why.  (We're using Coq 8.4pl2.)

My guess is that the blame belongs with the most unusual aspect of this 
development: it involves many functors (in the module-system sense).

Specifically, we want to build what is conceptually just a single 
functor, parameterizing a whole development over a few values.  However, 
we want to divide the code amongst some tens of files, for engineering 
reasons.  Each file that depends on other files contains a top-level 
functor whose body starts by instantiating other functors from the 
dependencies, with essentially the same parameters.  Many files contain 
multiple nested invocations of other functors.

Could there be some nasty performance scaling that is superlinear in the 
pattern of functor-application nesting?  We also see surprisingly high 
run time for other related commands, like [End] to finish a functor 
definition; but such commands are still orders of magnitude faster than 
recursive extraction (about a minute instead of several hours).