How to check local changes?

Stream: lean4 dev

[Dax Fohl]

I'm just going through the dev guide and trying to make some local changes and see the effect, but having trouble connecting the dots.

I figured an easy task to see if things are set up properly would be to remove the try/catch added in https://github.com/leanprover/lean4/pull/4177 and see if it reverted to the old behavior.

First I went through the user guide (not dev guide) and created an empty project with the proof from that PR, and observed the fixed behavior.

Then I went through the dev guide. I cloned the repo, built it (a few minutes), removed the try/catch and rebuilt. The build output looked reasonable; it saw the change in Simp.lean, and incrementally built everything from there on (just a few seconds).

I installed elan, and ran

elan toolchain link lean4 build/release/stage1
elan toolchain link lean4-stage0 build/release/stage0

per the docs. I verified it's in the path.

Now back in my user project, I updated lean-toolchain from leanprover/lean4:v4.20.1 to lean4 (is this correct?). VSCode noticed the change and asked to restart Lean, which I did, and it succeeds. Additionally I checked from the project folder command line, elan show reports

lean4 (overridden by '/Users/daxfohl/lean/test/Untitled/lean-toolchain')
Lean (version 4.22.0-pre, arm64-apple-darwin24.5.0, commit ec9ff12fc653, Release)

So, seems like everything is hooked up correctly. But when I go back to the user project and edit the simp args like in the PR's video, it still works like the try/catch is still there, i.e. I'm not seeing the effect of my changes at all.

Is there anything obvious I'm doing wrong?

[Kyle Miller]

How about you try modifying Lean in a way that would be much more visible, like add in a logInfo?

[Kyle Miller]

It's possible that other things have changed in the meantime. For instance, lean4#5863 might be a confounding your test.

[Dax Fohl]

Yeah that's what I'll try next. Main reason I didn't is, just getting started IDK what logInfo does or how to use it or check it; it was easier to undo a PR and check whether it matches the video. I'll give the logInfo a shot though; seems pretty obvious what it should do.

[Kyle Miller]

Can I ask what made you decide to select this PR in particular?

[Dax Fohl]

Hmm, IDK if there's a robust reason. I was looking at issue https://github.com/leanprover/lean4/issues/4181 because it had lots of upvotes, so I was thinking of maybe looking into that. The other PR was linked there in the 2nd comment as an example, and when I was setting up the dev environment, that just came to mind as something I could do to check whether it was set up right or not.

[Dax Fohl]

Anyway, logInfo works, so looks like you were right about 5863. So maybe the try/catch that was added in 4177 is no longer needed and should be removed?

[Dax Fohl]

Also do you think it's worth adding a section to https://github.com/leanprover/lean4/blob/master/doc/dev/index.md for how to check the setup?