Zulip Chat Archive

Stream: general

Topic: Can lean print its JSON traffic?


view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:14):

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

view this post on Zulip Yury G. Kudryashov (Dec 04 2019 at 20:14):

What is your OS?

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:15):

What is your OS?

Windows 10

view this post on Zulip 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

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:15):

64-bit

view this post on Zulip 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}

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Dec 04 2019 at 20:17):

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

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:17):

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

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:18):

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

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:19):

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

view this post on Zulip 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".

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:19):

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

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:21):

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

view this post on Zulip 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.

view this post on Zulip 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 }


pasted image

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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Dec 04 2019 at 20:54):

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

view this post on Zulip Patrick Massot (Dec 04 2019 at 20:55):

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

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 20:57):

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

view this post on Zulip Patrick Massot (Dec 04 2019 at 20:57):

You should try lean --help

view this post on Zulip 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)

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:00):

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

view this post on Zulip Patrick Massot (Dec 04 2019 at 21:01):

That's it.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:01):

So it should be -j=0?

view this post on Zulip Patrick Massot (Dec 04 2019 at 21:01):

No. -j0.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:01):

Then the help command is wrong?

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:02):

So 0 = infinity here?

view this post on Zulip Patrick Massot (Dec 04 2019 at 21:03):

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

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:06):

I see now. Thank you!

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Dec 04 2019 at 21:18):

It depends on what you want to be included.

view this post on Zulip 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".

view this post on Zulip 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.

view this post on Zulip Daniel Donnelly (Dec 04 2019 at 21:22):

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

view this post on Zulip 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