Coverage presentation nits

[System625]

What does this PR do?

Picks up three of the presentation items from the office-hours notes. One commit each.

1. Judgments defined by tests are gone

We should not include judgments defined from tests (e.g., is_zero)

10 of the 87 judgments in the report were test fixtures: is_zero, is_one and all_even from formality-core/tests/coverage.rs, sum_all and transitive_reachable from the #![cfg(test)] modules under formality-core/src/judgment/, the scraper's own inline fixtures (prove_thing, only_one, mixed), and move_place from formality-mdbook's #[cfg(test)] mod.

A file is now skipped when it lives under a tests/ directory or carries an inner #![cfg(test)], and a judgment_fn! inside an inline #[cfg(test)] mod is skipped on its own. The mdbook preprocessor builds its own index rather than calling scrape_dir, so it applies the same file-level filter.

Before	After
sidebar with the fixtures	gone

2. A judgment's page opens with its real source

(a) we presented the judgment with better indentation ... (b) we linked that
code into the source ... something like the top header just being an extract
from the source, but with the body omitted

The page used to open with a signature rebuilt from the scraped parameters, which collapsed them onto one line and left a stray comma:

borrow_check_block(env: TypeckEnv, assumptions: Wcs, state: FlowState, block: Block, places_live_on_exit: LivePlaces,) => FlowState

It now shows the real source, dedented, with the rules elided, followed by a link to the judgment on GitHub:

judgment_fn! {
    /// Prove that any loans issued in this basic block are respected.
    fn borrow_check_block(
        env: TypeckEnv,
        assumptions: Wcs,
        state: FlowState,
        block: Block,
        places_live_on_exit: LivePlaces,
    ) => FlowState {
        /* rules omitted */
    }
}

Because the text is sliced out of the source rather than rebuilt, doc comments and visibility come along, which is what you asked for.

Before	After
one-line signature	source extract

A scraper bug fixed in the same commit. The scraper read doc comments as code, which this change made impossible to ignore: judgment_fn!'s own doc example was reported as a judgment named fmt, and prove_outlives was reported as main, because the fn main() { in its doc example matched the signature regex before the real pub fn prove_outlives. That second one meant prove_outlives's recorded coverage matched no page at all. Line comments are now masked out before scanning (offsets preserved, so matches still slice out of the real source). The report drops fmt and gains prove_outlives under its real name.

the prove_outlives page, which did not exist before

This is the first of the two scraper gaps I described a thread ago; the overlap_check one (a hand-built ProofTree, not a
judgment_fn! at all) is untouched here.

3. "How to read this page"

We should figure out some way to explain what the red/green numbers mean

One standing page covering the index table, positive vs negative coverage, the ✗ / N/A / "no applicable rule observed" cells, and where a number leads. It is linked from the footer of every generated page: the index, each judgment page, each per-cell detail page, and both by-test pages. In the book it is a chapter just before the coverage index.

the explainer page

the footer link on a cell page

Heads-up for the CI coverage diff

coverage-summary.json is keyed by judgment, so the first diff after this lands will report the 10 test judgments and fmt as removed and prove_outlives as added. That is this PR, not a regression; it settles from the next build on.

Not in scope

The remaining items from the office notes (proof-tree default expansion, the issue-tracking bot, the CI-diff follow-ups) are untouched.

How does it work, what questions do you have?

The source-extract change is safe because the text is sliced out of the real source, so if the slice were wrong the rendered page would be visibly wrong, and the doc-comment mask keeps byte offsets, so a match found in the mask still points at the same place in the original.

AI disclosure

• I used an AI to author the main logic of the code

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality