This repository was archived by the owner on Oct 14, 2023. It is now read-only.
This repository was archived by the owner on Oct 14, 2023. It is now read-only.
Documentation for lean --server #1996
Open
Description
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.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
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.
Metadata
Metadata
Assignees
Labels
No labels