diff --git a/Http.lean b/Http.lean index c2e8653..0b5a0d6 100644 --- a/Http.lean +++ b/Http.lean @@ -1,4 +1,9 @@ import Http.Data import Http.IO.Connection +import Http.IO.Server -export Http.IO.Connection (server) +namespace Http + +export Http.IO (Connection) +export Http.IO.Server (server) +export Http.Protocols.Http1.Data (Chunk Trailers) diff --git a/Http/IO/Connection.lean b/Http/IO/Connection.lean index 45d4327..bedc121 100644 --- a/Http/IO/Connection.lean +++ b/Http/IO/Connection.lean @@ -29,7 +29,7 @@ def Connection.close (connection: Connection) : IO Unit := connection.guard do UV.IO.run connection.socket.stop connection.isClosing.set true -def Connection.write [Serialize α] (connection: Connection) (data: ByteArray) : IO Unit := connection.guard do +def Connection.write [Serialize α] (connection: Connection) (data: α) : IO Unit := connection.guard do connection.buffer.modify (ToBuffer.toBuffer · data) def Connection.rawWrite (connection: Connection) (buffer: Buffer) : IO Unit := do diff --git a/lakefile.lean b/lakefile.lean index a297af8..4cfc0d6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -17,4 +17,4 @@ lean_lib Http where require alloy from git "https://github.com/tydeu/lean4-alloy.git" require LibUV from git "https://github.com/algebraic-sofia/lean-libuv.git" @ "socket-fix" -require Parse from "../lean-parse" +require Parse from git "https://github.com/axiomed/Parse.lean.git"