Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: TCP socket support using LibUV #6683

Open
wants to merge 44 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 13 commits
Commits
Show all changes
44 commits
Select commit Hold shift + click to select a range
b875f26
feat: implement the basic libuv event loop
algebraic-dev Jan 2, 2025
7528056
doc: the event loop
hargoniX Jan 2, 2025
50cc599
fix: make the cond var safe and document it
hargoniX Jan 2, 2025
cd71bf0
feat: add async timer primitives based on libuv (#6219)
algebraic-dev Jan 6, 2025
f1e506a
feat: asynchronous timer API (#6306)
hargoniX Jan 10, 2025
c18310d
feat: start of the uv tc
algebraic-dev Jan 10, 2025
5726fcd
feat: basic tcp structure
algebraic-dev Jan 10, 2025
f376f93
Merge branch 'ft-async' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Jan 10, 2025
da8919a
feat: progress on connection
algebraic-dev Jan 14, 2025
04621bb
feat: three functions
algebraic-dev Jan 14, 2025
7a1c978
merge branch 'master' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Jan 17, 2025
260d5cb
chore: remove useless comment
algebraic-dev Jan 18, 2025
8e2fe1c
chore: remove useless modifications
algebraic-dev Jan 18, 2025
9c2e66b
feat: impl all functions
algebraic-dev Jan 23, 2025
c08d70b
fix: namespace brace
algebraic-dev Jan 23, 2025
889f9cb
fix: memory leak in accept
algebraic-dev Jan 23, 2025
cc2baa4
chore: stylistic changes
algebraic-dev Jan 23, 2025
28fe474
chore: small changes
algebraic-dev Jan 23, 2025
6e6016e
chore: remove useless print
algebraic-dev Jan 23, 2025
abf70f8
chore: comments and messages
algebraic-dev Jan 28, 2025
128aec9
chore: move things around
algebraic-dev Jan 28, 2025
4ec0f5f
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Jan 29, 2025
fdd5599
fix: behavior of loop configure function
algebraic-dev Jan 29, 2025
9e39fbd
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Jan 29, 2025
989f4f6
feat: high level interface and fix some memory leaks
algebraic-dev Jan 29, 2025
21f3829
feat: opt in client accept and fix some lean_dec and lean_inc
algebraic-dev Jan 30, 2025
65e3165
feat: move namespace
algebraic-dev Jan 30, 2025
05dc16a
feat: add shutdown and warning
algebraic-dev Jan 30, 2025
cefb9f0
fix: replace new with malloc
algebraic-dev Jan 30, 2025
20f04e8
chore: remove useless file
algebraic-dev Jan 30, 2025
f2a514d
feat: add buffer_size
algebraic-dev Feb 4, 2025
67800fd
fix: bug in getsockaddr
algebraic-dev Feb 4, 2025
e52e3a2
chore: add test
algebraic-dev Feb 4, 2025
e6e3ec8
fix: parametre in the timer.lean
algebraic-dev Feb 4, 2025
400d2a2
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Feb 4, 2025
e55f9f0
refactor: use async monad, just to show the example
algebraic-dev Feb 4, 2025
cc8ae03
fix: lean_always_assert
algebraic-dev Feb 5, 2025
27a55f1
Merge branch 'libuv-move' of github.com:algebraic-dev/lean4 into tcp-…
algebraic-dev Feb 5, 2025
1a5dcde
fix: documentation and function signature
algebraic-dev Feb 7, 2025
061c218
fix: remove user io error
algebraic-dev Feb 7, 2025
2419b54
feat: improve async tcp interface
algebraic-dev Feb 7, 2025
ccdcda2
Merge branch 'master' of github.com:leanprover/lean4 into tcp-socket
algebraic-dev Feb 7, 2025
ff1921a
fix: remove Tcp.lean files that MacOS don't detect because of the cas…
algebraic-dev Feb 7, 2025
a577e78
fix: deprecation
algebraic-dev Feb 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
89 changes: 89 additions & 0 deletions src/Std/Net/Tcp.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,89 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving, Sofia Rodrigues.
-/
prelude
import Init.Data.SInt
import Std.Net.Addr
import Init.System

namespace Std
namespace Net

private opaque TcpSocketImpl : NonemptyType.{0}

/--
Represents a TCP socket.
-/
def TcpSocket : Type := TcpSocketImpl.type

instance : Nonempty TcpSocket := TcpSocketImpl.property

namespace TcpSocket

/--
Creates a new TCP socket.
-/
@[extern "lean_uv_tcp_new"]
opaque new : IO TcpSocket

/--
Connect a TCP socket to the specified address.
-/
@[extern "lean_uv_tcp_connect"]
opaque connect (socket : TcpSocket) (addr : SocketAddress) : IO (IO.Promise (Except String Unit))

/--
Send data through a TCP socket.
-/
@[extern "lean_uv_tcp_send"]
opaque send (socket : TcpSocket) (data : ByteArray) : IO (IO.Promise (Except IO.Error Unit))

/--
Receive data from a TCP socket.
-/
@[extern "lean_uv_tcp_recv"]
opaque recv (socket : TcpSocket) : IO (IO.Promise (Except IO.Error ByteArray))

/--
Bind a TCP socket to a specific address.
-/
@[extern "lean_uv_tcp_bind"]
opaque bind (socket : TcpSocket) (addr : SocketAddress) : IO Unit

/--
Start listening for incoming connections on a TCP socket.
-/
@[extern "lean_uv_tcp_listen"]
opaque listen (socket : TcpSocket) (backlog : Int32) : IO Unit

/--
Accept an incoming connection on a listening TCP socket.
-/
@[extern "lean_uv_tcp_accept"]
opaque accept (socket : TcpSocket) : IO (IO.Promise (Except IO.Error TcpSocket))

/--
Get the remote address of a connected TCP socket.
-/
@[extern "lean_uv_tcp_getpeername"]
opaque getpeername (socket : TcpSocket) : IO SockAddr

/--
Get the local address of a bound TCP socket.
-/
@[extern "lean_uv_tcp_getsockname"]
opaque getsockname (socket : TcpSocket) : IO SockAddr

/--
Enable or disable the Nagle algorithm for a TCP socket.
-/
@[extern "lean_uv_tcp_nodelay"]
opaque nodelay (socket : TcpSocket) : IO Unit

/--
Enable or disable TCP keep-alive for a socket.
-/
@[extern "lean_uv_tcp_keepalive"]
opaque keepalive (socket : TcpSocket) (enable : Int32) (delay : UInt32) : IO Unit
2 changes: 1 addition & 1 deletion src/runtime/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp uv/event_loop.cpp
uv/timer.cpp)
uv/timer.cpp uv/tcp.cpp)
add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
set_target_properties(leanrt_initial-exec PROPERTIES
ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
Expand Down
1 change: 1 addition & 0 deletions src/runtime/libuv.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ namespace lean {

extern "C" void initialize_libuv() {
initialize_libuv_timer();
initialize_libuv_tcp_socket();
initialize_libuv_loop();

lthread([]() { event_loop_run_loop(&global_ev); });
Expand Down
3 changes: 2 additions & 1 deletion src/runtime/libuv.h
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,8 @@ Author: Markus Himmel, Sofia Rodrigues
#pragma once
#include <lean/lean.h>
#include "runtime/uv/event_loop.h"
#include "runtime/uv/timer.h"
#include "runtime/uv/timer.h"
#include "runtime/uv/tcp.h"
#include "runtime/alloc.h"
#include "runtime/io.h"
#include "runtime/utf8.h"
Expand Down
16 changes: 16 additions & 0 deletions src/runtime/uv/net_addr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -28,6 +28,22 @@ void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
}
}

extern "C" void lean_socket_addr_to_sockaddr(b_obj_arg ip_addr, struct sockaddr_in* out) {
lean_object * socket_addr_obj = lean_ctor_get(ip_addr, 0);
lean_object * ip_addr_obj = lean_ctor_get(socket_addr_obj, 0);
uint16_t port_obj = lean_ctor_get_uint16(socket_addr_obj, sizeof(void*)*1);

if (lean_ptr_tag(ip_addr) == 0) {
lean_ipv4_addr_to_in_addr(ip_addr_obj, &out->sin_addr);
out->sin_family = AF_INET;
} else {
lean_ipv6_addr_to_in6_addr(ip_addr_obj, (in6_addr*)&out->sin_addr);
out->sin_family = AF_INET6;
}

out->sin_port = htons(port_obj);
}

lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
obj_res ret = alloc_array(0, 4);
uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
Expand Down
1 change: 1 addition & 0 deletions src/runtime/uv/net_addr.h
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ namespace lean {

void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
extern "C" void lean_socket_addr_to_sockaddr(b_obj_arg ip_addr, struct sockaddr_in* out);
lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);

Expand Down
Loading
Loading