The file in question is some properties about lists, mainly base on mathcomp and complementing it with stuff about lists that is not in the mathcomp library.
I copy pasted the whole file into pastebin for demonstration, the
problem vscoq + this file does not play well, it takes couple of minutes to seek to the end of the file, I guess because the file is too big ?
ALso everytime I add a new lemma or type to this file It ends up recompiling everything because basically everything depends on some lemmas on this file.
I thought about splitting it into sub file: like lemmas for zip
, lemmas for PIn
.... etc but then it becomes clear where lemmas about both zip
and PIn
fit.
So is there a well known guideline for how to split bit theory files into smaller concise ones ?
The file in question:
https://pastebin.com/xackxWdL
The bigger problem is the file will always be growing, because there will always be that extra property about lists that one can add and later use.
see also https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/Pff/Pff.v
the way people usually handle large files of utility results is to split into small files by theme, and then introduce some new file that only contains Export
for the split files.
there is no guide other recipe to my knowledge, I think it's all closely analogous to regular PL and their "monster classes"
coq-lsp should limit replaying proofs unless their dependencies changed — but I don't know if this already works across files (sounds hard)
in a theoretical future where we have semantically organized code not tied to a filesystem representation, I think it'd be fine to collect stuff in huge chunks around vague themes. But currently, people use Git and filesystems, all arguably tied to Unix-style hierarchical organization, so 27k+ LOC files are typically really hard to maintain and hinder file-level parallelism, the most common way to speed up Coq builds
in most of the "real-world" Coq repos we looked at for some proof engineering research, people tended to do modifications all across the project in a commit, not just in a single place. This makes file-level parallelism + change impact analysis like timestamps really effective, whereas with the monster file you have to recompile the whole thing every time.
Paolo Giarrusso said:
coq-lsp should limit replaying proofs unless their dependencies changed — but I don't know if this already works across files (sounds hard)
I think this is one of the goals of fcc (https://github.com/ejgallego/coq-lsp/pull/507), but I do not know if this is really implemented yet (the commit introducing it says "caching (which is not yet very exploited)").
Last updated: Oct 13 2024 at 01:02 UTC