Multiple packages in the same repo + Resevoir?

Stream: general

[Markus de Medeiros]

For Iris-Lean, we want to have a core library which does not depend on mathlib+cslib, and also an extended library which does have these dependencies. It would be nice to have everything in one github repository, like:

├── Iris-Lean/
│   ├── lakefile.toml
│   └── src/
│       └── ...
├── Iris-Lean-Ext/
│   ├── lakefile.toml
│   └── src/
│       └── ...
└── lean-toolchain

Is there a way to set such a project up so that Iris-Lean and Iris-Lean-Ext get indexed by Reservoir as two separate packages? I don't think this setup meets the inclusion criteria as it stands. Alternatively, is there a way to combine Iris-Lean and Iris-Lean-Ext with a single lakefile at the top-level, but still allow them to be independently imported and for Iris-Lean to not have a Mathlib dependency?

[Mac Malone]

Unfortunately, this project setup is not currently supported. However, I am planning to add a manual package registration to Reservoir this quarter which will support this. Still, having both packages in the same repository does impose a cost on users, as they will have to clone the full repository (i.e., the source of both) when requiring just the basic package.

[Markus de Medeiros]

Thank you for the reply! It sounds like the best thing to do for the time being is to use a separate repo, but I'll keep an eye out for the changes to package registration.