ProvSQL Studio

ProvSQL Studio is a web UI for the ProvSQL extension. It is installed as a separate package, connects to any PostgreSQL database with ProvSQL installed, and lets you inspect provenance interactively through five complementary modes:

• Circuit mode renders the provenance directed acyclic graph (DAG) behind a result’s UUID or aggregate token, with frontier expansion, a node inspector, and on-the-fly semiring evaluation.

• Contributions mode ranks the input tuples by their Shapley value or Banzhaf power index toward a chosen result tuple, as a heat-map of signed contribution bars.

• Where mode highlights the source cells that contributed to each output value, against the live content of the provenance-tracked relations.

• Temporal mode places the rows of a relation or a query on a validity timeline, with as-of, during, and full-history time operations (requires PostgreSQL 14+).

• Notebook mode is a Jupyter-style notebook – SQL, Markdown, circuit and evaluation cells over a persistent database session – saved and loaded as standard .ipynb files.

A schema panel, a configuration panel, and a mode-switcher round out the UI; all are described below. Throughout the UI, help icons deep-link into the relevant section of this manual. Like the extension, Studio is free, open-source software distributed under the MIT License.

Tip

Try it in your browser, no install: the same Studio UI, with PostgreSQL and ProvSQL compiled to WebAssembly, runs entirely client-side as the ProvSQL Playground at provsql.org/playground/, on the tutorial and case-study databases; a first visit opens the interactive tutorial notebook. It needs a recent browser with WebAssembly JSPI; the landing page lists current browser support. Because the browser cannot launch external programs, the external knowledge compilers and model counters, as well as graph-easy for view_circuit, are not available there: probability is computed with ProvSQL’s built-in methods, and everything else works.

Studio combines well with psql: bulk fixture loads (psql -d mydb -f setup.sql) can go through psql before Studio takes over, or live in the setup cells of a notebook (see Notebook mode).

Installation

Studio targets Python ≥ 3.11. The released package is on PyPI:

pip install provsql-studio

Studio assumes the ProvSQL extension is already installed in the target database (see Getting ProvSQL) and is running at least the version listed under Compatibility.

For Studio developers, install from a local checkout in editable mode, so edits to the source take effect without reinstalling:

pip install -e ./studio

The Docker demonstration container ships a pre-installed Studio alongside the extension; see Docker Container.

Connecting

Launch Studio with a data source name (DSN):

provsql-studio --dsn postgresql://user@localhost:5432/mydb

If --dsn is omitted, Studio resolves the connection target in this order:

• The DATABASE_URL environment variable, used as a DSN.

• libpq’s standard environment variables (PGDATABASE, PGSERVICE, PGHOST…).

• Fallback to the postgres maintenance database on libpq’s default host (a local Unix socket on Linux and macOS, localhost on Windows). Studio then surfaces a banner inviting you to pick a real database from the in-page switcher.

The browser reaches the UI at http://127.0.0.1:8000/ (override the bind address and port with --host and --port).

In-page connection editor

A plug icon () next to the connection-status dot in the top navigation opens a pop-up panel where you can paste a DSN. Studio tests the new DSN before switching, so a typo or wrong password leaves the existing connection up and shows the PostgreSQL error inline. The status dot is refreshed every 5 seconds; its tooltip shows the active user@host:port endpoint.

Database switcher

Clicking the database name in the top nav lists every accessible database on the current server; pick one and the page reloads onto it. The query box is cleared on switch, but its content is pushed onto the history first, so Alt+↑ recovers it.

Two utility buttons sit nearby in the top nav: refreshes Studio’s cached metadata (schema, provenance mappings, custom semirings) after changes made outside the Studio session, and empties the connected database, dropping every user schema for a clean slate (the provsql extension survives).

Search path

Studio pins provsql at the end of search_path automatically, so the case-study idiom SET search_path TO public, provsql; is unnecessary. The header shows a lock chip for the pinned provsql; the rest of search_path is editable under the Session group of the Config panel (see Configuration).

Studio does not enforce a read-only PostgreSQL role: the query box accepts arbitrary SQL, including DDL (CREATE TABLE), DML (INSERT, UPDATE), and management helpers (add_provenance, set_prob, create_provenance_mapping). Connect Studio with a role that has the privileges your workflow expects.

Circuit mode

Circuit mode is the visual counterpart to view_circuit and the programmatic walks via get_gate_type, get_children, and identify_token. The provsql UUID column and any agg_token cells appear in the result table as raw values; clicking one renders its provenance DAG in the sidebar.

Circuit mode: a DISTINCT query renders a ⊕-rooted DAG. Pinning an input gate opens the inspector with its metadata and the stored probability.

Hovering a node lights up its subtree; clicking pins it and opens the inspector panel. Drag a node to reposition it; the offset is preserved across frontier expansions and reset on every fresh circuit load. A Reset node positions toolbar button undoes all drag-to-move offsets at once. Wheel-to-zoom is supported on the canvas (with / zoom buttons in the toolbar), and a Fit to screen button resets zoom and pan. A Fullscreen toggle pins the canvas to the browser window (Esc exits), and a Show UUIDs toggle expands the abbreviated UUIDs – in the result table, on the canvas, and in the inspector – to their full form.

