xubaiw/Socket.lean

Lean4-Socket

A toy implementation of socket programming for Lean 4.

Installation

Lake

import Lake
open System Lake DSL

package foo where
  dependencies := #[{
    name := `socket
    src := Source.git "https://github.com/xubaiw/lean4-socket.git" "main"
  }]

Usage

This prints out yout local address.

import Socket
open Socket

def main : IO Unit := do
  let addr ← SockAddr.mk "localhost" "8080"
  IO.println addr

Documentation

The documentation generated by doc-gen4 can be found here.

There are also basic usage in the examples directory.

Limitations

Many low level flags are unavailable now.
Only blocking sockets are supported.
No dependent type and linear constraints.

Reservoir