This is blocked by manual registration to Reservoir. See the [zulip thread]([#general > Multiple packages in the same repo + Resevoir?](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Multiple.20packages.20in.20the.20same.20repo.20.2B.20Resevoir.3F/with/569059510)).