Two projects in one repo

Stream: general

[Alex Meiburg]

@Joseph Tooby-Smith and I each have a repository about doing physics in Lean, albeit with some different focuses/goals. We've been talking about whether it would be best to make a combined one ... there's not much duplicated code/logic, but it would be nice if eventually they were somewhat integrated.

One possibility that occurred to us would be having two separate lean projects in the same repository. I'm not entirely sure what I mean by this myself, but one thing would be just having multiple build targets in there. Initially they would probably be quite separate in terms of their dependencies, but then we can start to share stuff as we go. This would mean we also must synchronize bumps and so on, and I'm not sure how it would interact with (say) docgen or linter settings or downstream users being able to point at one or the other.

Another option would be trying to have multiple lakefiles, two entirely separate Lean projects. I don't know if this is possible with the standard package management. Or we keep it as two separate repositories, like it is right now.

Does anyone have perspectives on what the benefits/drawbacks of these would be?

[Anne Baanen]

Keeping multiple separate Lakefiles in the same Git repo generally works quite well in my experience: if one project depends on the other and both live in the same repo you can reference the other project by local path instead of Git URL. (For example, DocGen is usually run by making a new project inside the existing repo, that depends on the original project + doc-gen4.)

[Anne Baanen]

(I haven't had much experience with multiple libraries in the same lakefile, this seems like it might mean too much synchronization is required.)

[Matteo Cipollina]

If it can be of any help, I have recently had similar needs and have managed to find a practical compromise (that works for me) by pasting project folders with their top-level .lean file in the top level of the repository I'm using and adding the folder to and adding the folder in the lakefile . In this way you don't need to change the imports in the pasted project's files. The only caveat is that the projects need to be under the same toolchain/lean/mathlib - I've found simpler to update the files rather than experimenting with different, more structured, set-ups...

[Joseph Tooby-Smith]

Thanks for putting this question together Alex.
I think having it under the same toolchain/lean/mathlib is what ideally we want.

I think the below covers all the options (with permutations of Project A and Project B).

Option 1

.
├── ProjectA /
│   └── Files for project A
├── ProjectA.lean
├── ProjectB /
│   └── Files for project B
├── ProjectB.lean
└── shared lakefile

• I'm not sure what such a lake file looks like
• I'm not sure how if someone could import ProjectA and not ProjectB for example.

Option 2

.
├── ProjectA /
│   └── Files for project A
├── ProjectA.lean
├── ProjectB/
│   ├── ProjectB/
│   │   └── Files for project B
│   ├── ProjectB.lean
│   └── lakefile for project B
└── lakefile for project A

• I'm not sure how someone would import Project B in this case in a downstream project.

Option 3

.
├── ProjectA /
│   ├── ProjectA/
│   │   └── Files for project A
│   ├── ProjectA.lean
│   └── lakefile for project A
└── ProjectB/
    ├── ProjectB/
    │   └── Files for project B
    ├── ProjectB.lean
    └── lakefile for project B

• disadvantage is that it would not get indexed by the Lean reservoir I think.
• Also not sure how one would import either Project A or ProjectB in a downstream lake file

Option 4

.
├── ProjectA/
│   ├── Files for project A
│   └── ProjectB/
│       └── Files for Project B
├── ProjectA.lean
└── single lakefile

(edit: Needless folder removed)

• disadvantage here is that there is a lot of upfront work

[Chris Henson]

How would the eventual integration work? Another target that both of these would have as a dependency?

[Alex Meiburg]

That's one option. As a first step, having a shared "Physics_ForMathlib" project or something that at least lets us share our ForMathlib folders.

Or you can do it "backwards": make a new project that depends on both, and gradually move files "down" to the shared project. I think this would kind of work with Option 1? This lets other contributors immediately start putting new files in the shared project, and then we gradually downstream code (starting with leaf files) into the shared project.

[Joseph Tooby-Smith]

Or you can do it "backwards": make a new project that depends on both, and gradually move files "down" to the shared project. I think this would kind of work with Option 1? This lets other contributors immediately start putting new files in the shared project, and then we gradually downstream code (starting with leaf files) into the shared project.

I struggle to see how this would not end up with something that in the end is schematically different from Option 4. Given that, I don't think the two libraries share much overlap currently.

[Martin Dvořák]

My guess (without knowing your specific situation) is that having three projects in three repositories would be the best organization.

[Joseph Tooby-Smith]

@Martin Dvořák The reason we are thinking about combining is more of a social one rather than a technical.

I think more broadly the options I gave above can be summarised into two broad approaches:

1. Keep two separate Lean projects but put them in the same repo. (Option 1 -3)
2. Combine the two Lean projects into a single Lean project with a single repo. (Option 4)

IMO: The advantage of 1 is that it keeps the 'identity' of the two projects, but it is technically more difficult and more complicated for downstream users. The advantage of 2 is that is technically simpler and less complicated for downstream users (only one import etc), but it risks losing the 'identity' of one or both of the projects. I think this last point is something we could potentially mitigate against with careful documentation, Readme adjustments etc to make it clear the origin of the parts.

[Jon Eugster]

regarding your questions about importing in somwhere downstrean: iirk lake will always clone/download the entire repo but it has support to specify a subfolder where the Lean project lies to import from.

Here are my thoughts:

Option1: Just a regular lakefile with two default_target libraries. Downstream, you would "require" the entire project and then simply "import Project A"

Option 2: looks a bit funky, but you could import B same way as in option (3). Don't see an advantage over (3) though...

Option 3: you can require them with something like require xy from git "url..." "subfolderA"

Option 4: basically A is the only library and B is a part of it. can be an option if you want full integration.

I think I'd recommend (1) if it's fine that they completely share the dependecies they require. Or (3) if you want to go be compnetely independent and don't care about being listed on reservoir (although don't know any recent features reservoir might have added)

[Joseph Tooby-Smith]

Many thanks @Jon Eugster, this is really helpful. I think the only advantage Option 2 has over Option 3 is that there is a .lakefile in the top level directory, and would thus get indexed on the reservoir.

Out of Options 1-3, I agree that Option 1 seems like the best, and potentially better than Option 4.

[Joseph Tooby-Smith]

Am I right in saying that in Option 1, ProjectA can depend on files in Project B AND ProjectB can depend on files in ProjectA. Further if you do e.g. import ProjectB downstream it will build all those files in ProjectB and precisely those needed in ProjectA.

[Alex Meiburg]

Option 1 is sounding the best to me, too. I think that's essentially what I have with the little "StatMech" folder in QuantumInfo right now, but I wasn't aware that there could be multiple default targets! That's cool

[Joseph Tooby-Smith]

What is the consequence of a target being the a default? Is it (just) that lake build would build both?

[François G. Dorais]

Yes, default only specifies what gets built with no specific target.

I've used 1,2,3 and they all work smoothly.

[François G. Dorais]

(But I suppose that depends on your expectations. Maybe that's a better starting place?)

[Markus de Medeiros]

See also: #general > Multiple packages in the same repo + Resevoir?

[Bhavik Mehta]

In https://github.com/b-mehta/Polychromatic there are two separate lean projects with their own lakefiles, which seems to be a common way of working with Verso projects