fix: async task assertions in tests by replacing assert! with assertBEq (#7729)

This PR replaces `assert!` with `assertBEq` to fix issues where asserts
didn't trigger the `ctest` due to being in a separate task. This was
caused by panics not being caught in tasks, while IO errors were handled
by the `AsyncTask` if we use the `block` function on them.

---------

Co-authored-by: Henrik Böving <hargonix@gmail.com>

tests/lean/run/async_tcp_fname_errors.lean

@@ -1,5 +1,3 @@
-#exit  -- TODO: sometimes times out, due to runtime timing changes?
-
 import Std.Internal.Async
 import Std.Internal.UV
 import Std.Net.Addr
@@ -7,6 +5,12 @@ import Std.Net.Addr
 open Std.Internal.IO.Async
 open Std.Net
 
+def assertBEq [BEq α] [ToString α] (actual expected : α) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError <|
+      s!"expected '{expected}', got '{actual}'"
+
+
 -- Define the Async monad
 structure Async (α : Type) where
   run : IO (AsyncTask α)
@@ -31,17 +35,13 @@ instance : MonadLift IO Async where
 
 /-- Mike is another client. -/
 def runMike (client: TCP.Socket.Client) : Async Unit := do
-  let mes ← await (client.recv? 1024)
-  assert! String.fromUTF8!<$>  mes == some "hi mike!! :)"
-  await (client.send (String.toUTF8 "hello robert!!"))
-  await (client.shutdown)
+  let message ← await (client.recv? 1024)
+  assertBEq (String.fromUTF8? =<< message) none
 
 /-- Joe is another client. -/
 def runJoe (client: TCP.Socket.Client) : Async Unit := do
-  let mes ← await (client.recv? 1024)
-  assert! String.fromUTF8!<$>  mes == some "hi joe! :)"
-  await (client.send (String.toUTF8 "hello robert!"))
-  await client.shutdown
+  let message ← await (client.recv? 1024)
+  assertBEq (String.fromUTF8? =<< message) none
 
 /-- Robert is the server. -/
 def runRobert (server: TCP.Socket.Server) : Async Unit := do
@@ -49,19 +49,19 @@ def runRobert (server: TCP.Socket.Server) : Async Unit := do
   discard <| await server.accept
 
 def clientServer : IO Unit := do
-  let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8080
+  let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8083
 
   let server ← TCP.Socket.Server.mk
   server.bind addr
   server.listen 128
 
-  assert! (← server.getSockName).port == 8080
+  assertBEq (← server.getSockName).port 8083
 
   let joe ← TCP.Socket.Client.mk
   let task ← joe.connect addr
   task.block
 
-  assert! (← joe.getPeerName).port == 8080
+  assertBEq (← joe.getPeerName).port 8083
 
   joe.noDelay
 
@@ -69,16 +69,20 @@ def clientServer : IO Unit := do
   let task ← mike.connect addr
   task.block
 
-  assert! (← mike.getPeerName).port == 8080
+  assertBEq (← mike.getPeerName).port 8083
 
   mike.noDelay
 
   let serverTask ← (runRobert server).run
 
-  discard <| (runJoe joe).run
-  discard <| (runMike mike).run
+  let joeTask ← (runJoe joe).run
+  let mikeTask ← (runMike mike).run
+
   serverTask.block
 
+  joeTask.block
+  mikeTask.block
+
 end Async
 
 #eval Async.clientServer

tests/lean/run/async_tcp_half.lean

@@ -5,6 +5,12 @@ import Std.Net.Addr
 open Std.Internal.IO.Async
 open Std.Net
 
+-- Using this function to create IO Error. For some reason the assert! is not pausing the execution.
+def assertBEq [BEq α] [ToString α] (actual expected : α) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError <|
+      s!"expected '{expected}', got '{actual}'"
+
 -- Define the Async monad
 structure Async (α : Type) where
   run : IO (AsyncTask α)
@@ -41,13 +47,13 @@ def listenClose : IO Unit := do
   server.listen 128
 
 def acceptClose : IO Unit := do
-  let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8082
+  let addr := SocketAddressV4.mk (.ofParts 127 0 0 1) 8081
 
   let server ← TCP.Socket.Server.mk
   server.bind addr
   server.listen 128
 
-  let _ ← (runJoe addr).run
+  let joeTask ← (runJoe addr).run
 
   let task ← server.accept
   let client ← task.block
@@ -55,12 +61,15 @@ def acceptClose : IO Unit := do
   let mes ← client.recv? 1024
   let msg ← mes.block
 
-  assert! (String.fromUTF8! <$> msg) == "hello robert!"
+  assertBEq (String.fromUTF8? =<< msg) ("hello robert!")
 
   let mes ← client.recv? 1024
   let msg ← mes.block
 
-  assert! (String.fromUTF8! <$> msg) == none
+  assertBEq (String.fromUTF8? =<< msg) none
+
+  -- Waiting to avoid errors from escaping.
+  joeTask.block
 
 #eval acceptClose
 #eval listenClose

tests/lean/run/async_tcp_server_client.lean

@@ -1,5 +1,3 @@
-#exit  -- TODO: sometimes times out, due to runtime timing changes?
-
 import Std.Internal.Async
 import Std.Internal.UV
 import Std.Net.Addr
@@ -7,6 +5,12 @@ import Std.Net.Addr
 open Std.Internal.IO.Async
 open Std.Net
 
+-- Using this function to create IO Error. For some reason the assert! is not pausing the execution.
+def assertBEq [BEq α] [ToString α] (actual expected : α) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError <|
+      s!"expected '{expected}', got '{actual}'"
+
 -- Define the Async monad
 structure Async (α : Type) where
   run : IO (AsyncTask α)
@@ -32,14 +36,14 @@ instance : MonadLift IO Async where
 /-- Mike is another client. -/
 def runMike (client: TCP.Socket.Client) : Async Unit := do
   let mes ← await (client.recv? 1024)
-  assert! String.fromUTF8! <$> mes == some "hi mike!! :)"
+  assertBEq (String.fromUTF8? =<< mes) (some "hi mike!! :)")
   await (client.send (String.toUTF8 "hello robert!!"))
   await (client.shutdown)
 
 /-- Joe is another client. -/
 def runJoe (client: TCP.Socket.Client) : Async Unit := do
   let mes ← await (client.recv? 1024)
-  assert! String.fromUTF8! <$> mes == some "hi joe! :)"
+  assertBEq (String.fromUTF8? =<< mes) (some "hi joe! :)")
   await (client.send (String.toUTF8 "hello robert!"))
   await client.shutdown
 
@@ -50,11 +54,11 @@ def runRobert (server: TCP.Socket.Server) : Async Unit := do
 
   await (joe.send (String.toUTF8 "hi joe! :)"))
   let mes ← await (joe.recv? 1024)
-  assert! String.fromUTF8! <$> mes == some "hello robert!"
+  assertBEq (String.fromUTF8? =<< mes) (some "hello robert!")
 
   await (mike.send (String.toUTF8 "hi mike!! :)"))
   let mes ← await (mike.recv? 1024)
-  assert! String.fromUTF8! <$> mes == some "hello robert!!"
+  assertBEq (String.fromUTF8? =<< mes) (some "hello robert!!")
 
   pure ()
 
@@ -63,13 +67,17 @@ def clientServer (addr : SocketAddress) : IO Unit := do
   server.bind addr
   server.listen 128
 
-  assert! (← server.getSockName).port == addr.port
+  let serverTask := runRobert server
+
+  let serverTask ← serverTask.run
+
+  assertBEq (← server.getSockName).port addr.port
 
   let joe ← TCP.Socket.Client.mk
   let task ← joe.connect addr
   task.block
 
-  assert! (← joe.getPeerName).port == addr.port
+  assertBEq (← joe.getPeerName).port addr.port
 
   joe.noDelay
 
@@ -77,15 +85,19 @@ def clientServer (addr : SocketAddress) : IO Unit := do
   let task ← mike.connect addr
   task.block
 
-  assert! (← mike.getPeerName).port == addr.port
+  assertBEq (← mike.getPeerName).port addr.port
 
   mike.noDelay
 
-  let serverTask ← (runRobert server).run
+  let joeTask := runJoe joe
+  let mikeTask := runMike mike
+
+  let joeTask ← joeTask.run
+  let mikeTask ← mikeTask.run
 
-  discard <| (runJoe joe).run
-  discard <| (runMike mike).run
   serverTask.block
+  joeTask.block
+  mikeTask.block
 
-#eval clientServer (SocketAddressV4.mk (.ofParts 127 0 0 1) 9000)
+#eval clientServer (SocketAddressV4.mk (.ofParts 127 0 0 1) 8084)
 #eval clientServer (SocketAddressV6.mk (.ofParts 0 0 0 0 0 0 0 1) 9000)

tests/lean/run/async_udp_sockets.lean

@@ -6,6 +6,11 @@ open Std.Internal.IO.Async.UDP
 open Std.Internal.IO.Async
 open Std.Net
 
+def assertBEq [BEq α] [ToString α] (actual expected : α) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError <|
+      s!"expected '{expected}', got '{actual}'"
+
 -- Define the Async monad
 structure Async (α : Type) where
   run : IO (AsyncTask α)
@@ -48,9 +53,10 @@ def acceptClose (addr : UInt16 → SocketAddress) (first second : UInt16) : IO U
   let (msg, addr) ← res.block
 
   if let some addr := addr then
-    assert! addr.port == second
+    assertBEq addr.port second
 
-  assert! ("hello robert!" == String.fromUTF8! msg)
+  assertBEq (String.fromUTF8! msg) "hello robert!"
 
 #eval acceptClose (SocketAddress.v4 ∘ SocketAddressV4.mk (.ofParts 127 0 0 1))  9001 9002
+
 #eval acceptClose (SocketAddress.v6 ∘ SocketAddressV6.mk (.ofParts 0 0 0 0 0 0 0 1))  9003 9004