Source: docs/cookbook-unary.md · Edit on GitHub

Cookbook: typed unary RPC

Preferred app path: generate typed stubs, then register/call without hand-rolled ByteArray codecs.

Generate stubs

lake build protocGenLean4Grpc
./scripts/gen-helloworld.sh
# → Examples/Helloworld/Generated.lean

Or with a real protoc:

protoc --plugin=protoc-gen-lean4-grpc=./.lake/build/bin/protoc-gen-lean4-grpc \
  --lean4_out=. -I examples examples/helloworld.proto

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}" }, .ok)
  Grpc.Server.serveH2c s { host := "127.0.0.1", port := 50051 }

With `ServerCallContext` (mTLS peer identity / inbound metadata)

Generated stubs also emit register*WithContext:

s := helloworld.registerGreeterSayHelloWithContext s fun ctx req => do
  match ctx.peerIdentity with
  | none => pure ({ message := "" }, .unauthenticated "mtls_required")
  | some id =>
      pure ({ message := s!"Hello, {req.name} (from {id.commonName})" }, .ok)

See Cookbook: interceptors & auth for mTLS serveTls and MirrorForge.

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

Deadlines and metadata

let md := Grpc.Metadata.empty
  |> (Grpc.Metadata.add · "x-request-id" "abc")
let res ← Grpc.Channel.unary ch "helloworld.Greeter" "SayHello"
  (helloworld.HelloRequest.encode { name := "Lean" }) md (some "2S")

Timeout strings: H / M / S / m / u / n (gRPC duration grammar).