pgquery

libpg_query's parse tree as Lean 4, plus the C decoder that fills it — the READING side of the leangres AST split. Generated from pg_query.proto; nothing is proven about it by design.

bazel_dep(name = "pgquery", version = "17.6.0")

View source & releases on GitHub ↗

libpg_query’s parse tree, as Lean 4 — plus the C decoder that fills it.

Postgres’s own parse-node taxonomy, generated from pg_query.proto, with a hand-curated typed layer over the statement shapes that downstream folds care about.

Part of leangres.

Two AST layers, on purpose

leangres has two representations of a Postgres statement and conflating them would be a mistake.

This module is the reading side. Pg.Query.Generated mirrors libpg_query’s protobuf faithfully — complete over Postgres’s grammar, machine-generated, regenerated wholesale on a libpg_query bump. Nothing is proven about it. It exists to get real SQL into Lean.

pgast is the writing side: small, hand-curated, closed, every constructor carrying a printer and a place in an exhaustiveness lock. Deliberately not complete, because completeness would mean carrying grammar corners nobody can state a theorem about.

The bridge between them is where round-trip guarantees live — emit from the typed AST, parse with Postgres’s own parser, ingest here, compare.

Contents

Top.lean carries fields already decoded — a QualifiedName split into schema + name, rather than a raw list of proto String message bytes. That pre-decoding lives in the C tool deliberately, so the Lean side stays simple enough to reason about.

The pipeline

SQL ──sql_to_protobuf──▶ .pgpb ──pgpb_to_lean_ast --typed──▶ Lean ──▶ a fold

sql_to_protobuf comes from rules_postgres; it is the ruleset’s tool, and this module is a consumer of it. CI exercises the whole chain rather than just checking the C compiles.

Dependencies

• pgcatalog — Top.lean imports Pg.Catalog.Tables for ArgMode alone, the proc-param direction enum. That single import is why pgquery sits above pgcatalog in the graph rather than beside it.
• rules_postgres (non-dev) — the C decoder is built against libpg_query’s protobuf-c bindings and is part of this module’s surface, so the libpg_query dependency is not gated dev-only.

Lean core otherwise. No mathlib, no batteries.

Consuming it

bazel_dep(name = "pgquery", version = "17.6.0")

lean_library(
    name = "my_fold",
    srcs = ["MyFold.lean"],
    deps = ["@pgquery//lean:pgquery"],
)

Published as compiled oleans. .olean is a compacted heap image — neither Lean-version- nor architecture-portable — so pin the same toolchain (leanprover/lean4:v4.30.0-rc2) and select the artifact for your platform.

Versioning

<pg_major>.<pg_minor>.<patch>. This module mirrors pg_query.proto, and libpg_query releases are themselves keyed to a Postgres major (17-6.2.2), so the version tracks the Postgres release modelled.

⚠ A convention, not an enforced constraint. compatibility_level was the mechanism that would have made bzlmod refuse a build mixing Postgres majors, and Bazel 9 made it a no-op. See pgcatalog’s MODULE.bazel for the two candidate enforcement mechanisms, neither built yet.

Provenance

Carved from tomato-bazel/rules_postgres with git filter-repo, history preserved. Commit hashes quoted in those messages may refer to commits that were filtered out.

License

MIT.

Conformance#

Dependencies#

Depends on

Used by (1 in the registry)

Versions#

1 published version, newest first. Each resolves to an immutable, integrity-checked archive.

Changelog#

← All modules