web: no way to watch a run — headless is hardcoded, and on macOS/Linux nothing else drives a UI

[AminChirazi]

What happens

app: web always launches Chrome headless, and nothing can change that. crates/flowproof-adapters/src/web.rs:353:

options.headless(true).sandbox(false);

No spec field, no env var, no CLI flag is plumbed through. browser: already carries viewport, user_agent and args, but args cannot reach this — headless(true) puts --headless on the command line and Chrome's switch is presence-based, so an extra --headless=false does not undo it.

Why it matters

On macOS and Linux, web is the only adapter that drives a UI at all — the native driver is Windows-only and everything else returns UnsupportedPlatform. So for every non-Windows user, there is no way to watch flowproof do anything, ever, including once while learning what a spec means.

That has two costs:

1. Learning. A new user writing their first spec cannot see Type Ada into the name field resolve to a real element. When a step does not resolve, they debug blind against a debug/dom.html dump.
2. Demoing. Showing flowproof to someone means showing a terminal and, once run(cli): the visual report exists and the output never mentions it #286 lands, a GIF. Watching a browser get driven live is a materially stronger demonstration, and it is currently impossible on a Mac.

Neither is a correctness problem. Both are adoption friction, which CHARTER.md:193 ranks at priority 3.

Two ways to do it, and they are not equivalent

Option A — an env var (FLOWPROOF_HEADFUL=1, matching the existing FLOWPROOF_NO_SHARED_BROWSER precedent at web.rs:478).

Small, no public API surface, no trace-format change. Says the right thing semantically: whether a human is watching is a property of this invocation, not of the flow.

Option B — a browser: headless: false spec field.

More discoverable, but BrowserSetup is serialised into the trace header — deliberately, so record and every replay run the same browser shape. That makes this a trace-format change: CHARTER.md:60 requires docs/trace-format.md and crates/flowproof-trace/schema/ to move in the same commit, and CHARTER.md:8 escalates it to a human regardless.

It also encodes something questionable in the trace. Viewport belongs there because it changes what the page renders. "Was someone watching" does not, and a trace that pins headless: false would try to open a window on a headless CI runner.

Recommendation: A. B can follow if the env var proves too obscure, but starting with B means a trace-format change to express a debugging preference.

Open question for a human

Whether this is wanted at all. Headless-only is defensible — determinism is the product, and a headed mode is a debugging affordance that will be reported as a bug the first time rendering differs between the two. Labelled needs-human for that reason rather than for the trace-format angle.

Acceptance

If A: a committed flow proving the default stays headless, plus documentation in docs/authoring.md that the escape hatch is for debugging and is not part of the replay contract.