Is `lean-client-js` library still usable for current Lean4?

Stream: general

[Alissa Tung]

Hello, I am trying to develop something for Lean4. I noticed that there is a lean-client-js library, but there is not many examples, and the vscode-lean4 repo does not refer to it (except the old/ dir). I am curious about is lean-client-js library still usable for current Lean4?

[Marc Huisinga]

The lean-client-js library is for the Lean 3 language server, which used a custom protocol (the Lean Server Protocol). The Lean 4 language server uses a different standardized protocol (the *Language* Server Protocol) that is also used by many other programming languages with some additional extensions to support interactive theorem proving.

To communicate with the Lean 4 language server, vscode-lean4 can mostly reuse an existing client library for the Language Server Protocol called vscode-languageclient. A TypeScript library with types for the protocol can be found at vscode-languageserver-protocol.
The extensions to the Language Server Protocol by Lean 4 can be found in Extra.lean. Some other types have been extended as well and converters.ts provides a clue on what those are.

If you want to develop something for Lean 4, then unless you are writing a new editor plugin, it is unlikely that you want to communicate with Lean 4 using the Language Server Protocol. Instead, you may want to use the meta-programming facilities of Lean 4 or write a custom frontend (see e.g. REPL). Perhaps REPL itself already does what you need, too.

[Alissa Tung]

Marc Huisinga 发言道：

The lean-client-js library is for the Lean 3 language server, which used a custom protocol (the Lean Server Protocol). The Lean 4 language server uses a different standardized protocol (the *Language* Server Protocol) that is also used by many other programming languages with some additional extensions to support interactive theorem proving.

To communicate with the Lean 4 language server, vscode-lean4 can mostly reuse an existing client library for the Language Server Protocol called vscode-languageclient. A TypeScript library with types for the protocol can be found at vscode-languageserver-protocol.
The extensions to the Language Server Protocol by Lean 4 can be found in Extra.lean. Some other types have been extended as well and converters.ts provides a clue on what those are.

If you want to develop something for Lean 4, then unless you are writing a new editor plugin, it is unlikely that you want to communicate with Lean 4 using the Language Server Protocol. Instead, you may want to use the meta-programming facilities of Lean 4 or write a custom frontend (see e.g. REPL). Perhaps REPL itself already does what you need, too.

Thank you for your comprehensive explanation, the suggestions are quiet useful!