Skip to content
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
@whitequark

Description

@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.
    • 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions