Zulip Chat Archive
Stream: lean4
Topic: Stop server in VSCode?
Mac (May 03 2021 at 19:01):
Is there a way to stop the Lean server altogether in VS Code? When rebuilding the Lean sources in VS Code, the build can fail because the previously built Lean is already running in as the Lean server for VS Code (and thus it can't overwrite the executable). Thus, if I could start the server before building and then start it again after, I could get around this issue.
Mario Carneiro (May 03 2021 at 19:02):
Does the server build the executable? I would have assumed not
Sebastian Ullrich (May 03 2021 at 19:17):
Wow, I assume you're on Windows?
Gabriel Ebner (May 03 2021 at 19:29):
See also this change in Lean 3: https://github.com/leanprover-community/lean/commit/667e1e138162ef6d65a2041abfe760a7aa79c2c5
Mac (May 03 2021 at 20:00):
Sebastian Ullrich said:
Wow, I assume you're on Windows?
Yep, I'm on Windows.
Sebastian Ullrich (May 03 2021 at 20:15):
Ok, then we should use something like the commit linked by Gabriel so that the server doesn't have to be stopped at all
Mac (May 03 2021 at 20:31):
Sounds great! That would be even more convient!
Sebastian Ullrich (May 03 2021 at 20:38):
If anyone wants to figure this out and test it, please go ahead :big_smile:
Mac (May 14 2021 at 15:59):
Fyi, in addition to this problem appearing while building a new Lean while the server is running, it also appears if one runs elan update on a toolchain while the toolchain server is running.
Mac (May 14 2021 at 15:59):
That is, the issue is also (Lean 4) user-facing in addition to (Lean 4) developer-facing.
Last updated: Dec 20 2023 at 11:08 UTC