Reproducibility is a graph, not a lockfile

Reproducibility is often reduced to a requirements file, a notebook, and a command that runs. Those things matter. They are not the whole problem.

A research result can change while every one of those pieces still appears to be present. A table can contain a rounded literal that no longer agrees with the prose. A missing estimate can be rendered as zero. A theorem name can continue to resolve after its statement has been weakened. A PDF can depend on a package that was available on the author's machine but never entered the release archive.

The more useful question is not whether a project can be run again. It is whether a reader can see the path by which an input became a scientific claim, and whether the important edges in that path are checked automatically.

That is the design problem behind this repository. Nix pins the cross-language environment. DVC owns the data and computation graph. Semflow adds a semantic code-dependency layer without taking over that graph. Typed and named interfaces keep results addressable. Lean checks formal claims. LaTeX builds the publication artifact.

The result is not a claim that every computation is automatically correct. It is a claim that fewer important decisions are left implicit.

This note uses the public release as its evidence boundary. It treats design claims as public only when the supporting documentation ships with that release. Some architecture notes exist only to guide development and are not part of the public record. For those components, the public README and source provide the evidence. A reproducible release should promise readers a path they can inspect, not expose the contents of a private workspace.

Five layers, five jobs

The tools are easier to understand when each one has a narrow responsibility:

Table 1. The repository's reproducibility layers and their owners.

Question	Owner	What it contributes
Which tools are available?	Nix	A locked, cross-language development and CI environment.
Which scientific stages connect?	DVC	Commands, parameters, data dependencies, outputs, caching, and the DAG.
Which Python code affects a stage?	Semflow	A deterministic, conservative semantic fingerprint for the command's reachable code.
How do people invoke the system?	just	A discoverable command surface shared across the language layers.
What stops drift?	prek and the type/proof gates	Formatting, linting, static typing, tests, and machine-checked claims.

This division is intentional. just is not the scientific DAG. DVC is not the operating-system environment. Semflow is not a replacement for DVC. A reproducible repository is a composition of boundaries, not a search for one universal tool.

DVC: the scientific graph

The DVC pipeline model is close to the way a computational paper needs to be described. A stage declares a command, its dependencies, its parameters, and its outputs. Connected stages form a directed graph. DVC can then decide which stages need to run when an input or parameter changes, and it can store large outputs outside ordinary Git history while keeping their identities in versioned metadata.

That is the part of the system that make is not designed to provide.

GNU Make describes rules in terms of targets, prerequisites, and recipes. It is excellent at answering a local build question: is this target older than one of its prerequisites, and if so, which command rebuilds it? For compiled software, that simple model is often exactly right.

Scientific pipelines have additional identities. A stage may depend on a parameter nested in a large configuration file, a directory of versioned data, a matrix of model and representation choices, or an output stored in a DVC remote. It may be frozen because it is expensive or paid, even when an upstream file changes. Its outputs may be a Parquet table, a provenance manifest, a figure, and a generated manuscript value that must move together.

Modification time is not enough to express that contract. DVC's dvc.yaml and dvc.lock make the stage graph, parameters, and output identities visible to Git. The repository's root build surface therefore remains simple:

semflow check
dvc repro
pipeline-graph

The first command checks the semantic dependency proxies. The second asks DVC to reproduce the declared graph. The third renders DVC's own graph for inspection. No parallel pipeline catalogue is allowed to become a second source of truth.

Why Semflow sits beside DVC

DVC knows that a stage runs pipeline typed-distance, and it knows which files and parameters the stage declares. It does not need to understand every function reachable from that Typer callback. Tracking an entire source directory would be safe but noisy: a docstring, an unrelated function, or a type-checking-only edit could invalidate many expensive stages.

Semflow addresses that narrower problem. It resolves the installed Typer command, finds the registered callback, follows the conservative first-party static closure, canonicalizes the relevant Python AST, and writes one deterministic JSON fingerprint for that entrypoint. The generated record contains the callback, normalization policy, aggregate digest, member digests, and any fallback explanation. It contains no timestamp or host-specific value.

