From b5368eaa6dcb69cf56658f011618fa1ebea94142 Mon Sep 17 00:00:00 2001 From: Yernat Yestekov Date: Tue, 11 Aug 2026 19:38:43 -0700 Subject: [PATCH] docs(contributing): state the proof lane's platform and font prerequisites The `verify` gate includes the `participant-opacity-proof` lane, whose prerequisites were undocumented. The lane is Linux x86_64 only and needs bubblewrap plus a fontconfig setup with at least one font, because Isabelle starts a JVM that will not run without one. Missing fonts are the costly case: the lane reports that the Isabelle kernel rejected the fixed proof session, which reads as a failing proof rather than an incomplete environment. The tool source is digest-bound by the proof-evidence manifest, so the message itself is left alone and the prerequisite is documented where contributors run the gate. Co-Authored-By: Claude Opus 5 (1M context) --- CONTRIBUTING.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index b82ab5a00..48442ff55 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -58,6 +58,20 @@ The full repository gate is: uv tool run --from 'nox[uv]==2026.4.10' nox -f noxfile.py -s verify ``` +That gate includes a `participant-opacity-proof` lane, which replays the pinned +Isabelle proof offline. The lane runs on Linux x86_64 only. It needs +`bubblewrap` to enforce the offline replay, and a fontconfig setup with at least +one installed font, because Isabelle starts a JVM that will not run without one: + +```shell +sudo apt-get install bubblewrap fontconfig fonts-dejavu-core +``` + +Without fonts, the lane reports that the Isabelle kernel rejected the fixed +proof session, which reads as a failing proof rather than a missing +prerequisite. Run the gate on Linux, or rely on continuous integration, when +your workstation is another platform. + Run the change-aware local gate while iterating: ```shell