search

leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
136 stars 42 forks source link

Server does not respond to new file #484

Closed b-mehta closed 1 day ago

b-mehta commented 1 week ago

Description

The lean4 server does not display any information or errors on a new file.

Context

Discussion: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Server.20crashes.20on.20new.20file

Steps to Reproduce

1) Have a running Lean server, working on a Lean file 2) Open a new file in VSCode in the same directory 3) Save it as test.lean 4) Write example : 1 = 2 := rfl in the file 5) Save the file 6) No errors are generated.

Expected behavior: The invalid theorem gives an error.

Actual behavior: The invalid theorem does not give an error.

Versions

vscode-lean4 version: 0.0.168 Lean version: 4.9.0-rc2 OS version: MacOS Monterey

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

b-mehta commented 6 days ago

Recording the workaround from the zulip thread for anyone coming across this:

You can close test.lean and then re-open it. Then, when the language client attempts to open the document, VS Code will already have updated window.tabGroups.