Documentation for lean --server

[whitequark]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Is there any documentation for lean --server? I want to implement a Lean mode for Sublime Text (similar to my Coq mode) but I wasn't able to find any documentation for the server protocol. I looked at the source code but I don't really understand it just from that. A high-level introduction would be appreciated.

[cipher1024]

Development of Lean 3 has stopped as the developers focus on Lean 4. You can post your issue on the community fork of Lean instead: https://github.com/leanprover-community/lean/issues. But the short answer may be that you'll have to write that documentation yourself as you discover how it works.

[Kha]

Yes, the server mode is sorely lacking documentation because most clients so far have been written by core developers. The lean-client-js server API should at least be much more readable than the C++ code. There's also an LSP implementation in that repo, which AFAIK is used by the vim client (but not by the VS Code extension).

In general, most requests should be relatively self-explanatory, perhaps with the exception of the roi request. This "range of interest" determines what parts of a file should be processed; for parts outside the ROI, neither informational nor error messages will be reported. At least in Emacs, the entire client-server communication can also be inspected by lean-turn-on-debug-mode.

[PatrickMassot]

Other sources of information:

• the original discussion at [RFC] New lean server protocol #1227
• https://github.com/leanprover/lean-client-js/blob/master/lean-client-js-core/src/commands.ts (this is a more specific version of Sebastian's suggestion)
• you can have a look at https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/server.py which is a rough python interface which is enough to produce the tactic state display in https://www.math.u-psud.fr/~pmassot/lean/ for instance (you need to click on math to see Lean code and then click on the darker areas around Lean lines to see the tactic state)

[whitequark]

Thanks everyone!