Can lean print its JSON traffic?

Stream: general

[Daniel Donnelly]

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]

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

[Yury G. Kudryashov]

What is your OS?

[Daniel Donnelly]

What is your OS?

Windows 10

[Andrew Ashworth]

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

[Daniel Donnelly]

64-bit

[Bryan Gin-ge Chen]

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]

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]

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]

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

[Daniel Donnelly]

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

[Yury G. Kudryashov]

@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]

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

[Daniel Donnelly]

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

[Bryan Gin-ge Chen]

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]

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

[Bryan Gin-ge Chen]

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]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

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 }

pasted image

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

[Daniel Donnelly]

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]

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

[Daniel Donnelly]

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

[Daniel Donnelly]

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]

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

[Patrick Massot]

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

[Daniel Donnelly]

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

[Patrick Massot]

You should try lean --help

[Daniel Donnelly]

@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]

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

[Patrick Massot]

That's it.

[Daniel Donnelly]

So it should be -j=0?

[Patrick Massot]

No. -j0.

[Daniel Donnelly]

Then the help command is wrong?

[Daniel Donnelly]

So 0 = infinity here?

[Patrick Massot]

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

[Daniel Donnelly]

I see now. Thank you!

[Daniel Donnelly]

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

[Patrick Massot]

It depends on what you want to be included.

[Bryan Gin-ge Chen]

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]

@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]

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

[Daniel Donnelly]

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