Lean server

Stream: lean4

[Arthur Paulino]

Hm, is there an example of a valid request that can be queried to the lean4 server? I'm struggling to get a valid response

[Notification Bot]

Arthur Paulino has marked this topic as unresolved.

[Arthur Paulino]

It keeps saying Watchdog error: Cannot read LSP request: Invalid header field: ...

[Mario Carneiro]

I think the easiest way to get some valid communication is to snoop on vscode; there is a setting you can enable to make any LSP extension print all traffic

[Mario Carneiro]

Another way to snoop is to make vscode call my_lean which is a shell script like tee in.txt | lean --server | tee out.txt

[Arthur Paulino]

Thanks! I wanna see how far I can go with this. I had never heard of LSP before so it's a learning experience :D

[Arthur Paulino]

Which extension should I use? Seems like the lean one isn't compatible with Lean 4. Is it the case?

[Arthur Paulino]

image.png I'm getting similar errors. The plugin seems to be trying to send requests to the lean3 server

[Mac]

@Arthur Paulino you should be using the lean4 extension for Lean 4. The lean extension is for Lean 3.

[Arthur Paulino]

Mario Carneiro said:

I think the easiest way to get some valid communication is to snoop on vscode; there is a setting you can enable to make any LSP extension print all traffic

Searched a lot but couldn't find such setting. does the lean4 plugin have it available?

[Arthur Paulino]

Nevermind, I think I found it

[Wojciech Nawrocki]

@Arthur Paulino in the VSCode settings, these are the Server Logging settings from the Lean 4 extension.

[Arthur Paulino]

Alright I was able to extract a request from the log:

{"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/arthur/ex.lean","languageId":"lean4","version":1,"text":"variable (p q: Prop)\n\nexample : p ↔ p := by\n  apply Iff.intro\n  {intro h; apply h}\n  {intro h; apply h}"}}}

But then I call lean --server < in.json and it responds

Watchdog error: Cannot read LSP request: Invalid header field: {"jsonrpc":"2.0","method":"textDocument/didOpen","params":{"textDocument":{"uri":"file:///home/arthur/ex.lean","languageId":"lean4","version":1,"text":"variable (p q: Prop)\n\nexample : p ↔ p := by\n  apply Iff.intro\n  {intro h; apply h}\n  {intro h; apply h}"}}}

[Arthur Paulino]

I suspect I am doing something fundamentally wrong

[Sebastian Ullrich]

The log does not include the HTTP-like LSP headers, see https://github.com/leanprover/lean4/blob/master/tests/lean/server/open_content.log and other .log files in that directory

[Sebastian Ullrich]

It would probably be easier to a) write the whole REPL in Lean or, if you e.g. want to use a readline-like library that has not yet been packaged for Lean, b) use a custom protocol between the main REPL program and a custom Lean program, where "protocol" could be as simple as "a single escaped line per request and response"

[Arthur Paulino]

How would that custom Lean program be? How would it communicate with the main REPL program?

[Sebastian Ullrich]

Read from IO.getStdin, write via IO.println :)

[Arthur Paulino]

The value read would be a string right? how to execute lean string code inside lean itself?