Reservoir

Http.lean

A WIP implementation of HTTP protocol in Lean 4.

The Goal

The goal of this project is to provide Lean community an HTTP Client and Server implementations as well as working and sensible set of HTTP primitives.

The broader goal of Axiomed initiative is to build an ecosystem of tools in Lean 4 that software engineers need in their everyday tasks, such as HTTP libs, async frameworks, DB connectors, parsers etc.

If you think Lean 4 can shine not only as a theorem prover, but as a general purpose language - you're welcome to join the organization!

Usage

You need to have libuv and pkg-config installed.

Add Http to your lakefile.lean:

def mkArrayLit (lvl : Level) (type : Expr) (l : List Expr) : Expr :=
  let empty := Expr.app (Expr.const ``Array.empty [lvl]) type
  let push r h := mkAppN (Expr.const ``Array.push [lvl]) #[type, r, h]
  l.foldl push empty

def elabRunPkgConfig (stx : Syntax) (args : Array String) : Elab.TermElabM Expr := do
  Lean.withRef stx do
    match ← (IO.Process.output { cmd := "pkg-config", args }).toBaseIO with
    | .ok out =>
      if out.exitCode != 0 then
        throwErrorAt stx "pkg-config failed: {out.exitCode}"
      let libParts := out.stdout.splitOn
      let stringType := Expr.const ``String []
      libParts
          |>.map (mkStrLit ·.trimRight)
          |> mkArrayLit .zero stringType
          |> pure
    | .error _ =>
        throwErrorAt stx "Could not run pkg-config"

syntax:lead (name := libuvLibsElab) "libuvLibs" : term

@[term_elab libuvLibsElab]
def elabLibUVLibs : Lean.Elab.Term.TermElab := fun stx _expectedType? =>
  elabRunPkgConfig stx #["--libs", "libuv"]

@[default_target]
lean_exe «change-the-name-of-your-application-here-it-needs-the-more-link-args» where
  root := `Main
  moreLinkArgs := libuvLibs

require Http from git "https://github.com/axiomed/Http.lean.git"

Example:

import Http

open Http.Data
open Http

def onConn (conn: Connection) : IO Unit := do
  -- Using defined headers with the formats that are assigned to them.
  conn.withHeaderStd .date (← Time.DateTime.now .GMT)
  conn.withHeaderStd .contentType (Mime.mk (.standard .text) "plain" (.empty |>.insert "charset" "utf-8"))

  -- Using a raw header that can be invalid for the client.
  conn.withHeader "transfer-encoding" "chunked"

  -- Send the headers so it can determine the content-type and stuff
  conn.sendHeaders

  -- Write strings to the response
  conn.write "some message"
  conn.write " here!"

  -- Ends the request.
  conn.end

def main : IO Unit :=
  Http.IO.Server.server
    (host := "127.0.0.1")
    (port := 8081)
    (onEnd := λconn _ => onConn conn)

Acknowledgements

This library is based on work @algebraic-sofia has done for her

It will be probably moved to the Lean STD.