Easiest way to hack on Std?

Stream: lean4

[Mai]

Hi. What's the simplest way to hack on the standard library? Do I have to compile the entire toolchain from scratch?

[Kevin Buzzard]

I don't know the answer to your first question but I'm pretty confident you don't have to compile anything, because I can hack on mathlib (which imports Std) without compiling anything by just typing lake exe cache get. Maybe the same works for Std?

[Yury G. Kudryashov]

@Kevin Buzzard Std is a part of the Lean main repository, so the story is very different there.

[Henrik Böving]

Mai said:

Hi. What's the simplest way to hack on the standard library? Do I have to compile the entire toolchain from scratch?

Yes

[Yury G. Kudryashov]

Are there plans to make it easier to contribute to Std?

[Jovan Gerbscheid]

You can set the Lean toolchain to the latest nightly version, and then work in the files locally. Though with this approach, the changes do not persist through imports.

[Ruben Van de Velde]

That's one of the disadvantages of making so much built into the core compiler rather than using external libraries like batteries

[Mirek Olšák]

I would like to point out that there is also no problem with adding new functions to the Std namespace from the outside, including for example extending the dot-notation for already existing objects (defining things like List.myFunction), which feels a little "hacky" even without editing the library files.
I am not sure which exact hack you need, maybe this was obvious, I just wanted to mention it here for completeness.