The important design decision is ownership. DVC still owns:

• commands and working directories;
• data dependencies and outputs;
• parameters, matrices, and foreach expansion;
• caching, frozen stages, and dvc.lock; and
• the execution graph itself.

Semflow only changes the representation of a Python code dependency. A stage can depend on a path such as:

.semflow/hashes/entrypoints/pipeline/typed-distance.json

When a reachable implementation changes, that JSON changes and DVC invalidates the stage. When an unrelated part of a shared module changes, it need not. If static analysis cannot resolve an edge safely, Semflow hashes the owning module and records why. Uncertainty therefore causes extra work rather than silent staleness.

This is also why Semflow does not use runtime tracing as its authority. A trace only sees the branches exercised by one particular dataset and run. A static closure can be conservative before the stage executes. The trade-off is that dynamic imports and dispatch remain outside the initial contract; the fallback makes that limitation visible instead of pretending it was analysed.

The workflow is review-first. semflow patch prints a diff and writes nothing. patch --apply changes the authored DVC YAML only after an explicit request. refresh --apply updates JSON fingerprints but refuses to repair stale instrumentation. The control-plane stage cannot instrument itself.

The Semflow package is therefore an adapter, not a new pipeline language. This distinction is useful beyond this repository: add a semantic layer when a workflow engine's file-level dependency model is too coarse, but do not quietly fork the engine's ownership model.

DVC, Snakemake, Make, and Docker solve different problems

The comparison with Snakemake is the most interesting one because Snakemake is also a serious workflow system. Its rules express input and output patterns, wildcards, resources, and shell commands. Its documentation also covers cluster and cloud execution, software environments, workflow reports, and benchmarking.

That does not make the choice a simple ranking. It makes the choice a question about the centre of gravity of the project.

Table 2. What the common tools make explicit.

Tool	Primary strength	What it does not replace here
Make	Small target/prerequisite build graphs.	Content-addressed data, experiment metadata, and remote artifact state.
Snakemake	Expressive rules, wildcards, resources, and scalable execution.	The repository's existing Git/DVC artifact and lockfile contract.
Docker	Portable runtime images and isolated processes.	The scientific dependency graph and data lineage.
DVC	Git-oriented data, stage, parameter, output, and experiment state.	The complete operating-system and language-toolchain closure.

Docker and DVC are particularly easy to confuse because both are described using words such as “reproducible” and “portable.” Docker packages an application and its runtime into an image and runs it as an isolated process. That is valuable for deployment and can be used underneath a workflow system. It does not, by itself, say that embeddings.parquet depends on a particular corpus, parameter, or source callback, nor does it tell a researcher which downstream figures become stale after a parameter changes.

Snakemake may be the better primary choice when cluster scheduling, heterogeneous resources, wildcard-heavy file production, or portable workflow reports are the defining requirements. DVC is a better fit for this repository's existing contract because the pipeline is already expressed in dvc.yaml, its resolved state is recorded in dvc.lock, its large artifacts belong in DVC remotes, and its publication outputs participate in the same Git/DVC path.

The comparison also clarifies the role of just. The repository uses it as a human-facing command runner, with recipes such as setup, lint, typecheck, check, and build. Its strength is discoverability and composition across Python, LaTeX, Lean, and TypeScript. It is not asked to infer data lineage. The expensive graph remains in DVC, where the graph can be inspected with dvc dag and reproduced with dvc repro.

Typing is useful when it carries meaning

Typing is often presented as a choice between developer convenience and strictness. In a scientific repository, its more important role is to make an interface carry semantic information.

The Python type checker was selected partly because it understands shape annotations such as Float[Array, "n d"]. That is not a proof that a numerical routine is correct, but it makes a dimension contract visible to the checker instead of leaving it as a comment. The TypeScript workspace applies the same boundary idea at the package level: applications own their dependencies, while Turbo hashes the task inputs that determine a generated site.

The pipeline's generated values push the idea one step further. A number in a paper is emitted as a reference, not copied as a literal:

