## Stream: general

### Topic: Can lean print its JSON traffic?

#### Daniel Donnelly (Dec 04 2019 at 20:09):

I am not understanding how the commands.ts file works. I was thinking I could write a program that just acts as a stdio reader and shows me all traffic both ways. Or, I could ask you if there's the ability to switch that on at the command line. Or if not could someone write a simple "printf()" routine that prints out the JSON to VSCode's terminal? That would save me a lot of trouble. By that I mean actually modifying lean. I'm not sure how to do that myself.

#### Daniel Donnelly (Dec 04 2019 at 20:14):

Can someone give me simple instructions how to build lean 4?

What is your OS?

What is your OS?

Windows 10

#### Andrew Ashworth (Dec 04 2019 at 20:15):

Lean 4 might be a little premature. I tried building it with MinGW a few months ago and it didn't work

64-bit

#### Bryan Gin-ge Chen (Dec 04 2019 at 20:15):

I'm not sure I understand your question, but if you run lean --server at the command line, you can type or paste in JSON commands, following the outputs of the functions in server.ts. For example, you can input:

{"command":"sync", "file_name":"test.lean", "content":"example : true := sorry", "seq_num":0}
{"command":"info", "file_name":"test.lean", "line":1, "column":10, "seq_num":0}


#### Daniel Donnelly (Dec 04 2019 at 20:16):

Yes, but I don't know what to type in. If I could use lean normally and see all traffic, that would be ideal.

#### Daniel Donnelly (Dec 04 2019 at 20:17):

Oh you're saying look at the lines:
return this.send({command: 'info', file_name: file, line, column}
etc and that is exactly the json?

#### Bryan Gin-ge Chen (Dec 04 2019 at 20:17):

It's close, for instance, it's missing the seq_num key.

#### Daniel Donnelly (Dec 04 2019 at 20:17):

So what is the start-up sequence for Lean in JSON commands?

#### Yury G. Kudryashov (Dec 04 2019 at 20:18):

@Bryan Gin-ge Chen I think that @Daniel Donnelly wants to see all the JSON traffic that goes between VS and Lean. On Linux I'd suggest some short bash script based on tee and redirection.

#### Daniel Donnelly (Dec 04 2019 at 20:18):

Can't someone just build me a binary that prints it all ?

#### Daniel Donnelly (Dec 04 2019 at 20:19):

Then in VSCode I could set the exec setting to that binary

#### Bryan Gin-ge Chen (Dec 04 2019 at 20:19):

If I could use lean normally and see all traffic, that would be ideal.

If you're not opposed to fooling around in the browser, you can do this in the online lean editor: https://leanprover-community.github.io/lean-web-editor/

Click the (?) to open the modal popup, then scroll to the bottom and check "Log server messages to console".

#### Daniel Donnelly (Dec 04 2019 at 20:19):

@Bryan Gin-ge Chen that's awesome! I will try it now

#### Bryan Gin-ge Chen (Dec 04 2019 at 20:20):

Then open your browser's dev console and you should see messages like this:

15:17:33.006 => server:   { command: "info", file_name: "/test.lean", line: 6, column: 33 }
15:17:33.009 <= server:   { response: "ok", seq_num: 2 }


#### Bryan Gin-ge Chen (Dec 04 2019 at 20:20):

It's possible to do something similar with the VS Code extension, but it's a bunch more steps.

#### Daniel Donnelly (Dec 04 2019 at 20:21):

@Bryan Gin-ge Chen This is perfect. Thank you!

#### Daniel Donnelly (Dec 04 2019 at 20:21):

Now I just have to open the executable with python which is out of the scope of here.

#### Daniel Donnelly (Dec 04 2019 at 20:29):

Then open your browser's dev console and you should see messages like this:

15:17:33.006 => server: { command: "info", file_name: "/test.lean", line: 6, column: 33 }
15:17:33.009 <= server: { response: "ok", seq_num: 2 }




What is all that under __proto__ and is that present in the JSON?

#### Daniel Donnelly (Dec 04 2019 at 20:38):

Also, should I have one LeanInterface (ie. a python subprocess instance) per file or should I have a singleton LeanInterface that works on all files?

#### Patrick Massot (Dec 04 2019 at 20:44):

Did you already look at https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/server.py?

#### Daniel Donnelly (Dec 04 2019 at 20:52):

@Patrick Massot thanks that's truely helpful. It shows all the stuff I actually need right now!

#### Daniel Donnelly (Dec 04 2019 at 20:54):

To answer my own question, since the online thing has an open / save feature, I opened up a local .lean file and it just sends a sync command to the server. So in that case it's a singleton server instance I should be doing.

#### Patrick Massot (Dec 04 2019 at 20:54):

That file is really rudimentary. It's exactly what I needed at that time, no more.

#### Patrick Massot (Dec 04 2019 at 20:55):

But turning it into a general purpose tool could be very useful.

#### Daniel Donnelly (Dec 04 2019 at 20:57):

@Patrick Massot what is -j0 flag or should I just drop that?

#### Patrick Massot (Dec 04 2019 at 20:57):

You should try lean --help

#### Daniel Donnelly (Dec 04 2019 at 21:00):

@Patrick Massot closest match is:
--threads=num -j number of threads used to process lean files

Lean (version 3.4.2, commit cbd2b6686ddb, Release)

#### Daniel Donnelly (Dec 04 2019 at 21:00):

@Patrick Massot that's not quite the format you have with j0

That's it.

#### Daniel Donnelly (Dec 04 2019 at 21:01):

So it should be -j=0?

#### Patrick Massot (Dec 04 2019 at 21:01):

No. -j0.

#### Daniel Donnelly (Dec 04 2019 at 21:01):

Then the help command is wrong?

#### Daniel Donnelly (Dec 04 2019 at 21:02):

So 0 = infinity here?

#### Patrick Massot (Dec 04 2019 at 21:03):

What's wrong? There is = in the long name version, not the short name version.

#### Daniel Donnelly (Dec 04 2019 at 21:06):

I see now. Thank you!

#### Daniel Donnelly (Dec 04 2019 at 21:16):

@Patrick Massot should LEAN_PATH be the user's workspace directory or is that always pointing to the lean base folder?

#### Patrick Massot (Dec 04 2019 at 21:18):

It depends on what you want to be included.

#### Bryan Gin-ge Chen (Dec 04 2019 at 21:18):

the __proto__ stuff is not part of the JSON. It shows up because the JSON gets parsed into a JS object and the browser console shows its "prototype chain".

#### Daniel Donnelly (Dec 04 2019 at 21:21):

@Bryan Gin-ge Chen thanks. Well the working directory lean uses seems to be the root of my application
Since i've pasted in a test.lean file and the server now responds with something other than error.

#### Daniel Donnelly (Dec 04 2019 at 21:22):

I've put the lean executable into a subfolder
Does that violate the license?

#### Daniel Donnelly (Dec 04 2019 at 21:23):

It's my_ide/lean/bin/lean.exe

Last updated: May 10 2021 at 00:31 UTC