why does a sync command take so long in the lean server

Stream: general

[Jason Rute]

In the lean server, if you send a sync command, e.g. even a one line file, and wait for the server to finish syncing (i.e. wait for a a current tasks response with no tasks), it will take about 0.2 seconds. Why? That seems really long in computer time. Is it intentional?

[Jason Rute]

To be more specific, if you send, say,

{"command": "sync", "content": "#eval 1", "file_name": "/test.lean", "seq_num": 100}

then the time it takes to get back

{"message":"file invalidated","response":"ok","seq_num":100}
{"is_running":false,"response":"current_tasks","tasks":[]}

is about .2 seconds. (This is assuming you have already warmed up the server by sending it many requests.)

[Jason Rute]

Ok, it looks like it is intentional.

[Kenny Lau]

looks like I'm not the only one making "XXX is slow" threads :P

[Gabriel Ebner]

The intention behind that delay was to limit the number of messages from the server to the client. With the delay, you get at most 5 messages per second. If you'd send a message every time the server has done something, then there'd be a lot more messages. In the editors, these messages just update the progress bar on the side so there's no need to be super fast.

[Jason Rute]

Yeah, this question is really a consequence of the fact that a number of us are trying to basically hack the language server capability of lean to create a way to programmatically interact with lean. This is really only an issue when I’m trying to interact with Lean in a tight loop. For example, I send something to Lean, see if it works, and based on that send something different to Lean. Anyway, it is annoying but not that big deal since the applications I have in mind can either get around the delay by putting multiple commands in the same file or just live with the delay. Also the language server has larger issues that create more headache for programatic interaction with lean than this delay. Thanks for the answer.

[Patrick Massot]

Yes, we are clearly bending the tool here. But this is not a bug, this is a feature. One of the motivation for my work on lean-client-python is that someone will hopefully soon start working on Lean 4 server mode, (and hopefully that someone is reading Zulip) and I hope to provide input about what users may want besides what we already have.

[Gabriel Ebner]

If you want to interact with Lean in a tight loop, then my suggestion would be to write your own server as a Lean program. Just a small read-eval-print-loop that accepts the commands you want.

[Patrick Massot]

Gabriel, is there already sufficient exposed interface for this in Lean 3?

[Patrick Massot]

If yes then maybe we don't need more in Lean 4.

[Gabriel Ebner]

@Marc Huisinga might want to say something about the Lean 4 server mode. But I think it will just as focused on editor integration as the Lean 3 one.

[Patrick Massot]

Ah, so Marc could be the mysterious someone :)

[Jason Rute]

@Gabriel Ebner Yeah, that is what I intend to do. @Patrick Massot I think it will be a little bit tricky, but the io monad and tactic monads (which can interact with each other) are pretty powerful.

[Sebastian Ullrich]

Yeah, if I understand your use case(s) (ML?) correctly, you should have much better and fine-grained options in Lean 4 such as playing your own elaborator than anything superficial you can do via a server API

[Patrick Massot]

Sebastian, what you say seems fair, but there are still people who will want to interact with Lean from another programming language, building interactive interfaces that don't look like a text editor, hence my experiment with Qt (which comes from a real project by Frédéric and Florian).

[Sebastian Ullrich]

If the LSP is sufficient for your needs, great, but otherwise it's probably easier to write a small Lean 4 library that exposes a C interface to the internal Lean functionality you need. Then you can use that anywhere you want.

[Patrick Massot]

Great, I can't wait to read the tutorial you'll write about this way!

[Sebastian Ullrich]

I thought you'd write it!

[Patrick Massot]

I know :wink:

[Patrick Massot]

I only hope you'll leave enough hints somewhere

[Reid Barton]

Try reading the first letter of every function definition in the elaborator?

[Jason Rute]

I definitely look forward to Lean 4, but I guess I'm too inpatient to wait. :slight_smile: One application I have in mind is as follows, which I think I can implement directly in Lean 3. It would take in the following commands:

