diff --git a/tests/lean/run/async_tcp_fname_errors.lean b/tests/lean/run/async_tcp_fname_errors.lean index ec93efb1f5..9b345052a8 100644 --- a/tests/lean/run/async_tcp_fname_errors.lean +++ b/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 diff --git a/tests/lean/run/async_tcp_half.lean b/tests/lean/run/async_tcp_half.lean index 700713676b..ee91e825f3 100644 --- a/tests/lean/run/async_tcp_half.lean +++ b/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 diff --git a/tests/lean/run/async_tcp_server_client.lean b/tests/lean/run/async_tcp_server_client.lean index 37f8a2bb7b..c80abfbac3 100644 --- a/tests/lean/run/async_tcp_server_client.lean +++ b/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) diff --git a/tests/lean/run/async_udp_sockets.lean b/tests/lean/run/async_udp_sockets.lean index 9e316be0f9..0582f88feb 100644 --- a/tests/lean/run/async_udp_sockets.lean +++ b/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