advice for developing a custom version of lean4

Stream: lean4

[Adam Topaz]

I want to experiment with making some changes to lean4 (just locally on my machine). I followed the instructions on the reference guide: I built forked and cloned the repo, built from source, set elan to use stage0 in src, etc. When I open src in vscode, everything seems to work as expected. But if I change something in one file, say A.lean, I can’t get the changes to be reflected in any other file in src which imports A.lean. I’ve tried restarting the server, and even restarting the editor. Is there a step I’m missing here?

[Wojciech Nawrocki]

Unless I am misunderstanding, that is how it's supposed to work: src is built using stage0, whose entire sources are the C files committed to stage0/. Your changes to A.lean under src/ only affect stage1. If they affected stage0 automatically, your Lean would be broken most of the time while working on src/ (speaking from experience here).

[Wojciech Nawrocki]

One way to test the changes is to open a folder that does use stage1, e.g. the tests/ directory.

[Wojciech Nawrocki]

I am talking about the compiler itself here. Changes to modules such as adding new definitions should be visible when working on src/ using stage0, afaict.

[Joachim Breitner]

Running make -C build/release/stage1 (or similar, I'm on mobile) might help updating the A.olean so that the other file sees the changes (of course they won't affect the compiler you are developing with, but I didn't think that's what you mean)

[Adam Topaz]

I changed a definition in a lean file from src, and I’m trying to see the change in another file that imports it, also in src. So do I understand correctly that it should just work?

[Mario Carneiro]

No, "refresh file dependencies" inside lean core is spelled cd build/release; make

[Adam Topaz]

Aha ok

[Adam Topaz]

Thanks Mario. that works!