Stream: Coq users

Topic: How to organize large file


view this post on Zulip walker (Jul 07 2023 at 10:06):

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.

view this post on Zulip Gaëtan Gilbert (Jul 07 2023 at 10:32):

see also https://gitlab.inria.fr/flocq/flocq/-/blob/master/src/Pff/Pff.v

view this post on Zulip Karl Palmskog (Jul 07 2023 at 10:35):

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.

view this post on Zulip Karl Palmskog (Jul 07 2023 at 10:38):

there is no guide other recipe to my knowledge, I think it's all closely analogous to regular PL and their "monster classes"

view this post on Zulip Paolo Giarrusso (Jul 07 2023 at 11:14):

coq-lsp should limit replaying proofs unless their dependencies changed — but I don't know if this already works across files (sounds hard)

view this post on Zulip Karl Palmskog (Jul 07 2023 at 11:26):

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

view this post on Zulip Karl Palmskog (Jul 07 2023 at 11:30):

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.

view this post on Zulip Théo Zimmermann (Jul 07 2023 at 12:31):

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: Jun 13 2024 at 19:02 UTC