Zulip Chat Archive

Stream: lean4

Topic: VS Code 0.0.60 - Manual refresh necessary

František Silváši (Jan 31 2022 at 19:52):

After updating the VS Code extension to 0.0.60, my Lean files no longer automatically refresh. I have to restart the lean server for changes to take effect. At first I thought there's been some sneaky option change, but there are errors being reported by the extension:

Error [ERR_STREAM_WRITE_AFTER_END]: write after end
    at Socket.Writable.write (internal/streams/writable.js:292:11)
    at c:\...\.vscode\extensions\leanprover.lean4-0.0.60\out\extension.js:2:552346
    at new Promise (<anonymous>)
    at l.write (c:\...\.vscode\extensions\leanprover.lean4-0.0.60\out\extension.js:2:552264)
    at g.doWrite (c:\...\.vscode\extensions\leanprover.lean4-0.0.60\out\extension.js:2:541871)
    at c:\...\.vscode\extensions\leanprover.lean4-0.0.60\out\extension.js:2:541766

František Silváši (Jan 31 2022 at 19:56):

Might be worth adding that I can peruse existing states in proofs and such just fine, but adding new definitions / theorems / proofs / interactive #evals, etc. does nothing unless I explicitly restart the server.

Gabriel Ebner (Jan 31 2022 at 19:56):

Don't worry, I can reproduce the bug.

Gabriel Ebner (Jan 31 2022 at 19:59):

0.0.61 is out. Can you check if that fixes the issue?

František Silváši (Jan 31 2022 at 20:00):

Sure, give me a second.

František Silváši (Jan 31 2022 at 20:03):

Works like a charm, that was quick, thanks <3.

Last updated: Dec 20 2023 at 11:08 UTC