# Base: the Provable Requirements devcontainer image.
#
# It is itself built FROM greeng340or/rust-dev-ubuntu (qrusty's previous base), then adds the full
# requirements-verification toolchain we want for hardening qrusty's docs/requirements with provreq
# (https://github.com/greeng3/provablerequirements):
# - provreq's verification engines: Kani, TLC, Prusti, Creusot (paid once in provreq's CI image,
# so we inherit them instead of source-building Prusti/Creusot here — that build is hours long)
# - Doorstop (venv, symlinked onto PATH), uv, yamllint
# - glab (GitLab CLI, v1.107.0) and gh — so `glab` survives a container rebuild without a
# separate install here; it comes baked into this base image
# - the cargo gate tools: cargo-audit, cargo-outdated, cargo-llvm-cov, taplo-cli, llvm-tools-preview
#
# `provreq engines` reports which of the engines above are present; they are exercised by
# `provreq verify` once the requirements are adopted. See .devcontainer/README.md and
# https://github.com/greeng3/provablerequirements for the full toolchain rationale.
FROM ghcr.io/greeng3/provreq-devcontainer:latest
# --- qrusty-specific system packages the provreq base doesn't carry ---
#
# clang / libclang-dev / llvm-dev: librocksdb-sys builds its bindings against libclang.
# lsof / silversearcher-ag / ripgrep: qrusty scripts + interactive use.
# Node.js (nodesource LTS): drives node-red, the markdown linter, and the integration clients.
#
# --ignore-installed on pip3: the underlying Ubuntu ("resolute") ships python3-packaging via dpkg,
# whose dist-info has no RECORD file. When pip resolves a different `packaging` as a dependency of
# build/pdoc/twine it tries to uninstall the distro copy and fails with "uninstall-no-record-file";
# --ignore-installed skips that uninstall and installs pip's own copy instead.
RUN apt-get update && apt-get install -y \
clang \
libclang-dev \
llvm-dev \
python3 \
python3-pip \
python3-venv \
curl \
lsof \
silversearcher-ag \
ripgrep \
&& pip3 install build pdoc twine --break-system-packages --ignore-installed \
&& curl -fsSL https://deb.nodesource.com/setup_lts.x | bash - \
&& apt-get install -y nodejs \
&& apt-get clean \
&& rm -rf /var/lib/apt/lists/*
# provreq CLI + UI — the requirements-hardening tool this container is built around.
#
# We build the frontend and install FROM that source tree so provreq's `web/dist` is embedded
# (rust-embed), giving a working `provreq serve` UI *here*, where qrusty's requirements live. A
# plain `cargo install --git … provreq` compiles only the backend and skips the frontend build, so
# `serve` then reports "The provreq UI has not been built". Node (installed above) drives the Vite
# build. Pinned to tag v0.0.32 for a reproducible image (v0.0.32 adds the feature requested after !153; v0.0.31 adds leaf-crate/workspace-scoped verify so Kani can check a C-free sub-crate of an FFI-heavy subject; v0.0.29 pulls in upstream fixes; v0.0.28 lets the asserted `cargo test` verify
# route pass per-subject cargo features/args/env via a `verify.cargo` block in the companion provreq.yml
# — needed here because qrusty's integration tests require `--features test-helpers`; v0.0.27 corrects the
# stale `verify --help` text that claimed verify "runs no engine yet — always unknown"; verify actually
# runs the full engine ensemble on a grounded requirement, and an `unknown` carries its reason; v0.0.26 shipped the end-to-end
# formalization guide — `provreq guide` + a GUIDE.md — covering the grounding/fidelity process; v0.0.24 constrained
# the translate prompt to the PRL pattern grammar and v0.0.25 shipped the drafting-page PRL syntax
# reference, together fixing "Draft with a model" emitting gate-invalid PRL; v0.0.23 auto-repeats bulk
# triage until convergence. Config semantics are unchanged from v0.0.14, which unified the LLM config source so the CLI and UI
# both read the one `.provreq/system.json` on the persistent /workspace mount, not container HOME which
# a rebuild wipes; v0.0.20 brought triage + full formalization into the UI, v0.0.21 surfaced the
# provider error body on rejected requests, v0.0.22 added the Anthropic transport selector — HTTP vs
# Claude Code). RUSTFLAGS is cleared for the same crt-static reason as the dev-tool installs below (the
# base sets `-C target-feature=+crt-static`); a dev-tool binary that never ships has no reason to be
# statically linked.
ARG PROVREQ_TAG=v0.0.32
RUN git clone --depth 1 --branch "$PROVREQ_TAG" \
https://github.com/greeng3/provablerequirements /tmp/provreq-src \
&& npm --prefix /tmp/provreq-src/web ci \
&& npm --prefix /tmp/provreq-src/web run build \
&& RUSTFLAGS= cargo install --path /tmp/provreq-src --locked \
&& rm -rf /tmp/provreq-src
# (No System-config seed step: as of provreq v0.0.13 the UI bootstraps `.provreq/system.json` on the
# first "add provider", and PROVREQ_SYSTEM_CONFIG (devcontainer.json) points at /workspace/.provreq —
# the persistent workspace mount — so the config and its API keys survive a container rebuild.)
# Rust dev tools the provreq base lacks (it already carries cargo-audit, cargo-outdated,
# cargo-llvm-cov, taplo-cli, and the llvm-tools-preview component).
# - cargo-machete: `make audit-deps-unused` (unused workspace deps)
# - cargo-edit: `make upgrade-deps-rust` (provides `cargo upgrade`)
# RUSTFLAGS cleared for this step only: with the base's static CRT, these tools' openssl/link steps
# pull in symbols that aren't linked here and fail to build.
RUN export RUSTFLAGS="" \
&& cargo install cargo-machete --locked \
&& cargo install cargo-edit --locked
# Markdown linter for `make lint-md` (the provreq base installs this via its postCreate, not the
# image, so qrusty bakes it in). yamllint is already provided by the base's `uv tool install`.
RUN npm install -g markdownlint-cli2
# Python dependencies for qrusty integrations.
COPY integrations/python/requirements.txt /tmp/requirements.txt
RUN pip3 install --break-system-packages --ignore-installed -r /tmp/requirements.txt && rm /tmp/requirements.txt
# Node-RED for integration development.
RUN npm install -g node-red
# Claude Code CLI — provreq (v0.0.22+) can drive its Anthropic provider through the local `claude`
# binary (the "Claude Code" transport, vs raw HTTP), reusing this CLI's auth instead of an API key.
RUN npm install -g @anthropic-ai/claude-code