Imports are out of date

Stream: general

[Noailles]

I have updated my lean toolchain, and have already run 'lake exe cache get' successfully. But VScode tells me 'Imports are out of date and must be rebuilt; use the "Restart File" command in your editor.'. What should I deal with this problem?

[Eric Wieser]

You should open the "command palette" and run the "restart file" command

[Noailles]

Thanks!

[Kevin Buzzard]

Yikes. Is this a new message? Should it be clarified?

[Mario Carneiro]

I believe it is new

[Mario Carneiro]

@Marc Huisinga Any chance of getting a popup with a button out for this soonish?

[Mario Carneiro]

I'm guessing that because the error message comes from Lake it doesn't have much ability to do more than give advice like this

[Mario Carneiro]

although I suppose it could give more precise coordinates to the "Restart file" command

[Marc Huisinga]

The error comes from the server. I'll see if I can add a popup for this soon.
On another note, you can also re-enable automatic builds on the most recent RC by selecting "Automatically Build Dependencies" in the VS Code extension settings.

[Floris van Doorn]

Does this mean that opening a Lean file will never cause dependencies to be built automatically, and you can still work in the file using the old olean files? That's great! :tada:

[Marc Huisinga]

Floris van Doorn said:

Does this mean that opening a Lean file will never cause dependencies to be built automatically, and you can still work in the file using the old olean files? That's great! :tada:

Dependencies will not be built automatically, but you cannot work with the old olean files either.

[Eric Wieser]

So is working with the old oleans no longer supported?

[Marc Huisinga]

You can still work with old oleans as you could before if you already had an editor for that file open. The only behaviour that changed is that opening a file or changing the imports does not automatically trigger a rebuild anymore.

[Marc Huisinga]

Mario Carneiro said:

Marc Huisinga Any chance of getting a popup with a button out for this soonish?

This is now at vscode-lean4#335 and I will merge and release it later today.