Contributing to lake

Stream: general

[Greg Shuflin]

I'm interested in contributing to the lake tool - in particular, I think it would be very useful if there was a lake add command analogous to cargo add, and also better documentation about the lakefile.toml syntax (as well as documentation about the old-style? lakefile.lean DSL, when you should use one or the other, etc.) I can probably do some of the legwork on this myself, and I'm happy to try to upstream commits to github, but I'm curious if there's anyone I should talk to about how to bootstrap myself into contributing to lake specifically

[Alok Singh]

@Mac Malone ?

[Mac Malone]

@Greg Shuflin Thanks for your interest!

We are currently working on richer documentation for Lake as part of the Lean reference manual, so improvements there may be best delayed until an initial version of that section comes out. CC @David Thrane Christiansen, who is the author of the manual.

As for lake add, this is something we have considered before. Unfortunately, I don't think there is an RFC issue for it yet -- making one would be much appreciated! One major complication is that the configuration code is currently undergoing a major refactor, so this may not be the best time to try to add a feature. On the other hand, this refactor may take a few months, so if you are eager to try something, feel free, just be aware that major merge conflicts may be enivitable.

Also, if you want to ensure that your contributions have the best chance of getting merged, please make sure to read (and follow) the contribution guidelines carefully.

[David Thrane Christiansen]

A draft Lake chapter should be ready very soon :)

[Greg Shuflin]

solid, I've made an issue for this: https://github.com/leanprover/lean4/issues/6676