Repository navigation
docs: document offline proof lane platform and font prerequisites #1118
Description
Documentation gap
The contributor guide documents the canonical verification command but not that the participant-opacity proof lane requires Linux x86_64, Bubblewrap, fontconfig, and an installed font. On a clean Linux host, a missing runtime prerequisite can therefore be mistaken for a rejected theorem.
Expected documentation
- State the supported proof-runner platform.
- List Bubblewrap, fontconfig, and a minimal font package.
- Explain that restrictive namespace policy produces a sandbox-unavailable result and must not be bypassed by weakening offline isolation.
- Direct non-Linux contributors to canonical CI.
Scope
This issue covers contributor documentation only. Proof-tool preflight and Ubuntu sandbox portability remain tracked in #1109.
Related implementation
Proposed in #1088.
Activity
docs(contributing): state proof runtime prerequisites (#1118, #1109)
docs(contributing): state proof runtime prerequisites (#1118, #1109)
fix(proof): make offline Isabelle replay portable on Ubuntu (#1131)
doublewhy commentedon Aug 13, 2026
Completed by #1131, squash-merged to
devas990e8fbc246769fd95f4100e225a2eb69e2812f3. The merged documentation records the offline proof platform, font, sandbox, and replay prerequisites; exact-head docs, verification, and Sonar passed. Closing manually because merges to non-defaultdevdo not trigger GitHub closing keywords.