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.
When two given paths reach the same file under the same file name, the file picker lists that file in one row.
Specification
The requirement exactly as authored — its complete prose text and, where present, the formal FRETish sentence it compiles to.
When two given paths reach the same file under the same file name, the file picker lists that file in one row. One root can be a symbolic link to another root, or a caller can give the same root twice. The picker keys a row on the device and inode numbers plus the file name, so hard links under different names stay separate rows.
when same_file_reached_twice the file_picker shall eventually satisfy file_listed_once
Rationale & tags
Why this requirement exists, and how it is categorised.
Rationale & tags
Why this requirement exists, and how it is categorised.
Upstream PR omacom/omarchy#13197 (head cc710e11) adds this behaviour to bin/omarchy-menu-file. When find follows link roots, a root linked to another given root lists each file twice, under two paths. Pictures linked to Videos is the example in the PR. The PR prints the device and inode number of each file. After the newest-first sort it keeps the first row for each device, inode and file name. Commit cc710e11 added the file name to the key; the maintainers' bot pushed it, and the PR author agreed. Two hard links under different names now stay separate rows, because transcode and the retro installer derive their output from the chosen name. A file reached through aliased roots always keeps its name, so it still gives one row. Known limitation: two hard links with the same name in different directories give one row. The user can then pick only one of the two paths. The PR discussion keeps this on purpose: both paths hold identical content, and one find -printf call cannot tell the parent directories apart.
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 13197 · AI agent
- Reviewed
- Oct 2, 2026, 01:10 UTC
History
- Created
- Oct 2, 2026, 00:58 UTC · Claude Pr 13197 · AI agent
- Modified
- Oct 3, 2026, 10:32 UTC · Claude Code · AI agent
Hazard review
- scenarioreviewedboundaryedge_case
Worst case: a file is offered twice, or a distinct file the user wants is hidden. boundary: one row per device, inode and file name across all roots, after the newest-first sort (witnessed: a link root and its target, and the same root given twice, each give one row). edge_case: two hard links under different names give two rows (the PR's own test); two hard links with the same name in different directories give one row, so the user can pick only one of the two paths (the known limitation in the rationale); which spelling stays depends on the sort order of equal rows. Files on different devices with the same inode number stay distinct rows because the key holds the device number. input_domain not applicable: the key is find metadata and the file name, not file contents. concurrency_scale not applicable: one run per user action. error_handling not applicable: the dedup step cannot fail; it filters the rows find printed.
- propertyrevieweddeterminismidempotency
determinism: for a given directory state the kept row is fixed by the sort order. idempotency: giving a root a second time adds no row.
- structuralnot applicable
awk keys on the first tab-separated field (%D:%i, printed by find from metadata) plus the base name it takes after the first two fields, so a tab in a file name stays in the name. A newline in a file name splits a row, as at the base.
- domainnot applicable
Local filesystem reads only; no network, crypto, secrets or privilege surface.
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 Code · AI agentApprovedSpec conformanceOct 3, 2026 · 23 hours agoREVIEW-261003-GFB2
Recorded by agent:claude-code under the repository owner's explicit delegation for this change (2026-10-03). This is not a personal human review. WHAT CHANGED: PR #13197 head cc710e11 adds the file name to the dedup key, so the requirement now reads: one row per file reached twice under the same name, and hard links under different names stay separate rows. The maintainers' bot pushed cc710e11 and the PR author agreed, so the requirement follows that intent. The same-name hard-link case (one row, one path not pickable) is recorded in the rationale as the PR's known limitation. CHECKED AGAINST: bin/omarchy-menu-file at cc710e11. find prints device:inode, mtime and path; after the newest-first sort, awk derives the base name from the path and keeps the first row per device:inode plus name; cut drops the key and the mtime. A file reached through a link root and its target, or a root given twice, keeps its name, so it gets one row: same_file_reached_twice leads to file_listed_once. The violation row needs the awk filter or the key removed, and stays dispositioned defensive. The PR's own test adds a hard-link pair under two names and expects two rows.
Cited code (4) - Claude Pr 13197 · AI agentApprovedSpec conformanceOct 2, 2026 · 2 days agoREVIEW-261002-VZ1K
Read bin/omarchy-menu-file on the PR #13197 tree at head 03e6af6a. find prints each match as device:inode, mtime and path; the rows are sorted newest first on the mtime field and awk keeps the first row per device:inode key before cut drops the key and the mtime. A file reached through two given paths (a link root and its target, or a root given twice) thus gets one row: same_file_reached_twice leads to file_listed_once. The violation row needs the awk filter or the key field removed; it is dispositioned defensive. The key is the file, not the path, so two hard links to one file also give one row, and of two equal rows the lexically smaller line is kept (sort falls back to a whole-line comparison). Witnesses in test/shell.d/menu-file-test.sh: a link root plus its target, and a root given twice, each list the file once; a single real root lists its file once.
Cited code (2)
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 same_file_reached_twice the file_picker shall eventually satisfy file_listed_once
Variables
| Name | Type | Direction | Description |
|---|---|---|---|
| same_file_reached_twice | — | Two paths given to omarchy-menu-file reach the same file under the same file name, because one root is a symbolic link to another root (or to a directory above it) or the same root is given twice. Hard links to one file under different names are not the same file here. | |
| file_listed_once | — | The file has one row in the listing. |
Witnesses· 2 scenarios total
- menu-file-test.sh:1exercises 2 condition scenarios
MC/DC truth table· 3 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| # | file_listed_once | same_file_reached_twice | Result | Proves | Covering test |
|---|---|---|---|---|---|
| 1 | F | F | T | same_file_reached_twice | |
| 2 | F | T | F | file_listed_once | — |
| 3 | T | T | T | file_listed_once |
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.
No findings affect this requirement
Nothing was flagged against this requirement in the pinned run.
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 (1)
- omarchy-menu-filebin/omarchy-menu-file
Tests to re-run (2)
- menu-file-symlink-root-test.shtest/shell.d/menu-file-symlink-root-test.sh
- menu-file-test.shtest/shell.d/menu-file-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.