如何在精益中使用套接字？

Question

如何在 Lean 4 中创建 TCP 套接字并接受传入连接或连接到远程地址？换句话说，如何在 Lean 4 中实现 TCP 服务器或客户端？

Answer 1

您需要包装套接字类型和函数才能在 Lean 4 中使用它们。

Lean 4 仍处于早期阶段，甚至还没有稳定版本。现在用于 Lean 的软件包很少，因此您不能指望像 Pythonsocket或 Rust 的std::net/那样的生产级软件包mio。

但如果你只是想尝试一下，你可以看看我的lean4-socket包，这是一个玩具实现。文件夹中还有一些简单的示例，例如发送HTTP请求（基于TCP）examples。