Query box

The query box is a syntax-highlighted SQL editor: PostgreSQL keywords, strings, comments, and identifiers are coloured inline.

Submit the current batch with Ctrl+Enter (or ⌘+Enter on macOS) inside the query box, or by clicking the Send query button next to it. While a batch is running, Send query gives way to a Cancel button that interrupts the statement in flight. Two gutter actions on the editor clear the query box () and load a .sql file into it ().

Past queries are kept in a session history. Alt+↑ and Alt+↓ step through them in place; the History button opens a list view of recent queries to pick from.

The query box accepts multiple semicolon-separated statements, run in a single transaction. Only the last statement’s result is rendered in the result table; preceding statements are useful for setup (SET, CREATE TABLE, fixture INSERTs…) before the interesting SELECT.

The result table is capped at Result rows (default 1000 rows, tunable in Configuration). When more rows are available, the result-table footer shows a (first 1000; more available) marker.

Each column header carries the column’s SQL type name as a tooltip, and ProvSQL-significant columns get a small pill next to the column name, as in the Schema panel: terracotta rv for random_variable, terracotta agg for agg_token, and purple prov for the row-provenance provsql column itself. These are the columns that carry circuit references, and are therefore clickable in Circuit mode.

When the result is certified tuple-independent or block-independent (Studio enables provsql.classify_top_level automatically), the prov pill becomes prov-tid or prov-bid; an OPAQUE result keeps the bare prov label in a muted tone. Hovering the pill shows the certified kind’s meaning and the provenance-tracked source relations the query touches, as in the corresponding NOTICE.

Per-query toggles

A four-way Provenance scheme switch next to the query box selects the provenance class the next batch runs under:

• Semiring (default): standard provenance tracking. The resulting circuit accepts every compiled and custom semiring.

• Where: sets provsql.provenance = 'where', recording the source cell of each output value (see Where-Provenance).

• Boolean: sets provsql.provenance = 'boolean', enabling the safe-query rewriting (see Probabilities). Only Boolean-compatible semirings evaluate the resulting circuit; the eval-strip semiring picker hides the others.

• Absorptive: sets provsql.provenance = 'absorptive', allowing constructions sound only for commutative absorptive semirings, chiefly the exact reachability route over graphs of bounded treewidth (see Network reliability on bounded-treewidth graphs). Only commutative absorptive (and Boolean-compatible) semirings then evaluate the circuit; a non-commutative one, such as sr_best_path, refuses it.

The switch is free in Circuit and Notebook modes. Where mode locks it to Where; Contributions and Temporal modes lock it to Boolean.

The selected scheme persists across batches. An update_provenance (provsql.update_provenance) checkbox next to the switch carries provenance through INSERT, UPDATE, and DELETE statements (see Data Modification Tracking); it is independent of the scheme and never locked.

Worked example

Ask for the distinct cities mentioned in personnel:

SELECT DISTINCT city FROM personnel;

The result table shows one row per city with a provsql UUID column. Clicking a UUID cell renders the corresponding circuit: a single ⊕ (plus) gate over the input gates of the underlying personnel rows. Clicking a column header sorts the table by that column (ascending, then descending on the next click; numeric columns sort numerically, with blank cells sinking to the bottom). This works on every Studio table, including the knowledge-compilation benchmark.

Frontier expansion

Studio caps each circuit fetch at the value of --max-circuit-nodes (default 200, tunable in Configuration). Nodes whose children were not fetched in the current request carry a small gold + badge: clicking it fetches another breadth-first layer below that node and merges it into the current scene. The cap applies to each fetch, so a circuit grows as you expand the frontiers that interest you.

Inspector panel

Pinning a node opens the inspector. Each gate type (see Inspecting the Circuit for the catalogue) renders a gate-specific metadata block: function and result type for agg, left and right attribute for eq, value for mulinput, relation id and column list for input and update, and so on. input and update gates additionally show the stored probability, read-only. A probability is written once; to change one, give the row a fresh input gate with replace_input, as the cell’s tooltip recalls. Circuits already built over the old gate keep the old value.

Some gates carry a badge:

• B: built under the 'boolean' provenance class, or simplified under Boolean-only rules;

• A (amber): built under the 'absorptive' class (e.g., a reachability query answered by the bounded-treewidth route), or simplified under absorptive rules;

• D (green): a d-DNNF certificate, on which probability_evaluate is linear and exact; the inspector states which property is certified;

• IF (teal): an inversion-free certificate (see Probabilities); the inspector shows its variable order.

A B or A badge narrows the evaluation strip’s semiring menu to the semirings that are sound on the marked gate.

Semiring evaluation strip

Below the canvas, the semiring evaluation strip targets the pinned node (or, when no node is pinned, the root). The semiring select organises compiled entries into four sub-groups, with custom and “Other” entries below:

