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 }

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).

See also

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