Proof Portal
Omarchy
ProbeLabsviewing a historical runA proof layer — requirements, tests and verified fixes — for two of Omarchy's subsystems: the application menu (launcher scripts, QML model, JSONC config, search and selection) and the lock screen (lock scripts, QML, PAM authentication). Scope is deliberately limited to those components of omacom/omarchy; the rest of the distribution is not covered.
Once the guard batch for an open has answered, the Remove menu lists Theme exactly when omarchy-theme-remove has a theme it can remove.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
Once the guard batch for an open has answered, the Remove menu lists Theme exactly when omarchy-theme-remove has a theme it can remove. omarchy-theme-removable names those themes: the directories under ~/.config/omarchy/themes that are not symlinks or dot-directories. The row asks the helper as its when:, and the remover reads its list from it. Until the batch answers, the menu draws the previous answers, as for every guarded row.
when remove_menu_guards_applied the menu_view shall immediately satisfy (remove_theme_row_shown <=> remover_has_removable_theme)
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream omacom/omarchy quattro 393a43d4 (and a85e29ab before it) has this defect. The remove.theme row runs omarchy-theme-remove with no terminal and has no when: guard. The script lists the theme directories that are not symlinks. With none, it prints "No extra themes installed." and exits 1, and nothing shows that line. A stock install has only the bundled themes, so the row only closes the menu for most users. Commit 5bc151f9 moved the remover to the menu picker and dropped the floating terminal that showed the line. The fix names the removable themes once, as omarchy-theme-extras does for Update > Extra Themes. omarchy-theme-removable lists them and exits nonzero when there are none. The row asks it as its when:, and the remover reads its list from it, so the two cannot disagree. The picker also stops offering a dot-directory, which the remover refuses. A themes folder that is itself a symlink offers nothing, as before the change. Each open re-runs the guards. The menu first draws the previous answers and updates when the batch lands, about half a second later. A user menu that overrides remove.theme replaces the whole row, guard included.
Verification & provenance
How this requirement was checked: the review trail, edit history, and the machine-analysis status terms (each ⓘ explains what it means).
Review
- Status
- in_review
- Reviewer
- Claude Pr New C · AI agent
- Reviewed
- Oct 3, 2026, 08:05 UTC
History
- Created
- Oct 3, 2026, 07:58 UTC · Claude Pr New C · AI agent
- Modified
- Oct 3, 2026, 13:29 UTC · Claude Pr New C · AI agent
Hazard review
- scenarioreviewededge_caseboundaryinput_domain
Worst cases: the row shows with nothing to remove and only closes the menu, or the row hides while a theme could be removed (a guard narrower than the remover, for example a when: of false). edge_case: each shape of the themes directory is a case. Hidden: missing, empty, a symlinked working copy only, only .git, only .backup, only a stray file. Also hidden: a themes folder that is itself a symlink into a dotfiles directory, which offers nothing, as on a85e29ab. Shown: a copied theme, a cloned theme, a worktree with a .git file, .git beside a real theme, and a theme named -n. All twelve are witnessed. boundary: zero versus one removable directory; the empty and copied homes witness both sides. input_domain applied: the entry kinds decide it. A symlink never counts, a plain file never counts, a name with a leading dot never counts, and nothing in a symlinked themes folder counts. A real directory counts whatever else sits beside it (mixed home), and the picker then offers only that directory. Names with a newline or a leading -- are pre-existing remover behaviour, outside this change and outside this requirement. concurrency_scale not applicable: each open re-runs the batch. The menu first draws the previous answers for about half a second, as for every guarded row. So a theme added or removed shows when the batch for that open lands.
- propertyreviewedtotality
Every HOME shape gives one defined answer once the batch has answered, row shown or row hidden. That answer equals whether the remover offers a name it would remove. No shape shows the row with nothing to offer or hides it with a theme to offer. Before the batch answers, the row keeps the previous answer (shown at the first open), as every guarded row does.
- structuralnot applicable
One JSONC string and one find predicate; no memory, encoding or numeric surface. The escaped quotes in the JSONC string are covered by the witness, which parses the shipped row.
- domainnot applicable
The guard reads the user's own HOME with user privileges and removes nothing. The removal is the remover script's own, unchanged.
Change history
Every recorded revision of this requirement's source file — newest first, each with its commit message and the diff for that change.
Review history
Human and AI-agent approvals of this requirement — the 'why was this approved' lineage, each with the reviewer's justification and the code it cites.
- Claude Pr New C · AI agentApprovedSpec conformanceOct 3, 2026 · 20 hours agoREVIEW-261003-C7RT
Read default/omarchy/omarchy-menu.jsonc, bin/omarchy-theme-removable, bin/omarchy-theme-remove and shell/plugins/menu/MenuModel.js on the mirror tree (the baseline plus the fix). The remove.theme row now carries "when":"omarchy-theme-removable". The helper lists the directories under ~/.config/omarchy/themes that are not symlinks or dot-directories, and exits nonzero when there are none. omarchy-theme-remove reads its picker list from the same helper. The guard batch (guardScript) answers remove.theme:w:0 when the directory is missing, empty, holds only symlinks, dot-directories or files, or is itself a symlink, and isVisible hides a row whose when: answered false. With a copied, cloned or worktree theme, .git beside a real theme, or a theme named -n, the guard answers 1, the row shows, and the picker offers only the real theme. So remove_theme_row_shown equals remover_has_removable_theme once remove_menu_guards_applied. Both violation rows need the guard and the remover to ask different questions, which they no longer can: a shown row with nothing to remove (the a85e29ab row with no when:) and a hidden row with a theme to remove (a guard narrower than the helper). Both are dispositioned defensive; the shown-side homes fail on the second. Before the batch for an open answers, the menu draws the previous answers (no-action row, witnessed in the mirror test). Witnesses in test/shell.d/menu-guards-test.sh run the shipped row through the generated batch and the real remover with a stub picker over twelve homes, and check the helper and picker lists for the mixed home; test/shell.d/menu-test.sh pins the when:. They fail on a85e29ab.
Cited code (4)
Obligations
What this requirement must witness to be considered satisfied — the required evidence, and the tests that discharge each one.
The tests that discharge each obligation aren't available for a historical run
The evidence matrix behind each obligation comes from the live audit index, which can't be rebuilt for a past commit. Nothing here means unknown — not that the requirement has no obligations.
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
Formula evidence
The formal formula behind this requirement, the variables it is written over, and the tests that exercise it (each term is explained inline).
FRETish formula
when remove_menu_guards_applied the menu_view shall immediately satisfy (remove_theme_row_shown <=> remover_has_removable_theme)
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| remove_menu_guards_applied | — | The guard batch has answered the Remove menu rows, and the menu applies those answers. | |
| remover_has_removable_theme | — | omarchy-theme-removable lists at least one theme: a directory under ~/.config/omarchy/themes that is not a symlink and has no leading dot, in a themes folder that is not itself a symlink. That is what the remover's picker offers. | |
| remove_theme_row_shown | — | The Remove menu lists Theme. |
Witnesses· 2 scenarios total
- preludeexercises 2 condition scenarios
MC/DC truth table· 4 rows
Each row assigns the formula's conditions (T/F) and shows the Result— the formula's value for that input row, not a test pass/fail. A row proves a condition when flipping only that condition flips the outcome. The test that covers each row is linked.
mcdc:ignoreNo-actionfalse-result row satisfied by designUncoveredneeds a covering test| # | remove_menu_guards_applied | remove_theme_row_shown | remover_has_removable_theme | Result | Proves | Covering test |
|---|---|---|---|---|---|---|
| 1 | F | T | F | T | remove_menu_guards_applied | |
| 2 | T | F | T | F | remove_theme_row_shown | — |
| 3 | T | T | F | F | remove_menu_guards_applied | — |
| 4 | T | T | T | T | remove_theme_row_shown |
Its place
How this requirement connects — what proves it, what it affects, and what it rests on. Authored links only here; automatically derived links come from the audit index.
Loading graph…
Trace evidence
The concrete artifacts linked to this requirement — implementing code, verifying tests, documents, and the findings raised against it.
0 open · 1 resolved
No open findings
Everything flagged against this requirement has been resolved.
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
Impact
Blast radius — authored trace links only (automatically derived links come from the audit index and aren't shown here).
If you change this
Files to re-check (3)
- omarchy-theme-removablebin/omarchy-theme-removable
- omarchy-theme-removebin/omarchy-theme-remove
- omarchy-menu.jsoncdefault/omarchy/omarchy-menu.jsonc
Tests to re-run (14)
- guard-remove-theme-cloned.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-cloned.events
- guard-remove-theme-copied.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-copied.events
- guard-remove-theme-dashed.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-dashed.events
- guard-remove-theme-dotted.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-dotted.events
- guard-remove-theme-empty.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-empty.events
- guard-remove-theme-filed.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-filed.events
- guard-remove-theme-folded.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-folded.events
- guard-remove-theme-hidden.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-hidden.events
- guard-remove-theme-linked.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-linked.events
- guard-remove-theme-missing.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-missing.events
- guard-remove-theme-mixed.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-mixed.events
- guard-remove-theme-worktree.eventstest/bdiff/corpus/lifecycle/guard-remove-theme-worktree.events
- harness.mjstest/bdiff/harness.mjs
- menu-guards-test.shtest/shell.d/menu-guards-test.sh
What this rests on
Discussions
Discuss this with the proof team. Nothing changes in your audit automatically — you open a request and a staff member records any outcome inside the thread.