• Compiled semirings

  • Boolean: boolexpr, boolean.

  • Lineage: formula, how, why, which, regex (sr_regex).

  • Numeric: counting, tropical, tropical-paths (sr_tropical_paths), best-path (sr_best_path), viterbi, lukasiewicz.

  • Intervals: interval-union, i.e., sr_temporal, sr_interval_num or sr_interval_int according to the mapping’s multirange type (PostgreSQL 14+).

  • User-enum: minmax (sr_minmax) and maxmin (sr_maxmin), over any user-defined enum; subset, clearance and consent (sr_subset, sr_clearance, sr_consent), over an enum or an array of one.

• Custom semirings: any user-defined wrapper over provenance_evaluate discovered in the schema.

• Other: probability and PROV-XML export. The probability method picker (see Probabilities) starts with the three guarantees, for which ProvSQL’s cost-based chooser picks the method: exact (the cheapest exact method), relative (1±ε) and additive (±ε); the method actually used is shown next to the result. It then groups the individual methods: exact (independent, possible-worlds, sieve, d-tree, tree-decomposition, compilation), weighted model counting (wmc, with a tool picker), and approximate (monte-carlo, karp-luby, stopping-rule). Further exact methods appear only when the target’s structure admits them: inversion-free on a root carrying an inversion-free certificate, mobius on a Möbius (μ) root, and sq-rewrite, bounded-jw or reachability on a root built by the corresponding planner-time rewrite. PROV-XML export uses to_provxml; see Provenance Export.

The mapping picker lists only the mappings whose value type suits the selected semiring ((no compatible mappings : expected …) when none does). boolexpr, formula and PROV-XML export take an optional, possibly partial mapping: leaves it does not cover are identified by their gate UUID or an x<id> placeholder. tropical-paths takes two mappings: the costs in the mapping picker, and the labels the paths are written with in a second picker next to it.

Run reports the result inline along with the runtime. For an approximate method the strip also shows the (ε, δ) error bound ProvSQL reports for that run:

• a relative error bound (the estimate is within a factor 1 ± ε of the true probability) for karp-luby and the weighted counters, shown as relative error ≤ 10%, prob ≥ 95%;

