lean --server

Stream: lean4

[Huajian Xin]

I used scripts to interact with Lean 3 server for a long time and I just move to Lean 4. I wonder how should I input request to Lean 4 server? In Lean 3 I usually tried commands like:

>>> lean --server
{"command":"sync","file_name":"","content":"#eval 1+1","seq_num":0}

But it seems to be changed in Lean 4, and how should I input?

[Siddhartha Gadgil]

What do you want to do by interacting with the server? It is likely that the Lean 4 REPL will let you do it easily.