\ppnum[3]{covariance-ceiling}

The prose and the table can therefore resolve the same catalogue entry. An undefined key raises a compile error. A missing value renders as an explicit missing marker rather than a fabricated zero. Rounding is centralized at the presentation boundary, so a call site carries a precision but not a competing rounding policy.

These are small contracts, but they address a large class of scientific errors: the computation and the explanation can drift while remaining syntactically valid.

The theorem needs an identity too

Formal verification adds a stricter version of the same problem. A manuscript can say that a result was machine-checked, but it should not need to expose Lean identifiers, source layout, or the complete toolchain to every reader.

The claim manifest is the publication bridge. A human-authored mapping connects a manuscript claim label to a fully qualified Lean declaration. The checking step confirms that the declaration exists, contains no sorryAx, and uses only the permitted axioms. More importantly, it records and hashes the elaborated theorem type. A declaration name alone is too weak: the name can remain unchanged while the proposition it denotes becomes weaker.

Verification status is generated from the checked manifest. If the proof breaks, or the statement changes, the rendered disclosure does not continue to claim that the old result was verified. The manuscript consumes an identifier-free projection, so publication prose stays readable while the repository retains a precise machine-checkable link.

This is the same principle as the value catalogue, applied to propositions: scientific objects need stable identities, and those identities need to be checked at the boundary where they are consumed.

One compiler, one publication artifact

The final output is not “the code ran.” It is a PDF, a source bundle, a figure set, and the generated values that a reader can inspect.

LaTeX is the sole canonical manuscript renderer. Tectonic builds, watches, releases, and audits the documents using a pinned content-addressable bundle. The bundle is vendored because “no network access” is weaker than “these exact bytes”: a cache-only build can still depend on a digest first accepted from an upstream server. Committing the resolved bundle makes the asset identity part of the repository.

The publication audit unpacks a venue archive into a clean directory and recompiles it. Absolute prerequisites outside the staging root are treated as unstaged inputs. Figures remain products of cached DVC stages; PGF moves only text typesetting into the manuscript compiler, so labels use the document's own font and point size. The data remains upstream of TeX: the renderer emits bindings, and TeX consumes those bindings rather than reading analysis files at compile time.

This is a deliberate rejection of two tempting shortcuts. A second release engine would provide useful publisher-parity evidence, but it would also create another artifact path, another package closure, and an audit compiled by a different engine. A general-purpose table library would reduce formatting code, but it would not preserve the manuscript's value references and missing-value semantics. The chosen design gives up convenience to keep ownership visible.

The archive is part of the method

The public source is not an accidental copy of the private workspace. The repository's git archive rules preserve paths while excluding development history, agent material, research notes, tests, and non-DVC implementation code outside the declared release closure. The release tooling checks that projection against the DVC and Semflow source closure.

That makes the archive a useful reproducibility object in its own right. A reader can distinguish between:

• the private environment used to develop the work;
• the versioned source and metadata needed to understand the computation; and
• the generated publication artifacts and their manifests.

The distinction also limits what the project should claim. A source archive can make the pipeline and publication boundary auditable without making the underlying empirical assumptions true. It cannot repair a wrong sample, identify a causal effect, or turn an unavailable external data source into a local one. Reproducibility is a condition for criticism, not a substitute for criticism.

A practical design test

When adding a new stage, model, proof, or publication target, ask five questions:

1. What is the authoritative representation?
2. Which exact inputs, parameters, and outputs define the boundary?
3. Which tool owns invalidation, and which tool merely consumes it?
4. What failure should be loud rather than silently repaired?
5. Can a clean release artifact prove what was actually used?

The answers will not always select Nix, DVC, Semflow, Lean, or LaTeX. They should, however, make it difficult for two tools to quietly own the same fact - or for no tool to own it at all.

That is why reproducibility is better understood as a graph. The graph is not only the sequence of computations. It is the set of declared identities and enforced boundaries that let a reader follow a result back to the assumptions that produced it.