lake clean lakefile.olean's

Stream: lean4

[Somo S.]

@Scott Morrison said:

Just noting: v4.1.0 of Lean is out.

In fact, so is v4.2.0-rc1, and Mathlib is already using it. In particular you will find many improvements in Lake, including substantially faster performance!

Quick question, I noticed in one of the v4.1.0-rc's lake clean would not clear the lakefile.olean's in source and lake-package directories.. is this still the case in v4.1.0?

[Scott Morrison]

Yes, that's still the case for v4.1.0 and v4.2.0-rc1. I agree that seems strange behaviour for a clean command. I hadn't noticed this previously. @Mac Malone?

[Mario Carneiro]

I would guess this is related to the fact that it's the only build output not in build/

[Mario Carneiro]

(which I argued against at the time)

[Somo S.]

yeah seems like a strange design choice ¯\_(ツ)_/¯

[Mac Malone]

@Scott Morrison Yeah, I noticed this and put it on my todo list, but honestly forgot about it in the flurry of performance improvements.

[Scott Morrison]

No problem. Made lean4#2592 to track. Thanks, @Somo S., for the reminder!

[Scott Morrison]

Separately, I noticed that people are creating issues for lake both at the old lake repository and the lean4 repository. Could we fix this? Is there some way to transfer the remaining relevant ones, and then prevent opening new ones at lake?

[Mario Carneiro]

my impression was that the lake repo was for issues

[Somo S.]

I recon archiving the old repo could help

[Scott Morrison]

Ah, I had missed that this was happening intentionally. I think it would be good to make sure Lake issues are all in one place. I don't mind which place, particularly!

[Somo S.]

if the intension is for lake source to permanently be in the lean repo. then i would think all issues should be there also

[Schrodinger ZHU Yifan]

Another thing I want to mention here is that newly added -Kvar=value (as used in meta if) does not seem to be effective once the old lakefile.olean is built.

[Mac Malone]

@Schrodinger ZHU Yifan Yep! To quote from the [release notes[(https://github.com/leanprover/lean4/blob/master/RELEASES.md#v410):

Lake configuration options (i.e., -K) will be fixed at the moment of elaboration. Setting these options when lake is using the cached configuration will have no effect. To change options, run lake with -R / --reconfigure.

[Mac Malone]

This has some benefits of its own, you can set -K options on the command line via -R and then they will persist into the Lake commands runs interactively (e.g., via VSCode) without having to change settings.

[Joachim Breitner]

Does lake somehow warn if the given configuration flags don't match those remembered in the .olean? Else I see a scenario where someone might have a very frustrating debugging experience, trying to find out why something isn't working as it should.

[Mac Malone]

@Joachim Breitner No, but that is certainly a good idea.