import must be rebuilt

Stream: lean4

[Patrick Massot]

I'm really not a fan of the new way Lean keeps telling me: Imports of ... are out of date and must be rebuilt. whenever I open a file. There is nothing you can do in this situation without rebuilding the imports. So why not doing it? If people really insist Lean shouldn't work before users politely ask it to, then we could have a VSCode dialog asking: Imports of ... are out of date and must be rebuilt. Do you want to proceed? and then do it when user click ok.

[Patrick Massot]

Wait, actually it already proposes to rebuild, so the second part of my message is irrelevant (although this would be a lot easier to spot if the dialog was no hidden in the lower-right corner but in the center of the screen since it is crucial).

[Ruben Van de Velde]

I really like that it isn't automatic anymore, especially when doing a merge. Maybe it could be personalized

[Patrick Massot]

The first question remains: why not rebuilding automatically in those cases where Lean refuses to do anything until you rebuild? I would understand this to be a warning only if doing anything was possible.

[Adam Topaz]

What I find extremely annoying is that I have to move my hand off the keyboard to the mouse, move the cursor ALL THE WAY to the corner, and actually click something :-/

[Adam Topaz]

Can we at least have an option to rebuilt imports automatically?

[Ruben Van de Velde]

There's a shortcut - ctrl shift x?

[Sebastian Ullrich]

image.png

[Adam Topaz]

Ok great!

[Sebastian Ullrich]

Yes, the shortcut is as before - it just has one more use case now

[Adam Topaz]

The shortcut doesn't get rid of the button...

[Sebastian Ullrich]

Oh, indeed. @Marc Huisinga Is this something we can influence?

[Ruben Van de Velde]

You can still edit or look at the code without the info view. It's really annoying if I'm fixing merge conflicts and it tries to build all of mathlib under me

[Ruben Van de Velde]

Especially if I have another repository open and I can't use killall lean to stop it

[Patrick Massot]

Ruben, you can still edit or look at the code while it's building.

[Eric Wieser]

Patrick Massot said:

Ruben, you can still edit or look at the code while it's building.

I find that typing \real etc doesn't work if Lean is really busy processing things

[Ruben Van de Velde]

Not if the fans lift my laptop off the table :)

[Eric Wieser]

Worse yet, if you click the vscode buttons to resolve merge conflicts, they sometimes make incorrect edits to the file due to everything being buffered for too long

[Sebastian Ullrich]

You should try these again after lean4#2714 lands in mathlib

[Scott Morrison]

@Patrick Massot, I want to explain the motivation here in more detail, as this is something I have been asking for.

It is not the case that when presented with this message there is nothing you can do but press ctrl-shift-x to start a rebuild!

The important alternative is that you can run lake exe cache get first, which may in fact save you a massive build.

If the rebuild starts automatically without displaying this message, or because you have set the lean4.automaticallyBuildDependencies option, then you destroy the possibility of running lake exe cache get, because a background build will already be running, clobbering your oleans as lake exe cache get runs.

This situation (automatically started builds from tabs, but also wanting to run cache) is what caused many of us to have to keep closing and reopening our VSCode windows --- which was very very annoying!

[Scott Morrison]

What can we do to make this better?

If we had a really fast cache noop (our current one might be fast enough, Mario's proposed replacement would have been, and in the long-term the Reservoir based one hopefully will be), then I would advocate for ctrl-shift-x actually being a short-cut for lake exe cache get + current behaviour.

And, possibly, go back to triggering automatic builds when you open a tab, but with lake exe cache get run every time.

[Eric Wieser]

Scott Morrison said:

The important alternative is that you can run lake exe cache get first, which may in fact save you a massive build.

I had no idea this was the now the case, and have been dutifully running pkill lake!

[Patrick Massot]

In my use case lake exe cache get would do nothing. But of course I agree that the proper solution is to have faster cache noop.

[Scott Morrison]

@Patrick Massot, what would you think about just uploading oleans during your CI? This would require the central infrastructure sharing the upload key with you. I think previously we've not wanted to do this out of some combination of security concerns, and having to decide a rule for who gets the key.

But I think it would be good to experiment to see if we can make it work.

Moreover, with the longer term intention to deprecate the current caching system, it feels less important to actually answer the "who gets the key" question well.

[Patrick Massot]

Actually I was working on Mathlib when I got annoyed by this. But this isn't very important, especially since better solutions are coming.

[Marc Huisinga]

Patrick Massot said:

Wait, actually it already proposes to rebuild, so the second part of my message is irrelevant (although this would be a lot easier to spot if the dialog was no hidden in the lower-right corner but in the center of the screen since it is crucial).

Using a modal dialog for this will almost certainly also annoy people and I'm sure that there are ways to open files where you do not immediately want to decide whether you want to rebuild the imports for each (e.g. when opening multiple files at once).

Sebastian Ullrich said:

Oh, indeed. Marc Huisinga Is this something we can influence?

I don't think so.

[Marc Huisinga]

There are a couple of commands that let you manage notifications using your keyboard:
image.png
But I don't think we want to call any of these automatically in the extension because of the obvious race conditions.

[Sebastian Ullrich]

Oh no. Not ideal either, but experienced users may welcome a setting to disable the notification then? I think we could also give the progress bar a different, less scary color in this case.

[Marc Huisinga]

Adam Topaz said:

The shortcut doesn't get rid of the button...

By the way, you can use Escape to hide the notification. Unfortunately, VS Code does not let us do it programmatically.

[Shreyas Srinivas]

@Marc Huisinga : One issue is that the extension often says I must "rebuild the imports for the file" and gives me the option to do this is the notification. But it doesn't appear as a command in the command panel. So if I accidentally get rid of the notification, I have to use my mouse to go to the notification to rebuild imports.

[Marc Huisinga]

It's "Restart File" in the command panel.

[Marc Huisinga]

I could rename the button to make this clearer.