1. Give Lean an expression to set as a theorem. Lean creates a new tactic state trying to prove that theorem.
2. Give it a tactic expression to apply (possibly in a restricted tactic DSL) to this state. Lean applies it and gives the state and an index for the state.
3. Given Lean an index for a previously visited state. Lean jumps back to that state.

The largest challenges will be: (1) Creating the tactic DSL which is tedious and I'll do one tactic at a time. (2) Making sure I can set up the environment as needed. (What if my theorem needs a universe u?). (3) Making sure I can enter expressions to Lean either as Lean code or in another form (s-expressions based on the internal Lean expression representation).

[Reid Barton]

Jason Rute said:

(What if my theorem needs a universe u?)

I'm sure this was not meant as an exhaustive list of concerns, but you can write a universe variable in a theorem statement as theorem {u} my_theorem {a : Type u} ...

[Jason Rute]

Wow, I wish I new that earlier! Thanks!

[Mario Carneiro]

it annoys me that there is no place in the grammar to put universe declarations in an example

[Mario Carneiro]

If this is still under construction in lean 4 I would like to vote for the syntax def foo.{u v} {A : Sort u} : A := sorry

[Mario Carneiro]

or example.{u v} ... for examples

[Mario Carneiro]

also what's up with universe shadowing? universe u def {u} foo := Sort u is a hard fail for no apparent reason

[Sebastian Ullrich]

Mario Carneiro said:

If this is still under construction in lean 4 I would like to vote for the syntax def foo.{u v} {A : Sort u} : A := sorry

You're close. https://github.com/leanprover/lean4/blob/master/src/Init/Lean/Parser/Command.lean#L44

[Gabriel Ebner]

Why do we need to declare universes in the first place?

[Sebastian Ullrich]

That's... a good question. Coincidentally I learned about https://github.com/rust-lang/rfcs/blob/master/text/2115-argument-lifetimes.md today, a very similar argument could be made about universes.

[Jason Rute]

Maybe we should make a list of all this things we've tried to hack the Lean server to do so that it is clear the sort of stuff we'd love from Lean 4. Here are some things:

• find all tactic keywords and their states when they are applied (often can do in Lean 3 but with many exceptions)
• find the entire tactic command from beginning to end. (Note really doable in Lean 3.)
• find all instances of the rw tactic (or the have tactic) so I can replace it with another tactic. (Finding tactic instances is hard. The Language server helps, but sometimes behaves weird.)
• replace a tactic- or term-proof of a declaration with another (maybe I'm trying out some automation and I want to see what declarations I can prove with that alone) (I have no idea how to find the start and end of a proof)
• full proof recording (break up a proof into a data structure which can be used to replay the proof).
• record theorems, states, etc in such a way that they can be consistently entered back into Lean. (Often fails in Lean 3 usually because of issues with @.)

[Sebastian Ullrich]

In Lean 3 at least we had universes vs universe variables, but there's only one kind of universe variable in Lean 4

[Patrick Massot]

Sebastian Ullrich [said](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic
You're close. https://github.com/leanprover/lean4/blob/master/src/Init/Lean/Parser/Command.lean#L44

Does this cover `example`? It doesn't look like it does.

[Patrick Massot]

Jason, you last point is known as the pretty-printer roundtrip issue, and they very much work on it. Search for delaborator in Lean 4 code.

[Reid Barton]

Mario Carneiro said:

it annoys me that there is no place in the grammar to put universe declarations in an example

Fun fact: it also doesn't work for instance, even if you add an instance name!

[Chris Wong]

@Sebastian Ullrich Note that the Rust RFC isn't stabilized yet, and is rather controversial. I'm not arguing for or against; just want to make things clear :slight_smile:

[Jason Rute]

@Gabriel Ebner Since you are changing things in the lean server, would you be willing to provide a command line option to drop that 200 ms delay on info requests. For vs code, you probably might still want the delay, but if you use the lean server programmatically from Python, it is an unnecessary slowdown. It is not a huge priority, as I'm not using the lean server right now for much of anything, but it would be a nice to have at some point I think (unless one just wants to wait for Lean 4 if it has a better solution).