contributing to leanprover-community/lean

Stream: general

[Floris van Doorn]

I just tried to make my first change (in ages) to the core library.

I didn't want to build Lean myself. I had to run elan override set leanprover-community-lean-3.16.5. Is that the intended way to do this?
Am I correct that leanproject will not help for this?
Shall I add a message like this to README?

[Johan Commelin]

I'm not an expert, but I think the answer is "yes", "yes", "yes please".

[Bryan Gin-ge Chen]

That will work to a certain extent, but I think "go-to-definition" in VS Code will take you to the wrong place. There may be other editor-related things that are broken too.

I don't know a good way to get all of that working without rebuilding Lean, sadly.

[Floris van Doorn]

Ah, good to know. I think it's still useful to mention this option in the Readme, but I added a warning: lean#368