Proof Portal
Omarchy
ProbeLabs65 findings · 95 requirementsA 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.
Bind descriptions are load-bearing: give binds a stable id
Reported by linyiru · filed Sep 18, 2026 · open at source
At a glance
- 1 · What is claimed?
- Only the report text below — no validator has restated it as checkable claims yet.
- 2 · What does it affect?
- 3 · Is it reproducible?
- No validation has been run yet.
- 4 · What remains unclear?
- Not validated yet: no claims, no reproducer.
- 5 · What happens next?
- Our staff decide whether the report is valid. Where this project allows it, agents decide whether it duplicates another report or a known issue. So far: partly in the audited area (menu) — decided by agents · verified; matches no known issue — decided by agents · verified. The outcome (valid, duplicate, not a bug, …) is not decided yet. See the decision.
Original report
Splitting this out of #12345 §7, where it is listed as needing its own project, at @WokoFlipper's request in https://github.com/omacom/omarchy/issues/12345#issuecomment-5727650774. It lands with no translation runtime, no catalog and no locale: it is a schema change to default/hypr/bindings/*.lua plus the cheatsheet reader. It is worth doing on its own merits, because today a description cannot be reworded either.
What a description is today
o.bind(keys, description, dispatcher, options) (default/hypr/helpers.lua:92) hands the description to five different roles.
- Display text in the cheatsheet,
bin/omarchy-menu-keybindings. - Join key, on both sides of the awk join that merges alternative chords for one action.
- Input to the ordering rules: 52 literal regexes match on description text to set precedence.
- Round-trip key after selection: the caller recovers which row was chosen from the text it displayed. #12363 is the general fix for that shape.
- A window matcher, for 4 binds.
command_from(default/hypr/helpers.lua:56-72) passes the description as the first argument toomarchy-launch-or-focus-webappwhen a bind is{ webapp = …, focus = true }. That reachesomarchy-launch-or-focus:13, where it is interpolated into a jq regex tested against the window's ownclassandtitle. Those are set by the application, and no locale changes them, so a translated description cannot match: the bind stops focusing the existing window and launches a new one on every press. The four areWhatsApp,Google Messages,Google PhotosandGoogle Maps, atdefault/hypr/bindings/applications.lua:28-31. All four are product names a translator would probably leave alone, which is what makes it a trap rather than a bug.
The scale, at 9c5482c5: default/hypr/bindings/*.lua has 193 o.bind/o.bind_toggle call sites across 6 files, of which 186 pass a literal description, 173 of those distinct; 2 pass none; and 5 build key and description in a loop, which is what makes the rendered list roughly 230 rows. The consequences of editing them are measured in #12345 §7: translating the 186 silently destroys 4 of 4 alternative-chord merges and reorders most of the rendered rows, with no error, no non-zero exit and no failing test. test/shell.d/keybindings-menu-test.sh pins 4 descriptions and, incidentally, 1 of the 52 precedence literals.
The shape that fixes it
A third field: a stable id the machinery keys on, and a description that is only ever displayed.
The migration can be incremental, because the id can default to today's value:
-- default/hypr/helpers.lua
function o.bind(keys, description, dispatcher, options)
local opts = options or {}
opts.id = opts.id or description -- every existing bind keeps working
...Joins, precedence and round-trips key on id; the cheatsheet renders description. A bind that gains an explicit id becomes editable, and a bind that does not behaves exactly as it does today. The same holds for the user's own ~/.config/hypr/bindings.lua, which enters the same stream.
The one thing that decides the design, and which I cannot measure from here
The cheatsheet reads hyprctl binds, so whatever carries the id has to survive into that output. Two candidates:
- A bind option. If Hyprland passes unknown
hl.bindoption keys through tohyprctl binds -j, the id rides along and nothing else is needed. - A sidecar map from bind to id, generated next to the lua files and joined by the cheatsheet. It needs no upstream support, but the chord is not a stable key either: it moves with the keymap, and the same action appears under alternative chords, which is the reason the merge exists. So a sidecar has to be keyed on chord plus dispatcher, not chord alone.
The measurement that decides it is one command on a running session: set an extra key in opts, then check whether it appears in hyprctl binds -j | jq '.[0]'. @WokoFlipper, @sbelcl, if either of you gets there before I reach a session, that is the whole blocker.
Already in flight
- #12363 gives
omarchy-menu-selecta--print-index, so a caller stops recovering an id by cutting up the row it displayed. That is role 4 above. - #12362 keys the cheatsheet cache on the active collation. Independent of translation, but the same code path: the row order already depends on
LC_COLLATEtoday, and a translated description would reorder rows for a second reason.
Pilot
@WokoFlipper carries 204 translated binding descriptions as an archive that explicitly must not be applied, and runs the merge machinery daily, so that is the largest ready-made label set and the first real consumer. Checking the schema against it before it lands costs less than finding out after. @sbelcl's runtime is independent of this and does not need to land first.
View raw text
Splitting this out of #12345 §7, where it is listed as needing its own project, at @WokoFlipper's request in https://github.com/omacom/omarchy/issues/12345#issuecomment-5727650774. It lands with no translation runtime, no catalog and no locale: it is a schema change to `default/hypr/bindings/*.lua` plus the cheatsheet reader. It is worth doing on its own merits, because today a description cannot be reworded either.
## What a description is today
`o.bind(keys, description, dispatcher, options)` (`default/hypr/helpers.lua:92`) hands the description to five different roles.
1. **Display text** in the cheatsheet, `bin/omarchy-menu-keybindings`.
2. **Join key**, on both sides of the awk join that merges alternative chords for one action.
3. **Input to the ordering rules**: 52 literal regexes match on description text to set precedence.
4. **Round-trip key** after selection: the caller recovers which row was chosen from the text it displayed. #12363 is the general fix for that shape.
5. **A window matcher**, for 4 binds. `command_from` (`default/hypr/helpers.lua:56-72`) passes the description as the first argument to `omarchy-launch-or-focus-webapp` when a bind is `{ webapp = …, focus = true }`. That reaches `omarchy-launch-or-focus:13`, where it is interpolated into a jq regex tested against the window's own `class` and `title`. Those are set by the application, and no locale changes them, so a translated description cannot match: the bind stops focusing the existing window and launches a new one on every press. The four are `WhatsApp`, `Google Messages`, `Google Photos` and `Google Maps`, at `default/hypr/bindings/applications.lua:28-31`. All four are product names a translator would probably leave alone, which is what makes it a trap rather than a bug.
The scale, at `9c5482c5`: `default/hypr/bindings/*.lua` has 193 `o.bind`/`o.bind_toggle` call sites across 6 files, of which 186 pass a literal description, 173 of those distinct; 2 pass none; and 5 build key and description in a loop, which is what makes the rendered list roughly 230 rows. The consequences of editing them are measured in #12345 §7: translating the 186 silently destroys 4 of 4 alternative-chord merges and reorders most of the rendered rows, with no error, no non-zero exit and no failing test. `test/shell.d/keybindings-menu-test.sh` pins 4 descriptions and, incidentally, 1 of the 52 precedence literals.
## The shape that fixes it
A third field: a stable id the machinery keys on, and a description that is only ever displayed.
The migration can be incremental, because the id can default to today's value:
```lua
-- default/hypr/helpers.lua
function o.bind(keys, description, dispatcher, options)
local opts = options or {}
opts.id = opts.id or description -- every existing bind keeps working
...
```
Joins, precedence and round-trips key on `id`; the cheatsheet renders `description`. A bind that gains an explicit `id` becomes editable, and a bind that does not behaves exactly as it does today. The same holds for the user's own `~/.config/hypr/bindings.lua`, which enters the same stream.
## The one thing that decides the design, and which I cannot measure from here
The cheatsheet reads `hyprctl binds`, so whatever carries the id has to survive into that output. Two candidates:
- **A bind option.** If Hyprland passes unknown `hl.bind` option keys through to `hyprctl binds -j`, the id rides along and nothing else is needed.
- **A sidecar map** from bind to id, generated next to the lua files and joined by the cheatsheet. It needs no upstream support, but the chord is not a stable key either: it moves with the keymap, and the same action appears under alternative chords, which is the reason the merge exists. So a sidecar has to be keyed on chord plus dispatcher, not chord alone.
The measurement that decides it is one command on a running session: set an extra key in `opts`, then check whether it appears in `hyprctl binds -j | jq '.[0]'`. @WokoFlipper, @sbelcl, if either of you gets there before I reach a session, that is the whole blocker.
## Already in flight
- #12363 gives `omarchy-menu-select` a `--print-index`, so a caller stops recovering an id by cutting up the row it displayed. That is role 4 above.
- #12362 keys the cheatsheet cache on the active collation. Independent of translation, but the same code path: the row order already depends on `LC_COLLATE` today, and a translated description would reorder rows for a second reason.
## Pilot
@WokoFlipper carries 204 translated binding descriptions as an archive that explicitly must not be applied, and runs the merge machinery daily, so that is the largest ready-made label set and the first real consumer. Checking the schema against it before it lands costs less than finding out after. @sbelcl's runtime is independent of this and does not need to land first.
Validation
Not checked yet. A validator will restate this report as checkable claims, map it to the project's requirements and write a reproducer that the proof engine runs.
Linked
- Related PRpr/13923· confirmed
- Related PRpr/12557· confirmed
- Related PRpr/13888· confirmed
- Related PRpr/12363· confirmed
Decision
Decisions are recorded by our staff — or, where this project allows it, by agents: checked by a second, independent agent, or by a single agent where the project's policy says so. Any decision reached so far is shown below.
- Decided by agents · verified: partly in the audited area (menu)
- Decided by agents · verified: matches no known issue
The outcome (valid, duplicate, not a bug, …) is not decided yet.