lean-ctx version: 3.9.12 (official binary, ~/.local/bin/lean-ctx)
OS: Linux (Ubuntu, x86_64)
AI tool: Claude Code
What happened:
Dashboard Overview status strip shows Verification 0% (0/0) in red, on a session with no verification problems at all (loss(avg)=0.0%, warn_runs=0, 0 failed proof claims). Two separate defects behind it:
1. 0/0 renders as 0% red instead of "no data".
static/components/cockpit-overview.js, _renderStatusStrip():
var vTotal = verif ? verif.total || 0 : 0;
var vPassed = verif ? verif.pass || 0 : 0;
var vPct = vTotal > 0 ? Math.round((vPassed / vTotal) * 100) : 0;
var vCol = vPct >= 80 ? 'var(--green)' : vPct >= 50 ? 'var(--yellow)' : 'var(--red)';
Empty denominator collapses to 0, which lands in the < 50 red bucket — so "never measured" is painted identically to "every check failed". The CLI is honest about the same state (0/0 pass (100%)), and the Health → Verification tab handles it correctly with an empty state; only the Overview chip misreports. The sloPct computation immediately above has the same total === 0 → 0% shape, so an SLO-less session would read red too.
2. Following the UI's own instruction cannot produce a verification run.
static/components/cockpit-health.js empty state says:
No verification runs yet. Run lean-ctx verify to check output quality.
but lean-ctx verify on 3.9.12 only prints the existing stats — it never records a run, so the counter stays 0/0 forever. It is also absent from lean-ctx help all (which lists verify-cache, savings verify, snapshot ... verify, compliance verify, but no bare verify), and ctx_session action="verify" reports itself deprecated in favour of output_stats. So the documented path out of 0/0 is a dead end.
I could not determine what subsystem is supposed to emit these runs — possibly it is gated behind something not enabled here, so this half may be a docs bug rather than a code bug. The session in question is not idle: 304 tool calls, 31 files touched, terse_mode on, compression_level = "standard", ~282k tokens saved — still zero verification runs. lean-ctx config schema exposes no verify/sampling knob, and the documented env vars (LEAN_CTX_DISABLED/RAW/COMPRESS/DEBUG/AUTONOMY/ENABLED) contain none either.
What you expected:
vTotal === 0 renders neutral — —, n/a, or a muted "not measured" chip — never red. (Same for the sloTotal === 0 case on the neighbouring chip.)
- Either
lean-ctx verify actually performs a verification run (making the Health tab's instruction true), or the Health empty state and --help point at whatever the real trigger is.
Steps to reproduce:
- Run any normal session through the MCP tools (compressed reads/shells) — no verification-specific setup.
lean-ctx dashboard --port=3333 --project=<repo> → Overview.
- Status strip:
Verification 0% (0/0) in red, next to Reliability 100% (3/3) green.
lean-ctx verify → prints stats, changes nothing.
- Reload dashboard → still
0% (0/0) red.
Relevant output:
$ lean-ctx --version
lean-ctx 3.9.12 (official, https://github.com/yvgude/lean-ctx)
$ lean-ctx verify
Verification: 0/0 pass (100%), warn_runs=0, warn_items=0, loss(avg)=0.0%
SLOs: 3/3 passing
Budget[role:coder]: tokens 0/200000 (0%) | shell 0/100 (0%) | cost $0.00/$5.00 (0%) → OK
Proof: written=0 last=-
$ lean-ctx help all | grep -c "^ verify "
0
# ctx_call {"name":"ctx_verify","arguments":{"action":"proof"}} — summary
{"total_claims":37,"proved":4,"passed":33,"failed":0,"skipped":0,"unverified":0}
# dashboard chip source of truth
$ curl -s localhost:3333/static/components/cockpit-overview.js | sed -n '588,594p'
var vTotal = verif ? verif.total || 0 : 0;
var vPassed = verif ? verif.pass || 0 : 0;
var vPct = vTotal > 0 ? Math.round((vPassed / vTotal) * 100) : 0;
var vCol = vPct >= 80
? 'var(--green)' : vPct >= 50
? 'var(--yellow)' : 'var(--red)';
Related in spirit (dashboard metrics reporting a state the data doesn't support): #1104, #1105, #1175.
lean-ctx version: 3.9.12 (official binary,
~/.local/bin/lean-ctx)OS: Linux (Ubuntu, x86_64)
AI tool: Claude Code
What happened:
Dashboard Overview status strip shows
Verification 0% (0/0)in red, on a session with no verification problems at all (loss(avg)=0.0%,warn_runs=0, 0 failed proof claims). Two separate defects behind it:1.
0/0renders as 0% red instead of "no data".static/components/cockpit-overview.js,_renderStatusStrip():Empty denominator collapses to
0, which lands in the< 50red bucket — so "never measured" is painted identically to "every check failed". The CLI is honest about the same state (0/0 pass (100%)), and the Health → Verification tab handles it correctly with an empty state; only the Overview chip misreports. ThesloPctcomputation immediately above has the sametotal === 0 → 0%shape, so an SLO-less session would read red too.2. Following the UI's own instruction cannot produce a verification run.
static/components/cockpit-health.jsempty state says:but
lean-ctx verifyon 3.9.12 only prints the existing stats — it never records a run, so the counter stays0/0forever. It is also absent fromlean-ctx help all(which listsverify-cache,savings verify,snapshot ... verify,compliance verify, but no bareverify), andctx_session action="verify"reports itself deprecated in favour ofoutput_stats. So the documented path out of0/0is a dead end.I could not determine what subsystem is supposed to emit these runs — possibly it is gated behind something not enabled here, so this half may be a docs bug rather than a code bug. The session in question is not idle: 304 tool calls, 31 files touched, terse_mode on,
compression_level = "standard", ~282k tokens saved — still zero verification runs.lean-ctx config schemaexposes no verify/sampling knob, and the documented env vars (LEAN_CTX_DISABLED/RAW/COMPRESS/DEBUG/AUTONOMY/ENABLED) contain none either.What you expected:
vTotal === 0renders neutral ——,n/a, or a muted "not measured" chip — never red. (Same for thesloTotal === 0case on the neighbouring chip.)lean-ctx verifyactually performs a verification run (making the Health tab's instruction true), or the Health empty state and--helppoint at whatever the real trigger is.Steps to reproduce:
lean-ctx dashboard --port=3333 --project=<repo>→ Overview.Verification 0% (0/0)in red, next toReliability 100% (3/3)green.lean-ctx verify→ prints stats, changes nothing.0% (0/0)red.Relevant output:
Related in spirit (dashboard metrics reporting a state the data doesn't support): #1104, #1105, #1175.