Adopt the Research Codebase Manifesto?

[Vtec234]

At one point we moved some dead-but-maybe-useful code into separate branches. There is also a dev branch which is supposed to be more broken in terms of CI than main. These facts, as well as that we may at some point want to move over code from other checkers and projects without necessarily immediately cleaning it up, suggest that we could benefit from a better organization of the file hierarchy instead of attempting to move between dedicated branches like this.

I propose that we adopt the Research Codebase Manifesto in some form. opencompl/ssa is another Lean project that has been using the RCM, and they report being happy with it.

[JamesGallicchio]

That sounds quite good to me.

I see the SSA project has everything in one lake facet, but it looks like they tried having separate lake facets? Do you know more about that?

I'd prefer the core library be in its own lake facet:

• Hoping the library gets some use outside of our group and it seems smart to dogfood the core library as a lake package.
• Can separate CI between core & projects/experiments

I particularly look forward to this forcing us to more frequently review each others' code, since we will be PRing to experiments and projects with lower standards than how we have been treating main.

[JamesGallicchio]

closing as completed