How to use lean --server ?

Stream: lean4

[zmkm]

I would like to create a backend server to interact with Lean. I noticed the lean command has --server and --worker flags and so I wonder 1. how these work exactly 2. how to specify the server port 3. what is the JSON format for request and response 4. general tips Thanks!

[Jon Eugster]

You could look at this file from lean4web:

https://github.com/leanprover-community/lean4web/blob/edd9e2c5bc478f757f9bd839eed3c36e3e96432e/server/index.mjs#L85

[zmkm]

Thanks for pointing to this link! If you had to handle say 1024 api requests / second, is it true that lean --server is faster and more memory efficient than lean --run mode? Also, is there some concurrency or parallel mechanism in Lean that allows you to batch run all these requests?