Working on multiple files / Lean:Restart

Stream: lean4

[Antoine Chambert-Loir]

When I work with multiple files and add a function to one of them, how should I tell Lean that, so that I may use the new functions in the other files.
On my setup, “Lean restart” does not work (VSCode gives me an error : “command 'lean.restartServer' not found”).
The only way I found consists in commenting out the “import” line, saving, restoring the “import line”, etc…

[Kevin Buzzard]

Lean restart is for Lean 3. Try Lean 4: Restart Server.

[Scott Morrison]

Ctrl-shift-x on non-macos systems, and option-r on macos.

[Scott Morrison]

The keybindings I gave you have to do in the down-stream dependency, to tell it to reload its imports.

[Alex J. Best]

"Lean 4: Refresh file dependencies" is the vscode command to run for this, to be clear

[Kevin Buzzard]

Oh, so am I also using the wrong thing? What's the difference and does it matter?

[Eric Wieser]

Lean 4: Restart Server will be slower because it restarts everything

[Kyle Miller]

You could think of "Lean 4: Refresh file dependencies" as sort of restarting the server for just the current file.

[Eric Wieser]

Is that weaker or stronger than "Lean 4: Restart file"?

[Kyle Miller]

The existence of "Lean 4: Restart file" is news to me

[Max Nowak 🐉]

I wonder how hard it would be to make the vscode extension do this automatically for focused files. Or at the very least invalidate any files depending on changed files, so you don't start scratching your head why you get weird errors.

[Kyle Miller]

I generally like being able to control when a file reloads (sometimes you work with a file that's a deep dependency of another, and you don't want to have anything invalidated for the second file until you're ready for it).

[Kyle Miller]

It'd be great if something would pop up in the corner letting you know you have an invalidated file and give you a button to push to do "refresh file dependencies". That'd help keep you from scratching your head and it'd be a UI affordance to let you know about this feature.

[Sebastian Ullrich]

Filed as lean4#2368