State of HTTP (Server-side)

Stream: general

[Oliver Dressler]

I'm looking to implement a minimal HTTP server in Lean. Just enough to support basic RPC calls. After a bit of research, I am tending towards building upon https://github.com/hargoniX/socket.lean, which is actively maintained. Is there anything a bit more high-level?

I also saw that the roadmap included a server http library, but I couldn't find any details on it.

[Henrik Böving]

There is infrastructure for asynchronous TCP machinery in internal namespaces of the standard library and @Sofia Rodrigues is actively working to put an HTTP sever on top of that

[Oliver Dressler]

Henrik Böving said:

There is infrastructure for asynchronous TCP machinery in internal namespaces of the standard library and Sofia Rodrigues is actively working to put an HTTP sever on top of that

Great, thanks!
https://github.com/leanprover/lean4/blob/master/src/Std/Internal/Async/TCP.lean looks like a much nicer abstraction. I'll get started using this as the basis, but will probably switch it out for the proper HTTP server once it is available. If you have a (rough) ETA that would be great, otherwise I'll just keep my eyes open for this.

[Tristan Figueroa-Reid]

I'm also quite interested in this - is the source for this on a branch anywhere?

[Sofia Rodrigues]

The code is in this branch. I'm currently fixing some other issues in the Async monad before returning to work on it. It's messy and experimental code, I would love to have some suggestions on how to improve it :)

[Tristan Figueroa-Reid]

Some quick questions:

1. Is Method#allowsRequestBody planning to actually enforce anything?
2. Will Request#uri have a more precise backing structure instead of String?

[Sofia Rodrigues]

Tristan Figueroa-Reid said:

Some quick questions:

1. Is Method#allowsRequestBody planning to actually enforce anything?
2. Will Request#uri have a more precise backing structure instead of String?

1. Yes
2. I'm talking with @Chris Bailey about his URL library, and if he’s interested, I think it would be a great addition to the Std library. Otherwise, I'll create some structures to represent some of the formats described by the RFC 9112.

[Chris Bailey]

Oliver Dressler said:

I'm looking to implement a minimal HTTP server in Lean. Just enough to support basic RPC calls.

As a heads up (to maybe save you some time down the road), there's an existing implementation of JsonRpc in Lean: https://leanprover-community.github.io/mathlib4_docs/Lean/Data/JsonRpc.html#Lean.JsonRpc.Message

[Oliver Dressler]

Chris Bailey said:

Oliver Dressler said:

I'm looking to implement a minimal HTTP server in Lean. Just enough to support basic RPC calls.

As a heads up (to maybe save you some time down the road), there's an existing implementation of JsonRpc in Lean: https://leanprover-community.github.io/mathlib4_docs/Lean/Data/JsonRpc.html#Lean.JsonRpc.Message

Thanks! This implementation seems quite heavily geared towards the LSP. I will use it as an inspiration but dont need the persistence/streaming, custom error codes, etc

[Oliver Dressler]

Sofia Rodrigues said:

The code is in this branch. I'm currently fixing some other issues in the Async monad before returning to work on it. It's messy and experimental code, I would love to have some suggestions on how to improve it :)

I had a quick look. From a usability perspective it would be nice to have

1. Some more logging per request (time & some infos from Request/Response)

2. A bit more context on the Errors, such as

inductive Error where
| entityTooLarge (actual: Nat) (limit: Nat)
-- ...

3. Centralized server config, like maxConnections, keepAliveTimeout, accessLogFormat, ...

On a nitpicky note, it seems Connection#timeoutRecv is not used currently?

In any case, thanks a lot for developing this!

[Oliver Dressler]

This has worked like a charm! Thanks again! Just as a reference, here is the server and client code I use:
https://github.com/oOo0oOo/LeanRPC/blob/main/LeanRPC/HTTP.lean