lean port

Stream: new members

[Marcin Tomaszewski]

hi, how to find out which port is lean server running on? I run it from visual studio code using lean 3

[Eric Wieser]

I assume you mean port as in TCP port?

[Marcin Tomaszewski]

yes

[Marcin Tomaszewski]

I would like to send a request with started proof to the server by c# program and receive response with new goal
like i send
theorem ...
begin
rw h,
end

and receive response
h:...
a,b \in \N
|- ...

[Scott Morrison]

It's a bit more complicated than that. You may like https://github.com/leanprover-community/repl (for Lean 4)

[Scott Morrison]

Or https://github.com/openai/lean-gym (for Lean 3)

[Marcin Tomaszewski]

i can use the repl.lean, but how can I communicate with this from other console? Say I start one console with repl and I want other program to send back and forth messages to the repl "server". If I cant do this then i have to launch repl everytime