Too many "mathlib" folders

[kbuzzard]

Why do we have ForMathlib, FromMathlib, Mathlib and MathlibExperiments as well as HIMExperiments. I should sort all of these out!

[kbuzzard]

claim

[YaelDillies]

Since you are interested in trying out my Mathlib folder workflow, let me explain it in depth using the two main projects I use it for: APAP and CamCombi. Here are the relevant excerpts of their respective README:

• APAP:

  The Lean code is contained in the directory LeanAPAP. The subdirectories are:

  • Mathlib: Material missing from existing mathlib developments
  • Prereqs: New developments to be integrated to mathlib

• CamCombi:

  The Lean code is located within the LeanCamCombi folder. Within it, one can find:

  • One subfolder for each course, [...]
  • A Mathlib subfolder for the prerequisites to be upstreamed to mathlib. Lemmas that belong in an existing mathlib file Mathlib.X will be located in LeanCamCombi.Mathlib.X. We aim to preserve the property that LeanCamCombi.Mathlib.X only imports Mathlib.X and files of the form LeanCamCombi.Mathlib.Y where Mathlib.X (transitively) imports Mathlib.Y. Prerequisites that do not belong in any existing mathlib file are placed in subtheory folders. See below.
  • One folder for each theory development. The formal lecture transcripts only contain what was stated in the lectures, but sometimes it makes sense for a theory to be developed as a whole before being incorporated by the prerequisites or imported in the formal lecture transcripts.
  • An Archive subfolder for archived results. [...]

Both of them have a MyProject.Mathlib folder with strict entry requirements:

• File MyProject.Mathlib.X can only exist if Mathlib.X exists already
• File MyProject.Mathlib.X can only import files Mathlib.X and MyProject.Mathlib.Y where Mathlib.X (transitively) imports Mathlib.Y.

However they differ in their treatment of the content that belongs in Mathlib but does not yet have a dedicated file there:

• APAP is focused on a single end goal, hence all prerequisite content is similar in flavour and I ended up dumping it all in a single Prereqs folder.
• CamCombi is open-ended, therefore prerequisites fall into several large areas and are not confined to a single folder.

I don't know which approach you want to take but I would suggest:

• Be strict about the entry requirements of the FLT.Mathlib folder. Content going to existing files vs new files is a useful distinction since in my experience PRs adding stuff to existing files (without import increases) are usually merged incredibly faster than PRs for new content.
• Go for the CamCombi approach to prerequisites, because FLT has a single end goal like APAP but many many more intermediate goals than APAP.

Furthermore, I can set you up an upstreaming dashboard once its design is a bit more settled.

[grunweg]

Just want to say: I'm really happy that the mathlib PR metadata collection for the queueboard repository is proving useful beyond its original goal (namely, for the upstreaming dashboard).