• an additive bound (a Hoeffding absolute error, https://en.wikipedia.org/wiki/Hoeffding%27s_inequality) for monte-carlo, shown as ± 0.0136 absolute, prob ≥ 95%.

The sample-based methods also report the sample count, e.g., …, 2,120 samples. Clear wipes the result; Copy copies it, with full precision for a probability. Clicking a probability toggles between the rounded display (Probability decimals in Configuration) and full precision.

The same evaluation picker also exposes the knowledge-compilation pipeline as standalone entries: a Knowledge compilation group offers the DIMACS CNF (tseytin_cnf), the compiled d-D circuit (compile_to_ddnnf_dot), the same d-D in NNF text form, and the tree decomposition with its treewidth (tree_decomposition_dot); the Probability group adds a Probability benchmark that times every method (with a per-method timeout, skipping unavailable tools). Selecting one and pressing Run produces the artifact directly: the d-D circuit and the tree decomposition take over the main canvas (a toolbar back button restores the original provenance circuit), while the CNF and NNF render as text panels. The compiler picker lists only the compilers installed on the server (see tool_available). See Knowledge Compilation for the full pipeline.

Knowledge compilation in Circuit mode: the provenance circuit of a self-join, compiled to a d-DNNF by d4 (here 13 gates / 18 edges / depth 6). The canvas subtitle reports the compiled size and target language; the back arrow in the toolbar restores the original provenance circuit.

The d-DNNF and tree-decomposition canvases pin and inspect like the provenance circuit, with two refinements specific to those views:

• In the tree-decomposition canvas, pinning a bag lists its members in the inspector, each resolved to its source row.

• Pinning a bag or an internal d-DNNF gate (AND / OR / NOT) hides the evaluation strip.

When the pinned node is instead an agg_token or semimod gate over random variables, the strip offers the moment, distribution profile and sample entries (otherwise offered on random_variable leaves; see Continuous Distributions) on the aggregated value, and hides the options that do not apply to such a target.

Oversized circuits

When a top-level circuit fetch exceeds the cap, Studio shows a structured banner instead of an error: This subgraph has 4,521 nodes; the cap is 200 (rendering at depth 4) followed by a single-click Render at depth 1, then expand interactively button when the depth-1 envelope itself fits under the cap; for very wide circuits (for instance aggregations with high fan-in) the button is omitted. The eval strip (above) still works on the unrendered root.

The actionable oversize-circuit banner: when a fetch exceeds the cap, Studio surfaces a single button to start at depth 1 and expand on demand.

Distribution profile panel

For a scalar random-variable node, the eval strip offers a Distribution profile entry under the Distribution group. It shows the mean , the variance and, where entropy can compute it, the entropy in nats, with a histogram of the distribution (rv_histogram) and a PDF/CDF toggle. The sample count comes from provsql.rv_mc_samples and the seed from provsql.monte_carlo_seed (both in the Config panel).

When the node has a closed form (rv_analytical_curves), the exact PDF or CDF is drawn over the histogram, with point masses as stems: a distribution of a registered family, a constant (provsql.as_random(c)), a provsql.categorical, or a provsql.mixture of these, also under conditioning. For instance, 2 * Exp(0.4) simplifies to Exp(0.2) and gets the exact exponential curve. Other nodes show the histogram only. An infeasible conditioning event raises a “conditioning event is infeasible” error.

The Distribution profile eval-strip panel on a gate_rv N(28, 2) leaf: header stats (support, , ), an inline-SVG histogram with the analytical PDF overlaid as a smooth terracotta curve, and a PDF/CDF toggle on the right.

The same group hosts a Sample entry that draws raw samples via rv_sample; the result renders as a collapsible panel with a six-value inline preview and a “show full list” expander. When the conditioning event’s acceptance rate yields fewer samples than the requested n, the panel suggests raising provsql.rv_mc_samples.

The Moment entry on the same strip computes moment or central_moment for a chosen k (raw vs central toggle), the Quantile entry computes the inverse CDF quantile at a chosen fraction p (0.5 – the default – is the median; 0.95 a 95th percentile / VaR), and the Support entry returns the closed-form support interval.

Conditioning and the row-prov auto-preset

The eval strip carries a Condition on text input that takes any provenance UUID; when it is filled, every distribution-shaped evaluation (profile, sample, moment, quantile, support) is conditioned on it. Clicking a result-table cell presets the field to the row’s provenance UUID, with a Conditioned by: row prov badge visible underneath the input. Clicking the active badge clears the conditioning and reverts to the unconditional answer; clicking the muted badge restores the row provenance. Manual edits stick within a row and reset on row navigation.

To compare the unconditional and conditional shapes, pin the random variable, run Distribution profile, toggle the badge, and run it again. Truncated Normal, Uniform and Exponential distributions are computed in closed form; otherwise the panel shows a rejection-sampling estimate with the configured number of samples.

Simplified-circuit rendering

Circuit mode honours the provsql.simplify_on_load setting (see Configuration Reference and Continuous Distributions), rendering the simplified circuit returned by simplified_circuit_subgraph. Toggling it in the Config panel switches between the circuit as built and the simplified circuit that evaluation actually uses. In the simplified view, comparisons decidable from the support of their operands collapse to Bernoulli gate_input leaves.

Contributions mode

Contributions mode answers a different question from Circuit mode: not how a result tuple was derived, but how much each input tuple mattered to it. It is the visual counterpart of the shapley / banzhaf family (see Shapley and Banzhaf Values), showing the output of shapley_all_vars / banzhaf_all_vars as an interactive, ranked heat-map.

Queries are typed into the same Query box as in Circuit mode, with the Provenance scheme locked to Boolean (see Per-query toggles). Run a query, then click a result row’s provsql cell to pin it as the target tuple: the contribution of every input tuple toward that target is computed and drawn in the sidebar. When the result has a single UUID-typed cell, it is pinned automatically, as in Circuit mode.

Contributions mode: the pinned target token at the top, then one signed contribution bar per input, ranked by magnitude.

Each bar diverges from a central baseline (positive contributions grow right, negative ones – possible under monus-based or conditioned circuits – grow left), scaled to the largest magnitude in the set, with the numeric value alongside. The value is shown to the configured number of decimals; click it to expand it to full precision and copy that value to the clipboard. The controls above the chart drive the computation:

• Measure: Shapley (averaged over input orderings) or Banzhaf (averaged over coalitions). Both are computed in the expected probabilistic sense, so the Shapley values of all inputs sum to the target’s marginal probability.

• Method: how each value is computed. auto picks the cheapest of interpret-as-dd / tree-decomposition / compilation by estimated cost; the named methods force one. compilation runs the external d-DNNF compiler chosen in the adjacent Compiler picker.

• Compiler: shown only for the compilation method, it lists the external d-DNNF compilers the server can reach (the same tool registry Probability evaluate draws on). In the Playground, where no compiler is bundled, the list is empty.

• Labels: the provenance mapping whose value column names the inputs (the ON provenance = variable join). With source row selected instead, each input is resolved to its full tracked row (in table-column order) via resolve_input; the bar shows the values and its tooltip names every column.

The Show full UUIDs toggle expands every abbreviated UUID (the target line, the result cells, and any unresolved input labels) to its full form, as in Circuit mode. The time taken by each computation is reported next to the target token, so the methods can be compared.

Changing any control re-computes for the pinned target. A wide input relation can mint thousands of variables; the chart shows the top 200 by magnitude and reports the total when it truncates.

Where mode

Where mode is the visual counterpart to where_provenance (see Where-Provenance). Queries are typed into the same Query box as in Circuit mode, with provsql.provenance = 'where' set automatically; no explicit where_provenance call is required. Hovering a result cell highlights the source cells (in the sidebar) that contributed to it.

Where mode: source relations on the right; hovering a cell highlights the personnel rows that produced it.

The sidebar lists every provenance-tracked relation. Each panel header reports its row count, e.g., personnel – 100 of ~50000 tuples when a relation exceeds the per-relation cap (default 100 rows, tunable in Configuration). The Input gates only toggle (default on) hides relations whose first provsql token is a derived gate, such as materialised query results, keeping only relations whose tokens are input gates.

Each result row gets a Circuit button that switches to Circuit mode and pre-loads the provenance DAG of that row’s token, and a Contributions button that switches to Contributions mode and pins the same token; see Mode-switching.

Worked example

Ask for the people listed in Paris:

SELECT * FROM personnel WHERE city = 'Paris';

Each output cell becomes hover-aware: hovering name, classification, or city lights up the matching cells in the personnel panel of the sidebar.

Wrap-fallback notice

If a Where-mode query touches no provenance-tracked relation, it runs as ordinary SQL and Studio shows an INFO banner instead of an error, so setup statements run normally.

Temporal mode

Temporal mode places the rows of a relation or a query on a validity timeline, from the validity ProvSQL tracks for each token (see Temporal Features). It requires PostgreSQL 14+.

Temporal mode: a During window over cs4_holds; the in-window portion of each term is drawn at full strength, the rest dimmed.

Two orthogonal controls drive the view:

• Source – either a Relation (a provenance-tracked table or a temporal view) or a Query (arbitrary SQL, typed into the same Query box).

• Time operation – As of (an instant), During (a window), or Full (every row, with its full validity).

For a Query source the Provenance scheme switch is locked to Boolean, as in Contributions mode.

For both sources, validity is computed with sr_temporal over a validity mapping, and the time operation filters rows as timeslice / timetravel do. A validity mapping is a (provenance, value <multirange>) relation, such as one made by create_provenance_mapping (maintained => true); the Validity mapping picker lists every such relation, with the canonical provsql.time_validity_view (the union ProvSQL maintains) first. The Relation source defaults to that canonical mapping; the Query source, whose SQL is arbitrary, requires an explicit choice.

Reading the timeline

Each result row gets one lane, and every disjoint sub-range of its validity is drawn as a bar. The time axis adapts its granularity to the span – seconds, minutes, hours, days, months, or years – and a caption to the left of the axis carries the coarse component the tick labels omit (the date for a clock-time axis, the year for a day axis). Where that coarse unit rolls over mid-axis – a new day, a new year – the tick at the boundary is marked with the new date or year.

• As of adds a draggable scrubber: drag the playhead (or click the axis) to time-travel, and the lanes re-filter to the rows valid at that instant.

• During frames the window. The bars keep their full validity – the overlap filter selects rows whose validity meets the window, it does not clip them, mirroring timeslice – while everything outside [from, to) is dimmed and the window bounds are marked.

By default the lanes follow the query’s own order. The Order control re-sorts them chronologically – by start (earliest validity first) or by end – without re-running the query.

Three validity shapes get an explicit marker: an unbounded end (-∞ / ∞) runs the bar to the axis edge; a single instant infers a narrow window from the instant’s precision; and an empty union (a row valid at no time) shows a centred ∅ never. Hovering a bar reveals its precise half-open interval, e.g., [2016-01-01, 2022-01-01). All instants are rendered and parsed at UTC.

The result table on the right mirrors the timeline’s rows; the underlying SELECT (with its sr_temporal call and time filter) is available from the query box, so a timeline view can be copied out as ordinary SQL. The case study walks through the same operations on a worked dataset.

Notebook mode

Notebook mode is a Jupyter-style notebook over your ProvSQL database: an ordered list of cells – SQL, Markdown, circuit snapshots, semiring evaluations – executed against a persistent database session (the kernel) and saved as a standard .ipynb file. It suits narrated, replayable analyses: the bundled tutorial and case studies (see Example notebooks) are notebooks.

Notebook mode with the bundled tutorial open: the tab bar (one tab per notebook), the toolbar with the kernel chip, and the compact outline/relations sidebar.

Cells and the kernel

SQL cells run on the notebook’s kernel: a dedicated database session that persists across cells, so temporary tables, SET commands, and prepared statements made by one cell are visible to the next, as in Jupyter. Each cell executes in its own transaction: a failed cell rolls back (the error lands in the cell’s output) while previously committed cells persist. What the failed cell added to the provenance circuit remains, unreferenced, while a probability it wrote is cleared; see Persistence, backups and replication for how to reclaim that space. Execution counters ([1], [2]…) track what ran on the current kernel, and results render as in the query box, with provenance pills and clickable UUID cells.

The kernel starts on the first run and its chip in the toolbar shows the backend pid and database. Run runs the selected cell; Run all executes the cells top to bottom; Interrupt cancels the statement in flight; Restart kernel discards the session (temporary tables and session SET s are lost, counters reset). A kernel also ends when it has been idle for 30 minutes, when the notebook page is left, on a connection switch, or when Studio or PostgreSQL restarts. A cell sent to an ended kernel then runs on a fresh one, with a note in its output: the earlier cells’ temporary tables and session settings did not carry over, so rerun those the cell depends on.

The toolbar also appends fresh cells ( SQL / Markdown) and, as in Circuit mode, expands abbreviated UUIDs in cell results to their full form (). Each cell carries its own run button and an action row: move it up / down ( / ), delete it (), insert a SQL () or Markdown () cell below, plus the per-cell scheme chip and Circuit-mode jump described below.

Markdown cells render GitHub-flavoured Markdown; fenced code blocks tagged sql get the same syntax highlighting as the SQL editors. Double-click (or press Enter) to edit, click away (or Esc) to render.

Keyboard shortcuts

The keymap follows Jupyter’s two-mode model: command mode acts on the selected cell (highlighted border), edit mode types into it.

Key	Action
Enter / Esc	Enter / leave edit mode on the selected cell.
Ctrl+Enter	Run the cell (render, for a Markdown cell), stay on it.
Shift+Enter	Run, then select the next cell; at the last cell, create a fresh SQL cell below and edit it.
Alt+Enter	Run, then insert a fresh SQL cell below and edit it.
a / b	Insert a SQL cell above / below.
d d / z	Delete the selected cell / undo the deletion.
m / y	Convert to Markdown / back to SQL. A non-empty SQL source is wrapped in an sql-tagged code fence on the way to Markdown and unwrapped on the way back.
j / k (or arrows)	Select the next / previous cell.

Circuit and evaluation cells

Clicking a provenance UUID in a result inserts a circuit cell below the query: a snapshot of the provenance DAG behind that token, drawn as in Circuit mode, without depth control (the fetch is capped like Circuit mode’s initial render). Clicking a different UUID retargets the same cell, and re-fetches the snapshot against the live circuit; the Circuit mode button jumps to the full canvas (frontier expansion, inspector, evaluation strip) preloaded with the token.

The circuit cell offers Evaluate, which inserts an evaluation cell run against the cell’s token. For a provenance token (an event), it offers a compiled semiring or probability: the same method picker as Circuit mode’s, starting from exact, without the methods that depend on the root’s structure, with optional free-text arguments and a provenance mapping. For a random-variable or aggregate token (a value), it offers the evaluations Circuit mode offers on such a token: Distribution profile (the same histogram / PDF / CDF panel, with wheel zoom), Moment (order k, raw or central), Quantile (fraction p), Sample (n draws), and formula. Each takes an optional event to condition on, filled in with the row’s provenance when the circuit came from a result row. The invocation and its result are saved with the notebook, so a loaded notebook shows its evaluations without recomputing them.

A circuit cell (one suspect’s provenance in the tutorial) and its evaluation cell: probability/exact on the pinned token.

Provenance scheme

The toolbar’s Provenance scheme selector is the notebook’s default (the same four-way switch as the query box, see Per-query toggles); each SQL cell can override it with the small scheme chip in its actions, which cycles through the schemes, e.g., to run one recursive-CTE cell under the Boolean scheme in an otherwise standard-provenance notebook.

Tabs and database bindings

A notebook runs against a database whose state persists beyond it, so every notebook is bound to the database it was authored against (recorded in the .ipynb metadata – the name only, never credentials), and the tab bar shows one tab per open notebook, named after its first level-1 Markdown heading. Loading a notebook always opens a new tab, bound per its metadata.

When a tab’s binding differs from the live connection, a banner says so and offers three actions: switch the connection to the bound database, create it if it does not exist (to run the notebook on a fresh database), or rebind the notebook to the current database. Nothing switches silently.

The binding banner: this notebook expects cs1 but the connection is on tutorial.

Saving, loading, autosave

Save downloads the notebook as an nbformat-v4 .ipynb, directly openable in Jupyter-aware tooling. Cell outputs are included in standard formats (HTML tables, SVG circuit snapshots, plain-text evaluation results), so GitHub and nbviewer render a saved notebook as a readable static document. Load opens an .ipynb in a new tab; it also accepts a .sql file (a fixture script, a pg_dump dump…), appended to the current notebook as one ready-to-run SQL cell. Between saves, every tab autosaves to the browser’s local storage, surviving reloads and mode switches.

Example notebooks

The Open example… menu lists the bundled notebooks: this manual’s tutorial and case studies, generated from the same sources as the chapters you are reading. Each is self-establishing – it opens with idempotent setup cells (schema, data, add_provenance) – so running it top to bottom on a fresh database reproduces the whole study from one file: open the example, let the binding banner create the bound database if it does not exist yet (see Tabs and database bindings), and press Run all. The /notebook?nb=<name> deep link opens an example directly.

Notebook mode in the Playground

Notebook mode works in the Playground, with one caveat: the in-browser PostgreSQL has a single session, shared by all notebook tabs. Kernel state is therefore visible across tabs, and restarting any kernel resets them all. The binding banner’s database-creation action works there too, and ?nb=<name> deep links open the bundled examples, e.g., provsql.org/playground/?nb=tutorial.

Schema panel

A Schema button in the top nav opens a searchable pop-up panel listing every SELECT-able relation. Each gets one of two relation-level pills:

Schema panel: TID and BID sub-pills annotate each provenance-tracked relation; primary-key columns are solid-underlined and repair_key (BID) grouping keys dotted-underlined.

• prov (purple) on a provenance-tracked relation. The pill is refined by the relation’s certified kind (see Probabilities for the TID vs BID model): PROV-TID for tuple-independent tables registered via add_provenance, PROV-BID for block-independent tables registered via repair_key, and a bare prov in a muted tone for relations whose kind is opaque. This is the classification that decides whether a query is in scope for the 'boolean' provenance class.

• mapping (gold) on a relation shaped (value <T>, provenance uuid), such as one from create_provenance_mapping. A mapping that is also provenance-tracked gets only the mapping pill.

Clicking a relation row (or focusing it and pressing Enter / Space) replaces the query box with a ready-to-run SELECT * FROM <relation>;.

Columns whose values are circuit references carry their own terracotta pill next to the column name: rv for random_variable (see Continuous Distributions) and agg for agg_token.

Key columns are underlined, following the relational-schema convention: a solid underline marks a primary-key column, and a dotted underline marks a repair_key (BID) grouping key, the attribute whose value defines a block of mutually-exclusive rows (see the TID vs BID model in Probabilities).

On a tracked table, each column is a click target that prefills SELECT create_provenance_mapping('<table>_<col>_mapping', '<schema>.<table>', '<col>'); into the query box. This is not offered on rv and agg columns, whose values are circuit references and would not make meaningful labels.

On any provenance-eligible plain table, prov and prov action chips prefill SELECT add_provenance(...) / SELECT remove_provenance(...). They are hidden on views (regular and materialised) and foreign tables, which cannot take a provenance column, and on mappings.

Configuration

The Config panel shows the ProvSQL configuration parameters a user is likely to change, each documented in Configuration Reference (the beside a name links to its entry, and its tooltip gives the server’s own description). Each widget follows the parameter’s type as PostgreSQL reports it: a switch, a choice list, a number with its unit and bounds, or a text field. A value is checked by PostgreSQL itself when it is entered, and a refused one is reported on the status line. A parameter the connected role may not change (one restricted to superusers, or set in the server’s configuration) is shown greyed out with its current value. The panel’s sections are:

• Tracking: provsql.active, and provsql.implicit_freeze (whether a part of a query whose provenance is not tracked is a warning or an error).

• Limits: provsql.max_memory and provsql.max_worlds, which stop an evaluation past a memory budget or a number of possible worlds, and Query timeout, the statement_timeout Studio applies to every batch, which stops a long evaluation too.

• Evaluation: provsql.monte_carlo_seed, provsql.rv_mc_samples and provsql.simplify_on_load.

• Messages: provsql.verbose_level.

• Advanced, folded: the parameters rarely changed, which tune the evaluation routes (provsql.ess_warn_fraction, provsql.gate_cache_size, provsql.joint_max_states, provsql.joint_max_treewidth, provsql.mobius_max_cnf, provsql.mobius_max_gates) and the durability of the circuit (provsql.store_synchronous_commit, provsql.store_wal_logging).

• Session: the visible part of search_path (provsql is always pinned at the end).

• Display limits: Max circuit depth (the depth cap on the initial fetch), Nodes per fetch (the per-fetch node cap), Sidebar rows per relation (per-relation row cap in the Where-mode sidebar), Result rows (row cap on the result table), and Probability decimals (number of decimals in the eval-strip’s probability display).

The parameters of the external tools are on the Tools panel. provsql.provenance and provsql.update_provenance are set next to the query box (see Per-query toggles). Studio also sets provsql.aggtoken_text_as_uuid = on for the whole session, which makes agg_token cells clickable in the result table.

The Config panel: the ProvSQL parameters by section, the rarely changed ones folded under Advanced.

All values persist on disk in provsql-studio/config.json under the platform’s user-config directory, and survive a Studio restart:

• Linux: $XDG_CONFIG_HOME/provsql-studio/ (defaults to ~/.config/provsql-studio/).

• macOS: ~/Library/Application Support/provsql-studio/.

• Windows: %APPDATA%\provsql-studio\ (typically C:\Users\<user>\AppData\Roaming\provsql-studio\).

Each option is also exposed on the CLI as a flag (--statement-timeout, --max-sidebar-rows, --max-result-rows, --max-circuit-nodes, --max-circuit-depth, --search-path, --tool-search-path); a flag given on the command line takes precedence at startup, and panel edits are saved to config.json. The one exception is Probability decimals, which is stored in the browser, not in config.json, and has no command-line flag.

Tools panel

A tools button (the wrench-and-screwdriver icon, ) in the top nav, left of the Config cog (), opens the external-tool registry: the provsql.tools catalog the compilation and weighted-counting dropdowns draw from (see External-Tool Registry).

Tools are grouped by operation (Compilation, Weighted counting, Rendering). Each row shows a tool’s availability (a green dot when its binary and dependencies resolve on the backend’s PATH, or, for a socket server, when its endpoint is configured), its name, a cli / kcmcp badge, and its endpoint or executable.

A superuser may manage the registry in place: edit a tool’s preference (higher is selected first), toggle it on or off, edit it (the pencil reopens the form pre-filled), or unregister it (the cross). Register a tool opens the same form. The Kind determines the fields: a cli tool takes an executable and a command template; a kcmcp tool (a warm KCMCP server) takes a Connection – either Managed (ProvSQL launches and supervises it via provsql.kcmcp_server) or an Endpoint address (unix:/path or host:port). The input formats, output format, and parser are offered as the values that make sense for the chosen operation. A non-superuser session sees the panel read-only.

The Settings section at the foot of the panel holds the parameters of the external tools: provsql.tool_search_path, the directories searched for them (superuser-only: a non-superuser session sees it read-only, labelled (admin-managed), with the value an administrator set or the server’s default PATH); provsql.fallback_compiler, the d-DNNF compiler makeDD falls back to (see Knowledge Compilation), chosen among the compilers available on the server; and provsql.kcmcp_server, shown read-only, since it is set in the server’s configuration.

The Settings section of the Tools panel.

The Tools panel: the registry grouped by operation, each tool with its availability, kind, preference, enable toggle, and edit / unregister actions (here a kcmcp compile server at the top of Compilation).

Mode-switching

The mode tabs in the top nav switch between Circuit, Contributions, Temporal, Where, and Notebook. A switch carries the current SQL forward (in Notebook mode, the selected cell’s SQL); it is re-run only if you just ran it, so unrun drafts and plain reloads never execute automatically (which matters for side-effecting statements like add_provenance).

Where mode’s per-row Circuit button, and in Notebook mode the per-cell open in Circuit mode action and the circuit cells’ Circuit mode button, open Circuit mode on that token; switching back returns to the same notebook, selection and scroll position included.

Limitations

• Per-fetch circuit cap, not per-scene: --max-circuit-nodes bounds each fetch independently, so a scene assembled by repeated frontier expansions can exceed the cap.

• Verbose semiring outputs are unbounded: formula, how, why, which, and PROV-XML export can return multi-megabyte strings on large circuits. Compute time is bounded by statement_timeout; output size is not. Use Clear after a bulky run, or evaluate against a pinned subnode to scope the output.

Compatibility

Studio’s version stream is independent of the extension’s. Studio is released on PyPI as provsql-studio from studio-vX.Y.Z git tags; the extension is released on PGXN as provsql from vX.Y.Z git tags. Each Studio release lists a minimum required extension version.

Studio	ProvSQL extension	Notes
1.0.x	≥ 1.4.0	First public release.
1.1.x	≥ 1.5.0	Adds rendering of continuous-distribution circuits, the Distribution profile / Sample / Moment / Support evaluators, the Condition on row-provenance preset, and simplified-circuit rendering driven by provsql.simplify_on_load. See Continuous Distributions.
1.2.x	≥ 1.6.0	Adds the three-way Provenance scheme selector (Semiring / Where / Boolean), the B badge, the PROV-TID / PROV-BID schema-panel pills, and the eval-strip filter hiding semirings that are not Boolean-compatible on a Boolean-marked root. See Probabilities and Adding Provenance to a Table.
1.3.x	≥ 1.7.0	Adds the knowledge-compilation entries (the DIMACS CNF with its variable-to-source-tuple mapping, the compiled d-DNNF and tree-decomposition canvases, the .nnf text export, and the multi-backend Probability benchmark), the provsql.fallback_compiler row in the Config panel, the moment / distribution-profile / sample entries on agg_token and semimod targets, and tool-availability filtering of the compiler / counter pickers. See Knowledge Compilation.
1.4.x	≥ 1.8.0	Adds the Tools panel, including KCMCP servers reached by a managed or explicit endpoint (see External-Tool Registry), and the inversion-free certificate: the IF badge, its inspector details, and the inversion-free method in the eval strip and Probability benchmark. See Probabilities.
1.5.x	≥ 1.9.0	Adds Notebook mode with its example notebooks and Playground support, the action to empty the connected database, and agg_token arithmetic results rendered as value (*) like plain aggregate tokens.
1.6.x	≥ 1.10.0	Adds Contributions mode and renders 1.10.0’s new constructs: the four-way provenance-scheme selector with the A badge, the D certificate badge, conditioned gates, and Möbius (μ) nodes. Notebook Markdown cells render math.
1.7.x	≥ 1.11.0	Adds Temporal mode, which also requires the server to be PostgreSQL 14+. See Temporal Features.
1.8.x	≥ 1.12.0	Offers the sq-rewrite, bounded-jw and reachability probability methods in the eval strip, each shown only on a token produced by that route, and makes Formula available on every gate kind with an optional provenance mapping (see Probabilities and Semiring Evaluation). Random-variable families added to the extension render without a Studio upgrade (see Continuous Distributions).
1.9.x	≥ 1.13.0	Shows the reason tag of ProvSQL’s warnings and refusals as a badge and keeps their hints visible, builds the configuration panel from the server’s parameters (with the new resource limits and the provsql.implicit_freeze setting), shows input probabilities read-only since they are written once (see Persistence, backups and replication), and renders the equation-system gates of recursions over cyclic data.

When the installed extension predates this minimum, Studio’s startup check prints the mismatch and exits. Pass --ignore-version to override the check, for instance when running against a development branch.