Source: docs/packaging.md · Edit on GitHub

Packaging and open-source distribution

How lean-grpc is structured for Lake consumers and what maintainers do to publish.

Layout (keep the monorepo)

lean-grpc is a single Lake package. Do not split libraries into separate repos for packaging.

Path / target	Role	Consumer API?
`Bytes`, `Hpack`, `H2`, `Proto`, `Grpc`	Library stack	Yes
`LeanGrpc.lean`	Umbrella import	Yes
`Proofs`	Compile-time theorems (CI only; not consumer API)	No
`native/` + OpenSSL link args	TLS FFI (`tls_ffi.o`, `-lssl -lcrypto`)	Required for TLS / ADC
`Tests/`, `Bench/`, `Examples/`, `scripts/`, `python_interop/`, `rust_interop/`	Dev / CI / demos	No
`lakefile.lean`, `lake-manifest.json`, `lean-toolchain`	Lake package root	Required for Reservoir

lean-grpc/
  lakefile.lean
  lake-manifest.json
  lean-toolchain
  LeanGrpc.lean / Grpc.lean / H2.lean / …
  Bytes/ Hpack/ H2/ Proto/ Grpc/ Proofs/ native/
  Examples/ Tests/ Bench/ scripts/ docs/
  LICENSE README CONTRIBUTING SECURITY CHANGELOG

Registries

Channel	Use
Reservoir	Primary Lean package index (inclusion criteria)
Lake git require + tags	Immediate consume path: pin `@ "vX.Y.Z"`
npm / PyPI / Maven / crates	Not used. Optional later: GitHub Release binaries for `protoc-gen-lean4-grpc` only

License

Apache-2.0 (SPDX). Matches Lean 4, mathlib4, and typical Reservoir packages; fits a TLS/networking stack (explicit patent grant). Confirm GitHub’s license badge shows Apache-2.0 on the public repository; adjust LICENSE / NOTICE only if detection fails.

Provenance: lean-grpc is an independent implementation of the published gRPC-over-HTTP/2 protocol (not a fork of official runtimes). Peer fixtures under python_interop/proto/ and rust_interop/proto/ retain Apache-2.0 gRPC-authors headers; see NOTICE and provenance.md.

Consumer contract

Public libraries: Bytes, Hpack, H2, Proto, Grpc (umbrella LeanGrpc). Tests, examples, and Proofs are not consumer API.

System dependencies:

Platform	Packages
Debian / Ubuntu	`libssl-dev`, `pkg-config`
macOS (Homebrew)	`openssl` (or `openssl@3`), `pkg-config`
No sudo / missing headers	`./scripts/fetch-openssl-headers.sh`

Link flags come from the Grpc library (-lssl -lcrypto). The OpenSSL FFI object (tls_ffi.o) is built via Lake. Peer gzip uses process helpers (LEAN_GRPC_ZLIB_HELPER after ./scripts/build_native.sh) or system gzip / a stored-deflate fallback — zlib_bridge.o is not linked into Lean. Optional: zlib1g-dev / Homebrew zlib only if you build the native zlib helper yourself.

macOS note: Lean’s linker may not find Homebrew OpenSSL unless library search paths are set:

export LIBRARY_PATH="$(brew --prefix openssl@3)/lib${LIBRARY_PATH:+:$LIBRARY_PATH}"
lake build

Depend via Lake (git tag):

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

Then import Grpc (and Proto if using bundled codecs).

Reservoir (after indexing):

require «lean-grpc»   -- once listed on reservoir.lean-lang.org

Package version in-tree is 1.0.0 (lakefile.lean, Grpc.version). Hosted docs: rileybetts.ai/oss/lean-grpc. Creating the git tag on origin is a separate maintainer step (below).

Maintainer notes

Release tagging, Reservoir crawl verification, and branching are documented in the full packaging guide on GitHub.

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