# ProvSQL

[![Linux](https://github.com/PierreSenellart/provsql/actions/workflows/build_and_test.yml/badge.svg?branch=master)](https://github.com/PierreSenellart/provsql/actions/workflows/build_and_test.yml)
[![Mac OS](https://github.com/PierreSenellart/provsql/actions/workflows/macos.yml/badge.svg?branch=master)](https://github.com/PierreSenellart/provsql/actions/workflows/macos.yml)
[![Windows Subsystem for Linux](https://github.com/PierreSenellart/provsql/actions/workflows/wsl.yml/badge.svg?branch=master)](https://github.com/PierreSenellart/provsql/actions/workflows/wsl.yml)
[![Studio](https://github.com/PierreSenellart/provsql/actions/workflows/studio.yml/badge.svg?branch=master)](https://github.com/PierreSenellart/provsql/actions/workflows/studio.yml)

[![DOI](https://zenodo.org/badge/DOI/10.5281/zenodo.19512786.svg)](https://doi.org/10.5281/zenodo.19512786)
[![Archived in Software Heritage](https://archive.softwareheritage.org/badge/origin/https://github.com/PierreSenellart/provsql/)](https://archive.softwareheritage.org/browse/origin/?origin_url=https://github.com/PierreSenellart/provsql)
[![Docker Image Version](https://img.shields.io/docker/v/inriavalda/provsql?sort=semver&label=docker)](https://hub.docker.com/r/inriavalda/provsql)

ProvSQL adds (m-)semiring provenance and uncertainty management to PostgreSQL,
enabling computation of probabilities, Shapley values, and various semiring
evaluations, as a PostgreSQL extension.

Website: **<https://provsql.org/>** – Documentation: **<https://provsql.org/docs/>**

## Quick Install

**Prerequisites:** PostgreSQL ≥ 11, a C++17 compiler, PostgreSQL development
headers, `uuid-ossp`, and the Boost libraries (`libboost-dev`,
`libboost-serialization-dev`).

```sh
make
make install   # as a user with write access to the PostgreSQL directories
```

Add to `postgresql.conf` and restart PostgreSQL:

```
shared_preload_libraries = 'provsql'
```

Then in each database:

```sql
CREATE EXTENSION provsql CASCADE;
```

See the [full installation guide](https://provsql.org/docs/user/getting-provsql.html)
for prerequisites, optional dependencies, testing, and Docker instructions.

## Studio

[ProvSQL Studio](https://pypi.org/project/provsql-studio/) is a separate
Python package that adds a web UI on top of the extension: a Circuit mode
that renders the provenance DAG behind any result UUID, with frontier
expansion, an inspector, and on-the-fly semiring evaluation; and a Where
mode that hover-highlights the source cells of each output value.

```sh
pip install provsql-studio
provsql-studio --dsn postgresql://localhost/mydb
```

See the [Studio chapter](https://provsql.org/docs/user/studio.html) of the
documentation.

## Formal foundations

The theory ProvSQL implements – m-semirings and their δ operator, the
semantics of annotated databases, the query rewriting and its compositional
closure, `HAVING` provenance, provenance circuits and probabilistic
evaluation – has a machine-checked counterpart in the companion Lean 4
library [provenance-lean](https://github.com/PierreSenellart/provenance-lean),
a `sorry`-free development whose API documentation is browsable at
<https://provsql.org/lean-docs/Provenance.html>. See the
[Lean formalization](https://provsql.org/lean/) page for an overview of what
is proved.

## Authorship

ProvSQL was designed and is maintained by Pierre Senellart. Over the years it
has received contributions from students and colleagues, listed on the
[contributors](https://github.com/PierreSenellart/provsql/graphs/contributors)
page of the repository.

Since 2026, a large part of the code, tests, and documentation has been written
with the assistance of generative models from Anthropic (*Claude*); ProvSQL
Studio and the website, both of that period, were written and designed that
way. The design, the SQL interface and the semantics of what ProvSQL computes
were decided and reviewed by the maintainer, who is responsible for the whole.
The test suite run in continuous integration on Linux, macOS and WSL is used to
verify the behavior of the library; part of this behavior, the query rewriting
in particular, is also verified by the Lean formalization described above.

## License

ProvSQL is provided as open-source software under the MIT License. See [LICENSE](LICENSE).

## Contact

<https://github.com/PierreSenellart/provsql>

Pierre Senellart <pierre@senellart.com>

Bug reports and feature requests are
preferably sent through the *Issues* feature of GitHub.