Watchdog error: Cannot read LSP request: A Lean 3 request was received. Please ensure that your editor has a Lean 4 compatible extension installed. For VSCode, this is

leanprover-community / lean-client-python

Python talking to the Lean theorem prover

Apache License 2.0

39 stars 6 forks source link

Watchdog error: Cannot read LSP request: A Lean 3 request was received. Please ensure that your editor has a Lean 4 compatible extension installed. For VSCode, this is #24

Closed enjoysmath closed 1 year ago

enjoysmath commented 1 year ago

Watchdog error: Cannot read LSP request: A Lean 3 request was received. Please ensure that your editor has a Lean 4 compatible extension installed. For VSCode, this is

As you can see I installed Lean4 on the right of the screenshot using Elan.

Please make this useful tool work. Thanks.

eric-wieser commented 1 year ago

This repository is only for Lean 3.

enjoysmath commented 1 year ago

Where's the one for Lean4?

eric-wieser commented 1 year ago

There isn't one, and probably won't ever be; Lean 4 speaks the standard language server protocol rather than inventing its own LSP. Presumably there are python clients somewhere for that.