Repository navigation
Add a recovery trace viewer, published with the docs - #8496
Open
Amaury Chamayou (achamayou) wants to merge 6 commits into
Open
Amaury Chamayou (achamayou) wants to merge 6 commits into
Amaury Chamayou (achamayou) wants to merge 6 commits into
Conversation
Amaury Chamayou (achamayou)
added this pull request to stack #8367
October 2, 2026 14:34
Max (maxtropets)
approved these changes
Oct 2, 2026
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 2, 2026 14:54
301cc98 to
4414f2a
Compare
Copilot started reviewing on behalf of
Amaury Chamayou (achamayou)
October 2, 2026 15:04
View session
Contributor
There was a problem hiding this comment.
Copilot review overview
🟡 Changes recommended
Run-ID collisions, broken first-step links, misleading preflight failures, and inaccessible controls affect core viewer behavior.
Review effort: Balanced
Findings: 4
Open (5)
What changed in this PR
Adds a documentation-published recovery trace viewer without changing CCF runtime behavior.
Changes:
- Adds Lean JSON replay dumps and diagnostics.
- Adds a static trace viewer and mutant fixture generation.
- Integrates viewer generation into documentation and CI workflows.
Custom instructions used
.github/copilot-instructions.md.github/instructions/changelog.instructions.md.github/skills/testing/SKILL.md.github/skills/formatting-and-linting/SKILL.md
| File | Description |
|---|---|
tests/infra/recovery_trace_mutations.py |
Adds the disabled-retry mutant. |
lean/disaster-recovery/replay/viewer/viewer.js |
Implements trace visualization and interaction. |
lean/disaster-recovery/replay/viewer/index.html |
Defines the viewer UI and styling. |
lean/disaster-recovery/replay/viewer/build.py |
Generates fixture and mutant dumps. |
lean/disaster-recovery/replay/viewer/.gitignore |
Excludes generated viewer data. |
lean/disaster-recovery/replay/ReplayMain.lean |
Adds the --dump option. |
lean/disaster-recovery/replay/README.md |
Documents dump generation and viewing. |
lean/disaster-recovery/DisasterRecovery/Replay/Dump.lean |
Serializes replay states and diagnostics. |
lean/disaster-recovery/DisasterRecovery/Replay.lean |
Exposes single-instruction replay. |
lean/disaster-recovery/DisasterRecovery.lean |
Exports the dump module. |
doc/operations/recovery.rst |
Documents trace collection and viewing. |
doc/contribute/build_ccf.rst |
Documents viewer build requirements. |
doc/conf.py |
Builds and publishes the viewer. |
CMakeLists.txt |
Skips viewer generation in docs tests. |
.github/workflows/lean.yml |
Validates viewer dump generation. |
.github/workflows/doc.yml |
Installs Lean for documentation builds. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 05:44
277cede to
b29a7c8
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 13:35
b29a7c8 to
768a908
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
2 times, most recently
from
October 6, 2026 15:20
97b44d2 to
4f3ce4b
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 15:45
4f3ce4b to
633749c
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 16:13
633749c to
72a8c3d
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 16:39
72a8c3d to
019696c
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 6, 2026 17:04
019696c to
2534467
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
4 times, most recently
from
October 7, 2026 10:14
ef98ac9 to
ad2e1cb
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
8 times, most recently
from
October 9, 2026 14:36
69ec00a to
5bdc891
Compare
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
2 times, most recently
from
October 9, 2026 16:59
d79b071 to
7e21e6f
Compare
disaster-recovery-replay --dump FILE writes a run as JSON: its records, the reduced instructions, and the model state after each step with the actions it enables. It also holds the queued copy that each delivery took, and each check's result, with each field's observed and model values when one fails. It replays through the same runInstruction and replay as the check, so the dump shows exactly what the replayer concludes. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
replayer/viewer/ is a static page that steps through a run written by disaster-recovery-replay --dump. It shows the trace records beside the model state of every node and the network, what changed at each step, which send each receive took, and where and why a replay stopped. It only renders dumps: every semantic fact comes from the replayer. build.py dumps the recorded traces in the replay fixtures, one stored invalid trace for each way a replay can stop, which it applies as check-fixtures.sh does, and any --logs DIR of node logs into viewer/data/. The quorum and multiple-timeout fixtures gain an invalid trace, commit-order.retry_after_end, the first that stops at a disabled action. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The recovery documentation says how to view your own traces. Like doxygen, doc/conf.py builds the replayer and the viewer's runs into the site as trace-viewer/ unless SKIP_TRACE_VIEWER is set, and skips older trees without a viewer. doc.yml installs Lean for that with the SNP job's pinned elan installer. The docs ctest sets SKIP_TRACE_VIEWER, as its runner has no Lean. The Lean workflow runs build.py, which fails if a dump is missing or its outcome disagrees with the replayer. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
A run's id names its dump in data/, so a --logs directory named like a fixture, another --logs directory or a stored trace silently replaced that run's dump, and index.json listed the id twice. build.py now exits naming the id before it writes the second dump. It also rejects the id index, whose dump index.json would replace. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The replayer rejects a configuration that the model does not accept, such as one with duplicate expected locations, before it runs any step, and the dump then marks every step skipped. The viewer said that the replay failed at step 0, and linked a step 0 that does not exist. It now says that the replay stopped before step 1, with the replayer's message, and that the skipped steps show the initial state. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The node and kind filters, the replay and log order tabs, and the step and record links were click-only spans and links without an href, and the open dump label wrapped a hidden file input, so none of them could take focus. They are now buttons, with aria-pressed on the filters and tabs, and the file input is out of sight but focusable, with a focus ring on its label. They look as before: the underlines stay on the text, as on inline links. Chrome also moved the point that Tab starts from to each row that the viewer scrolled into view, so after the page loaded, Tab skipped the controls above the state pane. The rows pane now scrolls itself, to the same offsets as scrollIntoView. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Amaury Chamayou (achamayou)
force-pushed
the
achamayou-fantastic-waddle
branch
from
October 9, 2026 17:14
7e21e6f to
a40a5f8
Compare
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
When a trace fails to replay (#8282), the replayer names the log line and rule, but not the model state around it. This adds a viewer that steps through a whole run: the trace records, the model state after each step and what it changed, which send each receive took, and where and why the replay stopped. It is published with the docs, showing the recorded traces and some of the invalid traces stored with them.
Implementation summary
disaster-recovery-replay --dump FILE(DisasterRecovery/TraceValidation/Dump.lean) writes a run as JSON: its records, the reduced instructions, and the model state after each step with the actions it enables. A failing step adds each field's observed and model values, or the guards of a disabled action. It steps withrunInstruction, the step thatreplayruns, and takes its outcome fromreplay, so the dump shows exactly what the replayer concludes.replayer/viewer/is a static page, vanilla JS and SVG with no dependencies, that only renders dumps: every semantic fact comes from the Lean side.build.pydumps the recorded traces, one stored invalid trace for each way a replay can stop, applied ascheck-fixtures.shapplies it, and any--logs DIRof node logs.doc/operations/recovery.rstsays how to view your own traces.doc/conf.pybuilds the viewer into the site astrace-viewer/, like doxygen (SKIP_TRACE_VIEWERskips it), anddoc.ymlinstalls Lean for that, with the same pinned elan installer as the SNP job. Thedocsctest that PR CI runs setsSKIP_TRACE_VIEWER, as its runner has no Lean.build.py, which fails if a dump is missing or its outcome disagrees with the replayer's exit code. The quorum and multiple-timeout fixtures gain an invalid trace,commit-order.retry_after_end, the first that stops at a disabled action.To review: on the Lean side there is
Dump.lean, a--dumpflag inreplayer/Main.leanand arunInstructionhook inTraceValidation.lean.Dump.leancalls the replayer and the model rather than repeating them.viewer.jsandindex.htmlare presentation only.Safety and compatibility
No runtime impact: this changes no CCF code and does not change the model. The published viewer shows only checked-in test fixtures. The docs workflow does not run on pull requests, so its
sphinx-multiversioncommand was run locally from this branch, for this branch and main. This branch's site hastrace-viewer/with every dump. main has no viewer, and its site builds without one, as older release branches will.