multiple packages in one repo with Lake

Stream: lean4

[Simon Hudon]

Does Lake support repos that contain multiple packages? Specifically, I'd like add a dependency like this "github.com/myaccount/myrepo/some-directory-in -the-repo". Is this feasible?

[Xubai Wang]

The dir field of Dependency structure is intended for this.

For your information, the definition is at https://github.com/leanprover/lake/blob/126144d4516b11748866298c86041ede2303f809/Lake/Config/Package.lean#L75
and as an example:
https://github.com/leanprover/lake/blob/126144d4516b11748866298c86041ede2303f809/examples/git/lakefile.lean

[Simon Hudon]

Great! Thanks!