modifying just the lean files, in lean core

Stream: general

[Scott Morrison]

Suppose I want to checkout git@github.com:leanprover-community/lean.git and just modify some of the Lean files. What do I actually do? The build instructions there are all about actually building Lean itself. I just want to modify some .lean files under the library directory. How do build everything in the library directory?

[Scott Morrison]

I've got so used to the wonders of elan/leanpkg based lean...

[Bryan Gin-ge Chen]

Hmm, if your default Lean is at 3.7.2c (or if you set an elan override for your lean repo directory) then you can just open library/ in VS Code and it should be OK for most things right now, since the master commit doesn't have any changes to Lean beyond 3.7.2c.

However, "Go to definition" won't direct you to the right place, and you might not be able to test your changes easily, since you'll still be running a different version of Lean using a different core library.

I don't know how to get all of that in sync without building Lean and setting up an elan override to a local toolchain (see elan toolchain help link).

[Yury G. Kudryashov]

I used elan run leanprover-community-lean-3.7.2 lean --make -j 1 . to compile modified library, doesn't give you editor support.

[Yury G. Kudryashov]

How do I override toolchain in a directory?

[Bryan Gin-ge Chen]

I can never remember the syntax so I just type elan override and follow what it says there.

[Bryan Gin-ge Chen]

Looks like it's elan override set leanprover-community-lean-3.7.2.

[Yury G. Kudryashov]

Emacs mode works after elan override!

[Yury G. Kudryashov]

@Scott Morrison What are you going to modify?

[Scott Morrison]

I wanted to muck around with ne.def, contrary to Mario's advice. :-)