Source: docs/getting-started.md · Edit on GitHub

Getting started

This guide gets a Lean 4 unary gRPC server and client running on h2c with typed generated stubs, then shows TLS dial and Lake dependency usage.

Requirements: Lean 4.32+ (see lean-toolchain), OpenSSL headers for the Grpc library (libssl-dev or ./scripts/fetch-openssl-headers.sh). Peer gzip optionally uses a zlib helper (./scripts/build_native.sh) or system gzip.

Package version: 1.0.0 (lakefile.lean / Grpc.version).

Build the repo

git clone https://github.com/RileyBetts/lean-grpc.git
cd lean-grpc
lake build
lake build helloworldServer helloworldClient grpcTests
./.lake/build/bin/grpcTests

Native OpenSSL FFI object (linked by Grpc):

./scripts/build_native.sh   # also builds optional zlib_helper for peer gzip

Run helloworld (typed stubs)

./scripts/gen-helloworld.sh   # regenerates Examples/Helloworld/Generated.lean
lake build helloworldServer helloworldClient
./.lake/build/bin/helloworldServer &
./.lake/build/bin/helloworldClient 127.0.0.1 50051 World
# → Hello, World

Minimal typed server

import Grpc
import Examples.Helloworld.Generated

def main : IO Unit := do
  let mut s := Grpc.Server.empty
  s := helloworld.registerGreeterSayHello s fun req => do
    pure ({ message := s!"Hello, {req.name}" }, Grpc.Status.ok)
  Grpc.Server.serveH2c s { host := "127.0.0.1", port := 50051 }

Minimal typed client

import Grpc
import Examples.Helloworld.Generated

def main : IO Unit := do
  let ch ← Grpc.Channel.connectH2c "127.0.0.1" 50051
  let stub : helloworld.GreeterStub := { channel := ch }
  match ← stub.SayHello { name := "Lean" } with
  | .ok reply => IO.println reply.message
  | .error e => IO.eprintln e

Raw ByteArray handlers (Grpc.Server.register + manual encode/decode) remain available; prefer generated stubs for new services. See cookbook-unary.md.

Dial with TLS

let ch ← Grpc.Channel.dial "api.example.com:443" {
  channel := .tls {
    caPath := some "/etc/ssl/certs/ca-certificates.crt"
    serverName := some "api.example.com"
  }
}

mTLS: set certPath / keyPath on the client config; on the server set clientCaPath and use Grpc.Server.serveTls. Details: tls-envoy.md, cookbook-interceptors.md.

Targets and service config

-- dns:///host:port or host:port
let ch ← Grpc.Channel.dial "dns:///127.0.0.1:50051" {}
  (Grpc.ServiceConfig.parse "{\"loadBalancingPolicy\":\"round_robin\",\"timeout\":\"5s\"}")

-- xDS when LEAN_GRPC_XDS_BOOTSTRAP points at a bootstrap JSON
let ch ← Grpc.Channel.dial "xds:///my-service" {}

Override resolved addresses in tests with LEAN_GRPC_RESOLVE_ADDRS=127.0.0.1:50051,127.0.0.1:50052.

Streaming

Prefer the batch helpers, or openStream for interactive duplex:

let (msgs, st) ← Grpc.Channel.serverStream ch "svc" "ServerStream" req
let res ← Grpc.Channel.clientStream ch "svc" "ClientStream" reqs
let (echo, st) ← Grpc.Channel.bidiStream ch "svc" "Bidi" reqs

Server side:

s := Grpc.Server.registerServerStreamTyped s "svc" "ServerStream"
  Req.decode Resp.encode fun req => pure (#[resp1, resp2], Grpc.Status.ok)

Full walkthrough: cookbook-streaming.md. Example: Examples/RouteGuide/.

Metadata, deadlines, compression

let md := Grpc.Metadata.empty
  |> (Grpc.Metadata.add · "x-request-id" "abc")
  |> (Grpc.Metadata.addBin · "x-bin" (ByteArray.mk #[1, 2, 3]))
let res ← Grpc.Channel.unary ch "svc" "Method" req md (some "2S") .gzip

Timeout strings follow gRPC (H/M/S/m/u/n). Compression algorithms: identity, gzip, deflate, snappy (negotiate prefers gzip).

Codegen

Descriptor path (typed messages + stubs — preferred):

./scripts/gen-helloworld.sh
# or: ./scripts/run-codegen-fixture.sh

Text path (Lake smoke; ByteArray placeholders only):

LEAN_GRPC_OUT=/tmp/gen LEAN_GRPC_PROTO=Examples/helloworld.proto \
  ./.lake/build/bin/protoc-gen-lean4-grpc

Real protoc plugin:

lake build protocGenLean4Grpc
protoc --plugin=protoc-gen-lean4-grpc=./.lake/build/bin/protoc-gen-lean4-grpc \
  --lean4_out=. your.proto

Current descriptor-codegen limits: nested messages / repeated / oneof / maps are incomplete — RouteGuide still uses hand-written Proto.RouteGuide codecs. See api-reference.md.

Depend from another Lake project

System deps: OpenSSL (libssl-dev / Homebrew openssl, plus pkg-config). Fallback: ./scripts/fetch-openssl-headers.sh.

In your lakefile.lean:

require «lean-grpc» from git
  "https://github.com/RileyBetts/lean-grpc.git" @ "v1.0.0"

Then import Grpc (and Proto if you use the bundled codecs). Public libs: Bytes, Hpack, H2, Proto, Grpc. Linking OpenSSL (-lssl -lcrypto) is pulled in via the Grpc Lake library (not via Bytes/Hpack/H2 alone). For peer gzip against foreign stacks, set LEAN_GRPC_ZLIB_HELPER after ./scripts/build_native.sh. Full packaging notes: packaging.md. Hosted docs: rileybetts.ai/oss/lean-grpc.

After Reservoir indexes the package you can use require «lean-grpc» without a git URL. Pin a commit SHA if the v1.0.0 tag is not yet on the remote you use.

Next steps

Source: docs/getting-started.md in RileyBetts/lean-grpc. Hosted docs may lag the repository slightly.