modifying lean core library code

Stream: general

[Jason Rute]

So I'm playing around with proof recording of sorts. I've written my own hacked versions of the rw, rwa, erw tactics that trace certain information. I'd like to try it out on the whole lean and mathlib libraries, but I am not sure how to do two things:

1. How do I safely modify the lean library code (in this case interactive.lean) without breaking my stable lean distribution? (I also assume I need to recompile the .lean files, but I assume I do that with lean --make.)
2. Is there a convenient way to have Lean run all files in the lean library and mathlib (so that I can get the trace information from my proof recording hack)?

[Jason Rute]

By "the Lean library", I mean the files in ~/.elan/toolchains/3.4.2/lib/lean/library/init.

[Scott Morrison]

For point 2., there is a script scripts/mk_all.sh (and a corresponding script scripts/rm_all.sh) that will create src/all.lean, which imports all of mathlib.

[Scott Morrison]

I'd be happy to hear the answer to 1. as well. I used to know how to hack core Lean comfortably, but seem to have lost that skill, and my current process involves deleting my ~/.elan directory and reinstalling when I'm done. :-(

[Johan Commelin]

@Scott Morrison Does this help? (Quote from a PM)
Gabriel Ebner said:

If you build lean locally, then you can just set the lean.executable configuration option in vscode to use the freshly built lean.
Another option for such a small change is to elan default nightly && elan update and then open the lean/library directory in vscode.

[Bryan Gin-ge Chen]

For 1, here's how I'd do it. It might be more complicated than necessary, so I'd also appreciate hearing about better ways. First, I'd clone the community Lean repo and then make your modifications there. Build Lean following the directions here and it will create some binaries in bin/ which use your modified library in library/.

You can then create a local toolchain from your copy of the lean repo with elan: see elan toolchain help link.

Then you can set it as an override in a copy of mathlib using elan override.

[Gabriel Ebner]

The elan override is how I do it as well. You should also set the elan override in the lean directory as well.

[Jason Rute]

So I have to recompile the C++ code to make this work?

[Bryan Gin-ge Chen]

Yeah, unfortunately I don't know another way, though to be honest I haven't tried very hard to find alternatives yet. It seems like there ought to be a way to specify a path to the core library...

[Jason Rute]

Ok. I found one way to do this without compiling C++ binaries. (Note: I may have even found a better way, but let's record this way first since I know it works.) (Edit: See below for cleaner solution.)

1. Go to ~/.elan/toolchains/ and find the lean toolchain you want to modify.

2. Copy it to another location: cp ~/.elan/toolchains/<toolchain> <path/to/where/lean/copy/will/be/stored>.
   2a. If you want version control, you can set up git for that new directory, just the library directory, or replace the library directory with a symbolic link to another library directory.

3. Link this new location as a new toolchain in elan: elan toolchain link <my_new_toolchain_name> <path/to/lean/copy>.

4. Go to the project directory and override which lean to use: elan override set <my_new_toolchain_name>.
   4b. (I don't know if it matters, but if using leanpkg, maybe you need/want to change the lean version in leanpkg.toml.)

5. In vs-code preferences for the lean plugin, change the lean executable path to ~/.elan/toolchains/<my_new_toolchain_name>/bin/lean but only for the workspace, not the user.

6. Modify the core library files in your copied lean directory without fear of breaking anything outside of that directory. (You will have to do lean --make, etc, but I think you folks know more about that than I do.)
7. Test on the command line by doing lean --path (and checking that your path is to the copy of the lean library). (Not sure how to test the vs code directly, but you can tell when a change you made to a core file is being used when another file imports it that core file.)

[Sebastian Ullrich]

Step 4 should already cover step 5

[Bryan Gin-ge Chen]

Yes, if you're using elan there's very rarely any reason to change the executable path setting in vscode-lean (hence the discussion here).

[Jason Rute]

Good to know.

[Jason Rute]

Ok, I have a much cleaner and easier hacky solution. Assuming your project was created with leanpkg (or probably the newer leanproject) and has a leanpkg.path file, then modify that file replacing builtin_path with path <path/of/replacement/lean/core/library>. Then do lean --path to make sure that new path has taken hold. It works great!

[Jason Rute]

(When I upgrade to leanproject, I'll double check that this solution still works.)

[Jason Rute]

You still have to do some variation of steps 1 and 2 above to make a copy of the core library.

[Bryan Gin-ge Chen]

Ah, of course. That makes sense. I'm not 100% sure, but I believe leanpkg.path may get overwritten when using leanpkg and leanproject to upgrade dependencies, so you may have to watch out there.

[Jason Rute]

Good point.

[Patrick Massot]

Currently leanproject still uses leanpkg under the hood (because I don't have enough time/motivation to get rid of it). In particular it calls leanpkg configure that creates leanpkg.path. So yes, it will be overwritten if you try to update mathlib.

[Patrick Massot]

But there is no problem "fixing" this. It only costs time. So, if you really need this, you need to either tell me you really really need it, or open a PR.

[Sebastian Ullrich]

Jason Rute said:

Ok, I have a much cleaner and easier solution. Assuming your project was created with leanpkg (or probably the newer leanproject) and has a leanpkg.path file, then modify that file replacing builtin_path with path <path/of/replacement/lean/core/library>. Then do lean --path to make sure that new path has taken hold. It works great!

So your elan toolchain + elan override commands are replaced with editing leanpkg.path? That does sound marginally easier, but as pointed out it's definitely less clean. I would still recommend an override. It's the highest-priority source of the desired Lean version for elan.

[Jason Rute]

Good to know. What I'm doing now isn't really core Lean development, but core Lean hacking. :grinning_face_with_smiling_eyes: So I'm comfortable with the consequences. Either way, I've found two ways to modify the core lean code without breaking Lean for other projects and without having to recompile the C++ code. If anyone asks, you all recommend the former approach, which makes sense.