Mac Malone

@Kha > Why is that relevant? tests/ is not a Lake project, even running the full build from src/ in it does not help as it will not actually build...

@Kha What are you attempting to benchmark? Without the stage0 update, this PR has no practical effect.

With #4127, only jobs that do something significant now have a caption printed in non-terminal mode (e.g., the server), So this will hopefully be addressed in RC2.

Looking through the Mathlib/Std failures, there are some direct replications of `ppSignature` code in core which are producing errors now. To make fixing this easier, I extract this element into...

@digama0 > I think it is a bit misleading to call this a "fat library", and suggest using the term "statically linked" instead. Statically linked is too general for this....

@eric-wieser Maybe it is worth separating out this specific feature request into its own RFC (either here or on the VSCode extension issue tracker)? For example, something like "request permission...

The CMake build specifically looks for a relative path for `LIB` (see [here](https://github.com/leanprover/lean4/blob/3de60bb1f63efe9bb56380f911f86980b9f3332c/src/CMakeLists.txt#L508-L509) for Windows, so I am not sure were the absolute path is coming from. Maybe this is...

@Kreijstal Oh, are you building Lean from a different drive than the source and/or build results?

@Kreijstal Such a case seems like a reasonable feature request we can consider supporting (or better documenting the lack of support for) in the future. Could you update the issue...

Closing due to staleness and the fact that these changes have since been incorporated in other PRs.