Skip to content

How to solve the input issue of the v4.8 repl server? #86

@Kouer-www

Description

@Kouer-www

I encountered an issue related to Lean REPL 4.8. (I have some reasons that necessitate the use of this version.)When used as a server, Lean REPL 4.8 requires three '\n' characters to get a response, unlike Lean REPL 4.11, which only needs two. However, using three '\n' characters triggers a formatting issue that causes the server to shut down. Is it possible to modify the internal code of the REPL so that it recognizes two '\n' characters as sufficient for a response?

Image

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