vscode questions

Stream: general

[Vadim Zaliva]

I am learning my ropes using Lean4 in vscode and have some questions. For example:

1. If there is a way to "restart" all out of date files? After git pull from upstream I have go in vscode through changes files and manuall do "Restart file" command for each.
2. Selecting goals in LeanInfo view and copying to clipboard is tricky. It loses focus, copy does not work sometimes

[Vadim Zaliva]

Maybe we should have a #vscode-lean channel ?

[Bolton Bailey]

1. Perhaps the "Restart Server" command? Restart file should restart all files below the current file in the import tree.
2. Not sure what exactly is causing your problem here, but yes the things you see in the infoview are not always themselves things that compile when copied into a file.

[Vadim Zaliva]

thanks for "Restart server" hint. it worked. For copy selection, I've opened an issue. It looks like a bug to me https://github.com/leanprover/vscode-lean4/issues/653

[Eric Wieser]

That link goes to issues created by the person who clicked it

[Vadim Zaliva]

sorry. fixed.

[Marc Huisinga]

Vadim Zaliva said:

1. If there is a way to "restart" all out of date files? After git pull from upstream I have go in vscode through changes files and manuall do "Restart file" command for each.

Running the 'Build Project' command from the VS Code extension will build the full project and restart the server while doing so, which ensures that you won't have any outdated build artifacts anymore.

Vadim Zaliva said:

2. Selecting goals in LeanInfo view and copying to clipboard is tricky. It loses focus, copy does not work sometimes

Thanks for creating the issue - I think this is fixable (both the context menu and the selections are handled by VS Code, but I think our term highlighting is probably confusing it). On the new pre-release of the extension (0.0.210) you can also right click on the goal state and select the 'Copy State' entry to copy the whole thing.