feat: small changes

Author: algebraic-dev

DNS.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sofia Rodrigues
+-/
+module
+
+prelude
+public import Std.Time
+public import Std.Internal.UV
+public import Std.Internal.Async.Basic
+
+public section
+
+namespace Std
+namespace Internal
+namespace IO
+namespace Async
+namespace DNS
+
+open Std.Net
+
+/--
+Represents a resolved hostname and service name from a socket address.
+-/
+structure NameInfo where
+  /--
+  The resolved hostname (e.g., "example.com").
+  -/
+  host : String
+
+  /--
+  The service name (e.g., "http" for port 80).
+  -/
+  service : String
+
+/--
+Asynchronously resolves a hostname and service to an array of socket addresses.
+-/
+@[inline]
+def getAddrInfo (host : String) (service : String) (addrFamily : Option AddressFamily := none) : Async (Array IPAddr) := do
+  Async.ofPromise <| UV.DNS.getAddrInfo
+    host
+    service
+    (match addrFamily with
+    | none => 0
+    | some .ipv4 => 1
+    | some .ipv6 => 2)
+
+/--
+Performs a reverse DNS lookup on a `SocketAddress`.
+-/
+@[inline]
+def getNameInfo (host : @& SocketAddress) : Async NameInfo :=
+  UV.DNS.getNameInfo host
+  |> Async.ofPromise
+  |>.map (Function.uncurry NameInfo.mk)
+
+end DNS
+end Async
+end IO
+end Internal
+end Std

src/Std/Internal/Async/Basic.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.System.Promise
+public meta import Lean.Elab.Term
 
 public section
 
@@ -306,11 +307,21 @@ def block (x : AsyncTask α) : IO α :=
   | .ok a => return a
   | .error e => .error e
 
+syntax "currFunctionError%" : term
+
+elab_rules : term
+| `(currFunctionError%) => do
+  let declName? ← Lean.Elab.Term.getDeclName?
+  let fnName := match declName? with
+    | some name => s!"the promise linked to `{name}` was dropped"
+    | none => "the promise linked to the Async was dropped"
+  Lean.Elab.Term.elabTerm (← `($(Lean.quote fnName))) none
+
 /--
 Create an `AsyncTask` that resolves to the value of `x`.
 -/
 @[inline]
-def ofPromise (x : IO.Promise (Except IO.Error α)) (error : String := "the promise linked to the Async Task was dropped") : AsyncTask α :=
+def ofPromise (x : IO.Promise (Except IO.Error α)) (error : String := by exact currFunctionError%) : AsyncTask α :=
   x.result?.map fun
     | none => .error error
     | some res => res
@@ -319,7 +330,7 @@ def ofPromise (x : IO.Promise (Except IO.Error α)) (error : String := "the prom
 Create an `AsyncTask` that resolves to the value of `x`.
 -/
 @[inline]
-def ofPurePromise (x : IO.Promise α) (error : String := "the promise linked to the Async Task was dropped") : AsyncTask α :=
+def ofPurePromise (x : IO.Promise α) (error : String := by exact currFunctionError%) : AsyncTask α :=
   x.result?.map (sync := true) fun
     | none => .error error
     | some res => pure res
@@ -884,7 +895,7 @@ protected def block (x : Async α) (prio := Task.Priority.default) : IO α :=
 Converts `Promise` into `Async`.
 -/
 @[inline]
-protected def ofPromise (task : IO (IO.Promise (Except IO.Error α))) (error : String := "the promise linked to the Async was dropped") : Async α := do
+protected def ofPromise (task : IO (IO.Promise (Except IO.Error α))) (error : String := by exact currFunctionError%) : Async α := do
   match ← task.toBaseIO with
   | .ok data => pure (f := BaseIO) <| MaybeTask.ofTask <| data.result?.map fun
     | none => .error error
@@ -925,7 +936,7 @@ protected def ofTask (task : Task α) : Async α := do
 Converts `IO (IO.Promise α)` to `Async`.
 -/
 @[inline]
-protected def ofPurePromise (task : IO (IO.Promise α)) (error : String := "the promise linked to the Async was dropped") : Async α := show BaseIO _ from do
+protected def ofPurePromise (task : IO (IO.Promise α)) (error : String := by exact currFunctionError%) : Async α := show BaseIO _ from do
   match ← task.toBaseIO with
   | .ok data => pure <| MaybeTask.ofTask <| data.result?.map fun
     | none => .error error

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

@@ -29,32 +29,32 @@ structure Config where
   /--
   Maximum number of requests per connection (for keep-alive).
   -/
-  maxRequestsPerConnection : Nat := 100
+  maxRequestsPerConnection : Nat := 1000
 
   /--
   Maximum number of headers allowed per response.
   -/
-  maxResponseHeaders : Nat := 50
+  maxResponseHeaders : Nat := 200
 
   /--
   Maximum size of a single header value in bytes.
   -/
-  maxHeaderValueSize : Nat := 8192
+  maxHeaderValueSize : Nat := 16384
 
   /--
   Maximum waiting time for additional data before timing out.
   -/
-  readTimeout : Time.Millisecond.Offset := 5000
+  readTimeout : Time.Millisecond.Offset := 30000
 
   /--
   Timeout duration for keep-alive connections.
   -/
-  keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨45000, by decide⟩
+  keepAliveTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨60000, by decide⟩
 
   /--
   Timeout for the entire request lifecycle (connect + read + write).
   -/
-  requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨10000, by decide⟩
+  requestTimeout : { x : Time.Millisecond.Offset // 0 < x } := ⟨120000, by decide⟩
 
   /--
   Whether to enable keep-alive connections.
@@ -69,17 +69,17 @@ structure Config where
   /--
   Maximum number of bytes to receive in a single read call.
   -/
-  maxRecvChunkSize : Nat := 8192
+  maxRecvChunkSize : Nat := 16384
 
   /--
   Default buffer size for request payloads.
   -/
-  defaultRequestBufferSize : Nat := 8192
+  defaultRequestBufferSize : Nat := 16384
 
   /--
   The user-agent string to send by default.
   -/
-  userAgent : Option HeaderValue := some (.new "LeanHTTPClient/1.1")
+  userAgent : Option HeaderValue := some (.new "lean-http/1.1")
 
 namespace Config