Folder structure

Stream: new members

[Martin Dvořák]

Hello! I want an advice. Do I use a good folder structure in my project that is supposed to grow into a large codebase in the future?
https://github.com/madvorak/grammars/

I will appreciate any tips from experienced LEANers.

I am also not sure whether it is convenient to have large files like this one.
https://github.com/madvorak/grammars/blob/main/src/cfgClosureUnion.lean

There is one theorem (the class of context-free languages is closed under union) and basically everything else serves for proving this theorem (auxiliary definitions and lemmata). Would it be better to have a separate folder for the one theorem and split the file into several files? For example into four files:
1) main theorem
2) proof of the first inclusion
3) proof of the second inclusion
4) common parts referenced by both 2 and 3

Or, would such a granularity make my project less clearly organized in the future, when the main issue becomes the amount of files in the project (rather than the amount of lines in a file) later?

[Cameron Torrance]

I've also been having similar problems figuring out how organise my personal project. Taking some inspiration from mathlib I'm trying to assign to ever major mathematical object I define a folder with at least the following structure : a folder/file for each non trivial component of the definition, a file called basic that defines the object and morphisms, and some trivial results are proven, a folder called instances where I define examples of the object, and folders (with the structure currently described) for gadgets associated with the object.

Whist this is easier to work with than giant file I used to have, here are a few problems I've been having with this structure:
1) Things can morally live in more than one place, should the category of open sets live in the topology folder or category theory folder?
2) Sometimes imports don't play nice with this structure. In my ideals folder I had a file for basic identities involving ideals, ideally (ha!) this would also include identities involving the radical but my definition the radical depended on results from this file.
3) I don't really know how medium sized proofs like the ones in your project fix into this file structure, proofs long enough that they ruin the flow of a file but doesn't like it deserves a file of its own . A super long proof whose elements morally live together would get a file or folder of its own but I don't really know how I'd structure this folder.

[Martin Dvořák]

As an experiment, I refactored the abovementioned proof into 4 files.
https://github.com/madvorak/grammars/tree/granularity/src/context_free/cfgUnderUnion

Do you think it looks better (on this branch) now?