docs(contributing): state the proof lane's platform and font prerequisites

[doublewhy]

Plain-language summary

• Context: OpenRAE includes an offline Isabelle proof lane whose sandbox has operating-system and font prerequisites.
• Problem: Contributors could enter the proof lane without those prerequisites and receive setup failures that looked like proof failures.
• Fix: Document the supported platform, sandbox tools, font requirements, and acquisition step before the proof is run.

Related issues

Closes #1118

Proof-tool preflight and Ubuntu sandbox portability remain tracked in #1109.

---

What breaks

A new contributor runs the documented full gate, nox -s verify, on a clean Linux machine and is told their proof failed:

IsabelleToolError: Isabelle kernel rejected the fixed proof session

Nothing is wrong with the proof. The machine is missing fonts.

Why that message appears

The participant-opacity-proof lane replays the pinned Isabelle proof. Isabelle starts a JVM, and that JVM will not run without a fontconfig setup, so it aborts with a non-zero exit. The lane reports any non-zero exit as the kernel rejecting the theory — which reads as "your mathematics is broken" rather than "install a font".

The sandbox already bind-mounts /etc/fonts, /usr/share/fonts and /var/cache/fontconfig, but only if runtime_path.exists(), so on a host without them the sandbox is silently font-less.

CONTRIBUTING.md lists Python, uv and nox as prerequisites, and does not mention that this lane is Linux x86_64 only or that it needs bubblewrap and fonts.

Concretely

On a stock Ubuntu 22.04 image this cost me a full debugging cycle before the real cause surfaced further up the output:

*** Fontconfig head is null, check your fonts or fonts configuration

It reproduces on an unmodified dev checkout, so it is not specific to any change, and clears completely with:

sudo apt-get install fontconfig fonts-dejavu-core

The fix

Document the prerequisite where contributors run the gate, including the misleading message, so the next person recognises it immediately.

Why documentation instead of a better error message

The better fix is obviously in the tool: preflight for fonts, or classify that failure as an environment problem rather than a rejected proof. I wrote that version first and it worked — then it broke two manifest tests.

tools/isabelle_tool.py is digest-bound. tools/check_participant_opacity_proof.py validates its SHA-256 against participant-opacity-proof-evidence.json as the "proof tool source", precisely so nobody can quietly alter the tool that certifies the proof. Editing it invalidates that attestation until the evidence is regenerated.

Re-attesting the proof-checking tool to improve an error message is not a trade I should make unilaterally, so I reverted the code and documented the prerequisite instead. If you would rather re-attest, say so and I will land the preflight and classifier — they are straightforward, and I have the tests.

Documentation only. Vale clean (the style rule caps sentences at 32 words), public-docs boundary check passes.

🤖 Generated with Claude Code

[Brad-Edwards]

Please note in the comments or body which issue this PR closes. If no issue exists, please create one and link it.

Thank you!

[doublewhy]

Linked the documentation issue in the PR body: this PR closes #1118. The proof-tool portability follow-up remains tracked in #1109. Thank you.

[doublewhy]

Superseded by #1131, which is rebuilt on the current dev branch and closes both #1109 and #1118. The successor keeps the prerequisite documentation and also fixes the Ubuntu/fontconfig sandbox setup and distinguishes setup failures from Isabelle kernel failures.