The Coq mailing list

[Jim Fehrle <jfehrle AT sbcglobal.net>]

> fortunately, my VST proof development is itself much more efficient, so therefore I can do big things with a large collection of .v files that each take no more than 1 gigabyte (and usually much less) to process with coqc.

Sounds like a memory leak.  Directly or indirectly, I expect you have to Require all of the .v files for final proof in the series, and you've not mentioned problems with that.  So the compiled-then-loaded form of the .v files is not taking too much memory.  https://realworldocaml.org/v1/en/html/understanding-the-garbage-collector.html says that both the major and minor heaps use compaction, so heap fragmentation shouldn't be an issue either.

Are you using a separate coqc process to compile each .v?  If you compile many .v files in one coqc process, does it run out of memory?