Renaming "refresh file dependencies"?

Stream: lean4

[Gabriel Ebner]

The command name "refresh file dependencies" is apparently quite unintuitive and unclear about what it does. For example @Chris Lovett never realized that it actually restarts the file worker, and that this is the main purpose of the command.

Should we rename it to "restart file worker" or even "restart file"?

[Mac]

How about "Reload File"? That way it nicely parallels with VSCode developer command of "Reload Window" as they do parallel things ("Reload File" reloads the worker without restarting the Lean server and "Reload Window" reloads the window without restarting VSCode).

[Mac]

(I was also surprised to discover that it restarted the worker if it broke. I had originally thought it just reset the internal Lean environment without restarting the process. Furthermore, had I not known -- due to working with the elaborator -- that it was impossible to reimport modules without resetting the environment, I would have thought it would have done just the reimporting i.e. without resetting the environment.)

[Gabriel Ebner]

Right, there's three commands here (with current names):

• "Reload Window" (restarts VSCode)
• "Restart Server" (restarts the Lean server)
• "Refresh File Dependencies" (restarts the file worker)

I think it's better to use "restart" instead of "reload" because it's consistent with other extensions. All of the extensions I have installed here use "restart server" ("Rust: Restart the Rust server", "ccls: Restart language server", "TypeScript: Restart TS Server", etc.).

[Henrik Böving]

Fyi in emacs we call it:

• lsp-workspace-restart (restarts the Lean server)
• lean4-refresh-file-dependencies (restarts the file worker)

for restarting emacs on the spot we don't really have something afaik.

[Mac]

When it comes to the renaming, I think there are two conflicting desires. If the problem a user has is that some imports updates are not registered, the command "Refresh File Dependencies" sticks out as a solution to that problem (whereas "Restart File" does not necessarily do so -- after all, it is conceptually possible to restart the worker without rebuilding/refreshing the dependencies). On the other hand, if the file is broken (i.e., the elaborator hit some bug and crashed), "Restart File" sticks out as a solution but "Refresh File Dependencies" does not.

[Mac]

Also, as an aside, since we are talking about resetting the server and elaborator bugs, does anyone know why / know how to fix a file where features like semantic highlighting and hovers is broken and/or error indicators are not updating (i.e., generally the info tree appears broken) but the info view is not? Resetting the file worker via "Refresh File Dependencies" works in that it updates the file (error indicators move to where they should be), but the file still remains non-interactive (e.g., no hovers, often no highlighting, and further changes will not update indicators).

[Gabriel Ebner]

I think that's https://github.com/leanprover/lean4/issues/1219

[Mac]

Yeah, that seems like it, as when my problem occurs in a given file, it continues to occur in the same file for the rest of eternity (EDIT: double checked, it does appear that issue does disappear at the very least after a system restart). But it only happens in certain files and without any clear reason why it does.

[Gabriel Ebner]

Back to the names. We could also have both commands ("refresh file deps" & "restart file") if this helps people find it. But fact is that the command restarts the file worker; that the dependencies are recompiled is very much a side effect.

[Mac]

I think that is reasonable (also, sorry for side-tracking the thread).

[Gabriel Ebner]

https://github.com/leanprover/vscode-lean4/pull/213

[Julian Berman]

Talking about "file workers" seems somewhat implementation-detaily to me, is there some reason an end user cares about that?

[Julian Berman]

I don't mean to further bikeshed the change, seems good to me, just want to make sure I'm not missing something

[Julian Berman]

Presumably an end user cares strictly about "my lean looks stuck" or "my imports aren't up to date" right? Not the fact that Lean happens to use one process per file.

[Gabriel Ebner]

If we have a restart command, then it must be clear what it restarts. The end user can also observe what is restarted by watching the orange bars. So I think it is very much relevant for the end user, because it answers the question "what will be covered in the orange bars of hell once I press this button".

[Gabriel Ebner]

The "file worker" terminology is a bit technical, that's why I left it out and simply called it "restart file".

[Sebastian Ullrich]

It's still mentioned in the restartFile description, which is what @Julian Berman might have been referring to

[Gabriel Ebner]

Oops, I've just copy&pasted that from the refreshFileDependencies description. Fixed now.