Cargo.toml

# Unless explicitly stated otherwise all files in this repository are licensed under the
# Apache License Version 2.0.
# This product includes software developed at Datadog (https://www.datadoghq.com/).
# Copyright 2026-Present Datadog, Inc.

[workspace]
members = ["sqleq-check", "sqleq-fuzz", "sqleq-lean", "sqleq-solver"]
# Bare `cargo build` / `cargo test` stay on the light crates: the frontend, and sqleq-check, the
# batch harness, which runs every other crate's binary as a subprocess and so builds none of them.
# sqleq-fuzz links DuckDB, whose release library its first build downloads, so it is opt-in:
# `cargo build -p sqleq-fuzz`.
# sqleq-lean needs a Lean toolchain at run time, so it is opt-in too: `cargo build -p sqleq-lean`.
# sqleq-solver compiles Z3 from source on its first build, so it is opt-in the same way:
# `cargo build -p sqleq-solver`.
default-members = [".", "sqleq-check"]
resolver = "2"

# Shared versions, so the two crates cannot drift apart on the parser.
[workspace.dependencies]
serde_json = "1"

# `visitor` gives us the derived AST walker. It is used for the "is this expression closed?"
# guards, where a hand-written match risks *missing* a variant — and a missed variant there is a
# soundness hole, not a coverage gap.
sqlparser = { version = "0.63", features = ["visitor"] }
# Robust CSV reader for the corpus: the DDL field holds quoted, multi-line SQL.
csv = "1"

[package]
name = "sqleq-frontend"
version = "0.1.0"
edition = "2021"
rust-version = "1.88"
description = "Analyze SQL equivalence pairs and lower them to prover IR (QED, SQLSolver)"
license = "Apache-2.0"
publish = false

[lib]
name = "sqleq_frontend"
path = "src/lib.rs"

[[bin]]
name = "sqleq-frontend"
path = "src/main.rs"

# Off by default. Exposes lowering internals to sqleq's own benchmark harness, which audits a
# corpus that cannot be published and so cannot live in this repository. Exempt from semver.
[features]
internals = []

[dependencies]
serde_json = { workspace = true }
sqlparser = { workspace = true }
csv = { workspace = true }
# Postgres's own grammar (libpg_query, compiled from the Postgres source it vendors). It decides
# whether a refusal is `parse`: text Postgres cannot parse, as opposed to Postgres syntax this
# frontend's parser does not read. See `FrontendError::Parse`.
pg_query = "6.2"

# Profiles are workspace-wide and may only be set at the root (moved here from sqleq-fuzz).
[profile.release]
opt-level = 3

# z3-sys's build script compiles Z3 through the `cmake` crate, which takes the CMake build type from
# this package's profile, and opt-level 0 means `Debug`: an unoptimised Z3 with its internal
# assertions and tracing compiled in, which creates `.z3-trace` in the working directory of every
# run. Dev builds, `cargo test` and CI included, get the same `Release` Z3 as a release build.
[profile.dev.package.z3-sys]
opt-level = 3
debug = false

# sqlparser 0.63.0 plus the two PostgreSQL INSERT clauses it cannot parse yet: `OVERRIDING
# { SYSTEM | USER } VALUE` and the `ON CONFLICT` target's `WHERE index_predicate`
# (apache/datafusion-sqlparser-rs#2626, #2627). Drop this, and bump the version, once a release
# carries both.
[patch.crates-io]
sqlparser = { git = "https://github.com/zvonimir-dd/datafusion-sqlparser-rs", rev = "23962bd728db232b2408f1180882fbe9fa3b270e" }