From e17f66244a9cb681f7a2339b90e6fa1194173351 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sat, 23 May 2020 15:52:33 +0100 Subject: [PATCH] Move network support to libidris2_support This makes the support stuff much simpler, and also makes the racket bootstrap process easier --- Makefile | 12 ++--- bootstrap-rkt.sh | 6 ++- bootstrap.sh | 4 +- bootstrap/{ => idris2_app}/idris2.rkt | 0 bootstrap/idris2_app/idris2.ss | 2 +- libs/network/Echo.idr | 56 ---------------------- libs/network/Makefile | 56 ++-------------------- libs/network/Network/FFI.idr | 64 ++++++++++++------------- libs/network/Network/Socket/Data.idr | 6 +-- libs/network/expected | 2 - libs/network/test.c | 58 ---------------------- {libs/network => support/c}/idris_net.c | 0 {libs/network => support/c}/idris_net.h | 0 13 files changed, 51 insertions(+), 215 deletions(-) rename bootstrap/{ => idris2_app}/idris2.rkt (100%) delete mode 100644 libs/network/Echo.idr delete mode 100644 libs/network/expected delete mode 100644 libs/network/test.c rename {libs/network => support/c}/idris_net.c (100%) rename {libs/network => support/c}/idris_net.h (100%) diff --git a/Makefile b/Makefile index b36feb7cb..5a2260a0d 100644 --- a/Makefile +++ b/Makefile @@ -35,11 +35,11 @@ endif ifeq ($(OS), windows) IDRIS2_PREFIX := $(shell cygpath -m ${PREFIX}) IDRIS2_CURDIR := $(shell cygpath -m ${CURDIR}) - export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc;${IDRIS2_CURDIR}/libs/network/build/ttc" + export IDRIS2_BOOT_PATH = "${IDRIS2_CURDIR}/libs/prelude/build/ttc;${IDRIS2_CURDIR}/libs/base/build/ttc" else IDRIS2_PREFIX := ${PREFIX} IDRIS2_CURDIR := ${CURDIR} - export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc:${IDRIS2_CURDIR}/libs/network/build/ttc + export IDRIS2_BOOT_PATH = ${IDRIS2_CURDIR}/libs/prelude/build/ttc:${IDRIS2_CURDIR}/libs/base/build/ttc endif @@ -127,7 +127,7 @@ install-support: support install-libs: libs ${MAKE} -C libs/prelude install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} ${MAKE} -C libs/base install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} - ${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} IDRIS2_VERSION=${IDRIS2_VERSION} + ${MAKE} -C libs/network install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} ${MAKE} -C libs/contrib install IDRIS2=../../${TARGET} IDRIS2_PATH=${IDRIS2_BOOT_PATH} @@ -145,11 +145,11 @@ endif bootstrap-racket: support cp support/c/${IDRIS2_SUPPORT} bootstrap/idris2_app - cp bootstrap/idris2.rkt bootstrap/idris2boot.rkt + cp bootstrap/idris2_app/idris2.rkt bootstrap/idris2_app/idris2-boot.rkt ifeq ($(OS), darwin) - sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt + sed -i '' 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt else - sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2boot.rkt + sed -i 's|__PREFIX__|${IDRIS2_CURDIR}/bootstrap|g' bootstrap/idris2_app/idris2-boot.rkt endif sh ./bootstrap-rkt.sh diff --git a/bootstrap-rkt.sh b/bootstrap-rkt.sh index a9678d2d6..0d6b968e3 100644 --- a/bootstrap-rkt.sh +++ b/bootstrap-rkt.sh @@ -4,11 +4,13 @@ cd bootstrap echo "Building idris2boot from idris2boot.rkt" -raco exe idris2boot.rkt +raco exe idris2_app/idris2-boot.rkt # Put the result in the usual place where the target goes mkdir -p ../build/exec -install idris2boot ../build/exec/idris2 +mkdir -p ../build/exec/idris2_app +install idris2-rktboot ../build/exec/idris2 +install idris2_app/* ../build/exec/idris2_app cd .. diff --git a/bootstrap.sh b/bootstrap.sh index b9d596946..6392efee1 100644 --- a/bootstrap.sh +++ b/bootstrap.sh @@ -27,13 +27,13 @@ if [ ${OS} = "windows" ]; then IDRIS2_BOOT_PATH="${IDRIS_PREFIX}/idris2-0.2.0/prelude;${IDRIS_PREFIX}/idris2-0.2.0/base;${IDRIS_PREFIX}/idris2-0.2.0/contrib;${IDRIS_PREFIX}/idris2-0.2.0/network" NEW_PREFIX=$(cygpath -m $(dirname "$DIR")) IDRIS2_NEW_PATH="${NEW_PREFIX}/libs/prelude/build/ttc;${NEW_PREFIX}/libs/base/build/ttc;${NEW_PREFIX}/libs/network/build/ttc" - IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib;${IDRIS_PREFIX}/idris2-0.2.0/network/lib" + IDRIS2_TEST_LIBS="${IDRIS_PREFIX}/idris2-0.2.0/lib" IDRIS2_TEST_DATA=${IDRIS_PREFIX}/idris2-0.2.0/support else IDRIS2_BOOT_PATH="${PREFIX}/idris2-0.2.0/prelude:${PREFIX}/idris2-0.2.0/base:${PREFIX}/idris2-0.2.0/contrib:${PREFIX}/idris2-0.2.0/network" NEWPREFIX="`dirname $DIR`" IDRIS2_NEW_PATH="${NEWPREFIX}/libs/prelude/build/ttc:${NEWPREFIX}/libs/base/build/ttc:${NEWPREFIX}/libs/network/build/ttc" - IDRIS2_TEST_LIBS="${PREFIX}/idris2-0.2.0/lib:${PREFIX}/idris2-0.2.0/network/lib" IDRIS2_TEST_DATA=${PREFIX}/idris2-0.2.0/support + IDRIS2_TEST_LIBS="${PREFIX}/idris2-0.2.0/lib" IDRIS2_TEST_DATA=${PREFIX}/idris2-0.2.0/support fi # Now rebuild everything properly diff --git a/bootstrap/idris2.rkt b/bootstrap/idris2_app/idris2.rkt similarity index 100% rename from bootstrap/idris2.rkt rename to bootstrap/idris2_app/idris2.rkt diff --git a/bootstrap/idris2_app/idris2.ss b/bootstrap/idris2_app/idris2.ss index 98cb28b9e..d36562ba2 100755 --- a/bootstrap/idris2_app/idris2.ss +++ b/bootstrap/idris2_app/idris2.ss @@ -7124,5 +7124,5 @@ (define Parser-IDEMode-Idris-ideTokens (lambda () (List-Prelude-C-43C-43 'erased (Prelude-map_Functor__List 'erased 'erased (lambda (x) (vector 0 (Lexer-Text-exact x) (lambda (eta-0) (vector 6 eta-0)))) (Parser-IDEMode-Idris-symbols)) (vector 1 (vector 0 (Lexer-Text-digits) (lambda (x) (vector 2 (Prelude-cast_Cast__String_Integer x)))) (vector 1 (vector 0 (Lexer-Text-stringLit) (lambda (x) (vector 3 (String-Utils-stripQuotes x)))) (vector 1 (vector 0 (Source-Lexer-Parser-identAllowDashes) (lambda (x) (vector 0 (vector 1 x (vector 0 ))))) (vector 1 (vector 0 (Lexer-Text-space) (lambda (eta-0) (vector 9 eta-0))) (vector 0 )))))))) (define Parser-IDEMode-Idris-ideParser (lambda (arg-0 arg-1 arg-2 arg-3) (Prelude-C-62C-62C-61_Monad__C-40EitherC-32C-36eC-41 'erased 'erased 'erased (Either-Utils-mapError 'erased 'erased 'erased (lambda (eta-0) (vector 1 eta-0)) (Parser-IDEMode-Idris-idelex arg-2)) (lambda (toks) (Prelude-C-62C-62C-61_Monad__C-40EitherC-32C-36eC-41 'erased 'erased 'erased (Either-Utils-mapError 'erased 'erased 'erased (lambda (eta-0) (Support-Parser-mapParseError eta-0)) (Core-Parser-Text-parse 'erased 'erased arg-1 arg-3 toks)) (lambda (parsed) (vector 1 (Builtin-fst 'erased 'erased parsed)))))))) (load-shared-object "libidris2_support.so") -(load-shared-object "idris_net.so") +(load-shared-object "libidris2_support.so") (PrimIO-unsafePerformIO 'erased (lambda (eta-0) (Main-main eta-0)))) diff --git a/libs/network/Echo.idr b/libs/network/Echo.idr deleted file mode 100644 index 49b71e0db..000000000 --- a/libs/network/Echo.idr +++ /dev/null @@ -1,56 +0,0 @@ -module Main - -import System -import Network.Socket -import Network.Socket.Data -import Network.Socket.Raw - -runServer : IO (Either String (Port, ThreadID)) -runServer = do - Right sock <- socket AF_INET Stream 0 - | Left fail => pure (Left $ "Failed to open socket: " ++ show fail) - res <- bind sock (Just (Hostname "localhost")) 0 - if res /= 0 - then pure (Left $ "Failed to bind socket with error: " ++ show res) - else do - port <- getSockPort sock - res <- listen sock - if res /= 0 - then pure (Left $ "Failed to listen on socket with error: " ++ show res) - else do - forked <- fork (serve port sock) - pure $ Right (port, forked) - - where - serve : Port -> Socket -> IO () - serve port sock = do - Right (s, _) <- accept sock - | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err) - Right (str, _) <- recv s 1024 - | Left err => putStrLn ("Failed to accept on socket with error: " ++ show err) - putStrLn ("Received: " ++ str) - Right n <- send s ("echo: " ++ str) - | Left err => putStrLn ("Server failed to send data with error: " ++ show err) - pure () - -runClient : Port -> IO () -runClient serverPort = do - Right sock <- socket AF_INET Stream 0 - | Left fail => putStrLn ("Failed to open socket: " ++ show fail) - res <- connect sock (Hostname "localhost") serverPort - if res /= 0 - then putStrLn ("Failed to connect client to port " ++ show serverPort ++ ": " ++ show res) - else do - Right n <- send sock ("hello world!") - | Left err => putStrLn ("Client failed to send data with error: " ++ show err) - Right (str, _) <- recv sock 1024 - | Left err => putStrLn ("Client failed to receive on socket with error: " ++ show err) - -- assuming that stdout buffers get flushed in between system calls, this is "guaranteed" - -- to be printed after the server prints its own message - putStrLn ("Received: " ++ str) - -main : IO () -main = do - Right (serverPort, tid) <- runServer - | Left err => putStrLn $ "[server] " ++ err - runClient serverPort diff --git a/libs/network/Makefile b/libs/network/Makefile index fc3fdeba6..8a41f50e9 100644 --- a/libs/network/Makefile +++ b/libs/network/Makefile @@ -1,58 +1,8 @@ -include ../../config.mk - -INSTALLDIR = ${PREFIX}/idris2-${IDRIS2_VERSION}/network/lib - -IDRIS_SRCS = Network/Socket.idr Network/Socket/Data.idr Network/Socket/Raw.idr - -TARGET = idris_net - -SRCS = idris_net.c -OBJS = $(SRCS:.c=.o) -DEPS = $(OBJS:.o=.d) - -ifeq ($(OS), windows) - LDFLAGS += -lws2_32 -endif - - -all: $(TARGET)$(SHLIB_SUFFIX) +all: ${IDRIS2} --build network.ipkg - -build: $(TARGET)$(SHLIB_SUFFIX) $(IDRIS_SRCS) - @if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi - ${IDRIS2} --build network.ipkg - -$(TARGET)$(SHLIB_SUFFIX): $(OBJS) - $(CC) -shared -o $@ $^ $(LDFLAGS) - - --include $(DEPS) - -%.d: %.c - @$(CPP) $(CFLAGS) $< -MM -MT $(@:.d=.o) >$@ - - -.PHONY: clean - -clean : - $(RM) $(OBJS) $(TARGET)$(SHLIB_SUFFIX) - $(RM) -r build - -cleandep: clean - $(RM) $(DEPS) - - -.PHONY: install - install: - @if [ -z "${IDRIS2}" ]; then echo 'variable $$IDRIS2 is not set, aborting'; exit 1; fi ${IDRIS2} --install network.ipkg - @if ! [ -d $(INSTALLDIR) ]; then mkdir -p $(INSTALLDIR); fi - install $(TARGET)$(SHLIB_SUFFIX) $(wildcard *.h) $(INSTALLDIR) - -test: build test.c - $(CC) -o network-tests -L. -I. test.c $(TARGET)$(SHLIB_SUFFIX) - LD_LIBRARY_PATH=. ./network-tests - @$(RM) ./network-tests test.o +clean: + $(RM) -r build diff --git a/libs/network/Network/FFI.idr b/libs/network/Network/FFI.idr index bfff4c87c..280c92738 100644 --- a/libs/network/Network/FFI.idr +++ b/libs/network/Network/FFI.idr @@ -7,143 +7,143 @@ import Network.Socket.Data -- From sys/socket.h -%foreign "C:close,idris_net" +%foreign "C:close,libidris2_support" export socket_close : (sockdes : SocketDescriptor) -> PrimIO Int -%foreign "C:listen,idris_net" +%foreign "C:listen,libidris2_support" export socket_listen : (sockfd : SocketDescriptor) -> (backlog : Int) -> PrimIO Int -- From idris_net.h -%foreign "C:idrnet_socket,idris_net" +%foreign "C:idrnet_socket,libidris2_support" export idrnet_socket : (domain, type, protocol : Int) -> PrimIO Int -%foreign "C:idrnet_bind,idris_net" +%foreign "C:idrnet_bind,libidris2_support" export idrnet_bind : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String) -> (port : Port) -> PrimIO Int -%foreign "C:idrnet_connect,idris_net" +%foreign "C:idrnet_connect,libidris2_support" export idrnet_connect : (sockfd : SocketDescriptor) -> (family, socket_type : Int) -> (host : String) -> (port : Port) -> PrimIO Int -%foreign "C:idrnet_sockaddr_family,idris_net" +%foreign "C:idrnet_sockaddr_family,libidris2_support" export idrnet_sockaddr_family : (sockaddr : AnyPtr) -> PrimIO Int -%foreign "C:idrnet_sockaddr_ipv4,idris_net" +%foreign "C:idrnet_sockaddr_ipv4,libidris2_support" export idrnet_sockaddr_ipv4 : (sockaddr : AnyPtr) -> PrimIO String -%foreign "C:idrnet_sockaddr_ipv4_port,idris_net" +%foreign "C:idrnet_sockaddr_ipv4_port,libidris2_support" export idrnet_sockaddr_ipv4_port : (sockaddr : AnyPtr) -> PrimIO Int -%foreign "C:idrnet_sockaddr_port,idris_net" +%foreign "C:idrnet_sockaddr_port,libidris2_support" export idrnet_sockaddr_port : (sockfd : SocketDescriptor) -> PrimIO Int -%foreign "C:idrnet_create_sockaddr,idris_net" +%foreign "C:idrnet_create_sockaddr,libidris2_support" export idrnet_create_sockaddr : PrimIO AnyPtr -%foreign "C:idrnet_accept,idris_net" +%foreign "C:idrnet_accept,libidris2_support" export idrnet_accept : (sockfd : SocketDescriptor) -> (sockaddr : AnyPtr) -> PrimIO Int -%foreign "C:idrnet_send,idris_net" +%foreign "C:idrnet_send,libidris2_support" export idrnet_send : (sockfd : SocketDescriptor) -> (dataString : String) -> PrimIO Int -%foreign "C:idrnet_send_buf,idris_net" +%foreign "C:idrnet_send_buf,libidris2_support" export idrnet_send_buf : (sockfd : SocketDescriptor) -> (dataBuffer : AnyPtr) -> (len : Int) -> PrimIO Int -%foreign "C:idrnet_recv,idris_net" +%foreign "C:idrnet_recv,libidris2_support" export idrnet_recv : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr -%foreign "C:idrnet_recv_buf,idris_net" +%foreign "C:idrnet_recv_buf,libidris2_support" export idrnet_recv_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO Int -%foreign "C:idrnet_sendto,idris_net" +%foreign "C:idrnet_sendto,libidris2_support" export idrnet_sendto : (sockfd : SocketDescriptor) -> (dataString,host : String) -> (port : Port) -> (family : Int) -> PrimIO Int -%foreign "C:idrnet_sendto_buf,idris_net" +%foreign "C:idrnet_sendto_buf,libidris2_support" export idrnet_sendto_buf : (sockfd : SocketDescriptor) -> (dataBuf : AnyPtr) -> (buf_len : Int) -> (host : String) -> (port : Port) -> (family : Int) -> PrimIO Int -%foreign "C:idrnet_recvfrom,idris_net" +%foreign "C:idrnet_recvfrom,libidris2_support" export idrnet_recvfrom : (sockfd : SocketDescriptor) -> (len : Int) -> PrimIO AnyPtr -%foreign "C:idrnet_recvfrom_buf,idris_net" +%foreign "C:idrnet_recvfrom_buf,libidris2_support" export idrnet_recvfrom_buf : (sockfd : SocketDescriptor) -> (buf : AnyPtr) -> (len : Int) -> PrimIO AnyPtr -%foreign "C:idrnet_get_recv_res,idris_net" +%foreign "C:idrnet_get_recv_res,libidris2_support" export idrnet_get_recv_res : (res_struct : AnyPtr) -> PrimIO Int -%foreign "C:idrnet_get_recv_payload,idris_net" +%foreign "C:idrnet_get_recv_payload,libidris2_support" export idrnet_get_recv_payload : (res_struct : AnyPtr) -> PrimIO String -%foreign "C:idrnet_free_recv_struct,idris_net" +%foreign "C:idrnet_free_recv_struct,libidris2_support" export idrnet_free_recv_struct : (res_struct : AnyPtr) -> PrimIO () -%foreign "C:idrnet_get_recvfrom_res,idris_net" +%foreign "C:idrnet_get_recvfrom_res,libidris2_support" export idrnet_get_recvfrom_res : (res_struct : AnyPtr) -> PrimIO Int -%foreign "C:idrnet_get_recvfrom_payload,idris_net" +%foreign "C:idrnet_get_recvfrom_payload,libidris2_support" export idrnet_get_recvfrom_payload : (res_struct : AnyPtr) -> PrimIO String -%foreign "C:idrnet_get_recvfrom_sockaddr,idris_net" +%foreign "C:idrnet_get_recvfrom_sockaddr,libidris2_support" export idrnet_get_recvfrom_sockaddr : (res_struct : AnyPtr) -> PrimIO AnyPtr -%foreign "C:idrnet_free_recvfrom_struct,idris_net" +%foreign "C:idrnet_free_recvfrom_struct,libidris2_support" export idrnet_free_recvfrom_struct : (res_struct : AnyPtr) -> PrimIO () -%foreign "C:idrnet_geteagain,idris_net" +%foreign "C:idrnet_geteagain,libidris2_support" export idrnet_geteagain : PrimIO Int -%foreign "C:idrnet_errno,idris_net" +%foreign "C:idrnet_errno,libidris2_support" export idrnet_errno : PrimIO Int -%foreign "C:idrnet_malloc,idris_net" +%foreign "C:idrnet_malloc,libidris2_support" export idrnet_malloc : (size : Int) -> PrimIO AnyPtr -%foreign "C:idrnet_free,idris_net" +%foreign "C:idrnet_free,libidris2_support" export idrnet_free : (ptr : AnyPtr) -> PrimIO () -%foreign "C:idrnet_peek,idris_net" +%foreign "C:idrnet_peek,libidris2_support" export idrnet_peek : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> PrimIO {-Unsigned-} Int -%foreign "C:idrnet_poke,idris_net" +%foreign "C:idrnet_poke,libidris2_support" export idrnet_poke : (ptr : AnyPtr) -> (offset : {-Unsigned-} Int) -> (val : Int {- should be Char? -}) -> PrimIO () diff --git a/libs/network/Network/Socket/Data.idr b/libs/network/Network/Socket/Data.idr index 939d24218..0310ce7af 100644 --- a/libs/network/Network/Socket/Data.idr +++ b/libs/network/Network/Socket/Data.idr @@ -47,7 +47,7 @@ BACKLOG : Int BACKLOG = 20 -- Repeat to avoid a dependency cycle -%foreign "C:idrnet_geteagain,idris_net" +%foreign "C:idrnet_geteagain,libidris2_support" idrnet_geteagain : PrimIO Int export @@ -60,10 +60,10 @@ EAGAIN = -- ---------------------------------------------------------------- [ Error Code ] -- repeat without export to avoid dependency cycles -%foreign "C:idrnet_errno,idris_net" +%foreign "C:idrnet_errno,libidris2_support" idrnet_errno : PrimIO Int -%foreign "C:isNull,idris_net" +%foreign "C:isNull,libidris2_support" idrnet_isNull : (ptr : AnyPtr) -> PrimIO Int diff --git a/libs/network/expected b/libs/network/expected deleted file mode 100644 index 92aad5a55..000000000 --- a/libs/network/expected +++ /dev/null @@ -1,2 +0,0 @@ -Received: hello world! -Received: echo: hello world! diff --git a/libs/network/test.c b/libs/network/test.c deleted file mode 100644 index 47906453c..000000000 --- a/libs/network/test.c +++ /dev/null @@ -1,58 +0,0 @@ -#include -#include -#ifndef _WIN32 -#include -#include -#endif - -#include "idris_net.h" - -void test_sockaddr_port_returns_random_port_when_bind_port_is_0() { - int sock = idrnet_socket(AF_INET, 1, 0); - assert(sock > 0); - - int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 0); - assert(res == 0); - - res = idrnet_sockaddr_port(sock); - assert(res > 0); - - close(sock); -} - -void test_sockaddr_port_returns_explicitly_assigned_port() { - int sock = idrnet_socket(AF_INET, 1, 0); - assert(sock > 0); - - int res = idrnet_bind(sock, AF_INET, 1, "127.0.0.1", 34567); - assert(res == 0); - - res = idrnet_sockaddr_port(sock); - assert(res == 34567); - - close(sock); -} - -void test_peek_and_poke_buffer() { - void *buf = idrnet_malloc(100); - assert(buf > 0); - - for (int i = 0; i < 100; i++) { - idrnet_poke(buf,i,7*i); - } - - for(int i = 0; i < 100; i++) { - assert (idrnet_peek(buf,i) == (0xff & 7*i)); - } - idrnet_free(buf); -} - - -int main(void) { - test_sockaddr_port_returns_explicitly_assigned_port(); - test_sockaddr_port_returns_random_port_when_bind_port_is_0(); - test_peek_and_poke_buffer(); - - printf("network library tests SUCCESS\n"); - return 0; -} diff --git a/libs/network/idris_net.c b/support/c/idris_net.c similarity index 100% rename from libs/network/idris_net.c rename to support/c/idris_net.c diff --git a/libs/network/idris_net.h b/support/c/idris_net.h similarity index 100% rename from libs/network/idris_net.h rename to support/c/idris_net.h