Mac Malone

@digama0 One other little minor note I forgot. `lake env` has already has a dump format! If you run a bare `lake env` with no args, it will dump the...

@mhuisi Could you elaborate? I do not see how this introduces more possibility of deadlock than `IO.Ref.modify` and/or `IO.Mutex`. The example I can think of is that if you wait...

@Kha The Lake linking fixed one of the tests, but the other is now failing with `l_System_FilePath_join was replaced` ([log](https://github.com/leanprover/lean4/actions/runs/8192309889/job/22403532585?pr=3601#step:17:3681)).

I believe I have fixed everything I can on the Lake side and everything now can function, so I will hand this back to you @Kha.

@Kha Added the release note. Feel free to merge when convenient.

@Kha Does this need a stage0 update or similar for the change to `many(1)Indent` to appear in the tests? Or is this an actual bug on my end?

@digama0 What is the best way to do that? For instance, after building mathport with the custom Lean, what should I port? P.S. Also, since you are here and you...

@digama0 > Looking at the test failures, it appears there are already some undesirable formatting changes which need to be tweaked. I don't think there are any build issues here,...

@semorrison Should not this be symmetric? That is, if Lean solves `max u v =?= max u ?v` should it not also solve `max u v =?= max ?u v`?...

@semorrison Ah, okay, makes sense. 👍