RFC: move Lake into a subtree

[Kha]

Now that fixes from Lean changes are roughly as common as actual changes to Lake, I would like to get rid of our common enemy the git submodule. By moving to git subtree, which creates a bona-fide copy of the Lake repo inside this repo instead of the weak link submodules represent, necessary fixes to Lake can be done in this repo as easily as to any other local files and can be imported back into the Lake repo at the maintainers' leisure. Lake commits imported into this repo can be squashed into a single commit, ensuring the history will look basically the same as right now (except for more changed files per commit).

No other changes to organization are proposed; issue tracking and feature development of Lake should stay in the Lake repo.

Summary of changed procedures:

• pull new changes from Lake:

git subtree pull --prefix=src/lake https://github.com/leanprover/lake lean4-master --squash

• make compatibility changes to Lake: just edit the local files
• push fixes to Lake, e.g. after a PR is merged:

git subtree push --prefix=src/lake https://github.com/leanprover/lake lean4-master

Of course, the lean4-master Lake branch may also be considered redundant with the Lake in the lean4 repo itself in this setup.

/cc @leanprover/dev @tydeu

[Kha]

See also rust-lang/compiler-team#266

[tydeu]

@Kha This seems largely fine. My only real question is: Why the squash? Why not just pull changes verbatim? For instance, in the Rust example you mentioned one of the stated benefits there is "Git subtree preserves commits on both sides."

[Kha]

@tydeu I think either way is fine, but since we didn't have a problem with the granularity of Lake updates so far, I kept the status quo. I never had to bisect through a Lake update in lean4 so far, for example.

[gebner]

Yes! ❤️ Anything to get us away from the submodule!

I don't have a strong opinion on whether to squash or not. Lake doesn't have a lot of commits so I don't think it makes a big difference either way.

[digama0]

I'm also in favor of using git subtree here. I think it would be better not to squash as it will make it harder to follow things on the lake side if there are a bunch of unrelated PRs being merged together. Rust has some nice tooling for that but it's still not a great experience to see all those rollup merges in the history and a useless diff. (Squashing once per PR is fine.)

[Kha]

Only the commits coming from the Lake repo would be squashed. Basically every squashed commit would be "chore: update Lake"

[gebner]

@Kha I think we all agree that this is a good move. Are you waiting for anything before doing it?

[digama0]

What does this mean for contributors? Is it now possible to make lake changes either via lean4 PRs or lake PRs? When should we do one or the other?

[tydeu]

@digama0 All PRs will now be to here, the Lake repository will be frozen/archived.

[hargoniX]

In that case I have a little question, how is doc-gen supposed to pull in Lake stuff now, can I just import Lake without dependencies now?

[Kha]

@hargoniX The missing part is the static library, not the oleans, no?

[hargoniX]

I don't know what the missing part is I haven't tried updating it yet, I'll take a look tomorrow.

[digama0]

That's right, import Lake works but causes linker errors because the static library is not available. This is a concern, if the Lake repo is to be archived, so hopefully we can get it distributed with lean?

[Kha]

#2337