feat: small changes

Author: algebraic-dev

src/Std/Internal/Async/Basic.lean

@@ -138,6 +138,13 @@ Construct an `ETask` that is already resolved with value `x`.
 protected def pure (x : α) : ETask ε α :=
   Task.pure <| .ok x
 
+/--
+Returns `true` if a `ETask` has finished it's execution
+-/
+@[inline]
+protected def isFinished (x : ETask ε α) : BaseIO Bool := do
+  return (← IO.getTaskState x) == IO.TaskState.finished
+
 /--
 Creates a new `ETask` that will run after `x` has finished. If `x`:
 - errors, return an `ETask` that resolves to the error.
@@ -242,6 +249,13 @@ Construct an `AsyncTask` that is already resolved with value `x`.
 protected def pure (x : α) : AsyncTask α :=
   Task.pure <| .ok x
 
+/--
+Returns `true` if a `AsyncTask` has finished it's execution
+-/
+@[inline]
+protected def isFinished (x : AsyncTask α) : BaseIO Bool := do
+  return (← IO.getTaskState x) == IO.TaskState.finished
+
 /--
 Create a new `AsyncTask` that will run after `x` has finished.
 If `x`:

src/Std/Internal/Http/Data/Body/ByteStream.lean

@@ -92,10 +92,8 @@ and contains some data.
 -/
 def tryRecv (stream : ByteStream) : Async (Option ByteArray) := do
   stream.state.atomically do
-    match ← tryRecvFromBuffer' with
-    | some ⟨#[], _⟩ => pure none
-    | none => pure none
-    | some res => pure (some res.toByteArray)
+    let buf ← tryRecvFromBuffer'
+    return Util.BufferBuilder.toByteArray <$> buf
 
 /--
 Receives (reads) all currently available data from the stream, emptying it.

src/Std/Internal/Http/Data/Method.lean

@@ -85,36 +85,6 @@ def fromString? : String → Option Method
   | "PATCH" => some .patch
   | _ => none
 
-/--
-Request methods are considered safe if their defined semantics are essentially read-only.
-
-* Reference: https://httpwg.org/specs/rfc9110.html#method.properties
--/
-def isSafe : Method → Prop
-  | .get | .head | .options | .trace => True
-  | _ => False
-
-/--
-A request method is considered idempotent if the intended effect on the server of multiple
-identical requests with that method is the same as the effect for a single such request.
-
-* Reference: https://httpwg.org/specs/rfc9110.html#idempotent.methods
--/
-def isIdempotent : Method → Prop
-  | .get | .head | .options | .trace => True
-  | .put | .delete => True
-  | _ => False
-
-/--
-Checks if the given method allows a request body. GET and HEAD methods do not typically allow
-request bodies.
-
-* Reference: https://developer.mozilla.org/en-US/docs/Web/HTTP/Methods
--/
-def allowsRequestBody : Method → Bool
-  | .get | .head => False
-  | _ => True
-
 instance : ToString Method where
   toString
     | .get => "GET"

src/Std/Internal/Http/Data/Request.lean

@@ -81,13 +81,6 @@ instance : ToString Head where
     "\r\n" ++
     toString req.headers ++ "\r\n\r\n"
 
-/--
-Determines if a request method typically doesn't allow a request body
--/
-@[inline]
-def isInformational (request : Head) : Bool :=
-  ¬request.method.allowsRequestBody
-
 /--
 Creates a new HTTP Request builder with default head (method: GET, version: HTTP/1.1, asterisk URI, empty headers)
 -/

src/Std/Internal/Http/Protocol/H1.lean

@@ -42,11 +42,6 @@ structure Config where
   -/
   maxHeaderSize : Nat := 8192
 
-  /--
-  Connection timeout in milliseconds.
-  -/
-  timeoutMilliseconds : Time.Millisecond.Offset := 1000
-
   /--
   Whether to enable keep-alive connections by default.
   -/
@@ -62,11 +57,6 @@ structure Config where
   -/
   serverName : Option HeaderValue := some (.new "LeanHTTP/1.1")
 
-  /--
-  Default buffer size for the connection
-  -/
-  defaultPayloadBytes : Nat := 8192
-
 /--
 Specific HTTP processing errors with detailed information.
 -/

src/Std/Internal/Http/Server.lean

@@ -22,18 +22,13 @@ open Time
 Serve conection
 -/
 def serve
-  (addr : Net.SocketAddress)
-  (onRequest : Request Body → Async (Response Body))
-  (onReady : Async Unit := pure ())
-  (onFailure : Error → Async Unit := fun _ => pure ())
-  (config : Config := {})
-  (backlog : UInt32 := 128) : Async Unit := do
-    let server ← Socket.Server.mk
-    server.bind addr
-    server.listen backlog
+    (addr : Net.SocketAddress)
+    (onRequest : Request Body → Async (Response Body))
+    (config : Config := {}) (backlog : UInt32 := 128) : Async Unit := do
+  let server ← Socket.Server.mk
+  server.bind addr
+  server.listen backlog
 
-    onReady
-
-    while true do
-      let client ← server.accept
-      background (prio := .max) <| serveConnection client onRequest onFailure config
+  while true do
+    let client ← server.accept
+    background (prio := .max) <| serveConnection client onRequest config

src/Std/Internal/Http/Server/ClientConnection.lean

@@ -134,7 +134,6 @@ Close the mock connection and notify all waiters.
 def close (client : Mock.Client) : BaseIO Unit := do
   client.state.atomically do
     let st ← get
-    -- Notify all waiting consumers that connection is closed
     for consumer in st.consumers.toArray do
       discard <| consumer.resolve none
 
@@ -202,7 +201,6 @@ private def recvReady' : AtomicT MockClient.State Async Bool := do
 Receive data from the mock client, simulating network behavior.
 -/
 def recv? (client : Mock.Client) (size : UInt64) : Async (Option ByteArray) := do
-  -- Try to get data immediately
   client.state.atomically do
     if let some data ← tryRecv' size then
       return (some data)

src/Std/Internal/Http/Server/Config.lean

@@ -34,9 +34,19 @@ structure Config where
   maxHeaderSize : Nat := 8192
 
   /--
-  Connection timeout in milliseconds.
+  Maximum waiting time for more data.
   -/
-  timeoutMilliseconds : Time.Millisecond.Offset := 1000
+  lingeringTimeout : Time.Millisecond.Offset := 5000
+
+  /--
+  Timeout for keep-alive connections
+  -/
+  keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } :=  ⟨45000, by decide⟩
+
+  /--
+  Maximum timeout time for request more data.
+  -/
+  requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨10000, by decide⟩
 
   /--
   Whether to enable keep-alive connections by default.
@@ -49,7 +59,12 @@ structure Config where
   highMark : Nat := 4096
 
   /--
-  Default buffer size for the connection.
+  The maximum size that the connection can receive in a single recv call.
+  -/
+  maximumRecvSize : Nat := 8192
+
+  /--
+  Default buffer size for the connection
   -/
   defaultPayloadBytes : Nat := 8192
 
@@ -67,7 +82,6 @@ def toH1Config (config : Config) : Protocol.H1.Machine.Config :=
   { maxRequests := config.maxRequests
     maxHeaders := config.maxHeaders
     maxHeaderSize := config.maxHeaderSize
-    timeoutMilliseconds := config.timeoutMilliseconds
     enableKeepAlive := config.enableKeepAlive
     highMark := config.highMark
     serverName := config.serverName