Onboarding: a first-run tour on every client

AGENTS.md

@@ -46,6 +46,7 @@ When using Bend:
 - `src/core/bothub.bend`'s `Dir.*` and `DirWork.*`: per-peer directory merges and a four-slot deduplicating refresh queue (laws `remote_dir_*`). `src/server/botnet.bend` uses two-second connect/four-second total deadlines and atomically caches the directory in `<home>/bots.cache`; the hub publishes each peer as it arrives, restores cached rows away at startup, and refreshes on links and peer return. Tests: `test/botdir_test.bend`, `test/tools/botdir_e2e.ts`.
 - `src/core/subs.bend`: the Subagents panel (pure): the tasks a thread delegated and what Claude runs for it (Agent calls, background shells and monitors: model.bend's `Bg`, whose line keeps the call, what it was asked and its kind, `Bg.kind`; a shell's row reads "shell: …" and only subagents count as agents). A subagent's lines (`parent_tool_use_id`) go to its own log, `M.Bg.log(thread)` (`@sub:<thread>`, off the timeline; hub.bend's `Sub.*`), never the thread's messages. Rows at work say what they do now; a subagent at work shows its newest steps until shut (`fold` action, key `sub:<call>`); the panel is outlined in the accent with "N at work" while any work, and a sidebar row says "N agents" where its age goes (`Subs.badge`). The panel is open while any row works and folds to its head ("Subagents · 3 done") once all are done; a click on the head opens or shuts it, and that choice holds (`Subs.panel.*`, the `fold` action with key `subs:<thread>`); folded, the web's panel scrolls with the thread instead of sticking to its top. Window `Lay.subs`/`Sa.*` (above the timeline), web `View.subs` (sticky), phones `subs` (above the composer). Laws `subs_*`, `bg_start_keeps_call`; test `test/subagents_test.bend`.
 - `src/core/tools.bend`: the thread header's buttons, one list for all four clients (pure: each an icon, a label, a sentence for its tooltip, on/danger, and where a group starts; stop, then pin/settle/snooze/archive/delete, then fork thread/bring back, then terminal/panel; laws `tools_*`). The window draws them icon + label with a line between groups and drops to icons only when the title would be squeezed (`Lay.tools` in layout.bend; the terminal button is the window action `vw-key`); the web as `WIcon.button`s (`View.tools`); the phones' toolbar menus map the icon names to SF Symbols and Material icons (`icon(_:)` in Views.swift, `toolIcon` in ThreadParts.kt). The panel button is "Viewer" (it holds Board, Schematic, 3D, Mech, Files, Diff and Browser), so the header has no Diff button of its own. An agent starting in a KiCad project opens its thread's panel on the board (hub.bend's `Auto.view`, sent by server.bend's `Hub.auto` at each Claude, Codex or Grok start as a `view` message with `auto`); a client takes it only while that thread's viewer has shown nothing and its panel was never toggled by hand (client.bend's `Viewer.auto`, `panel.hand:<t>`; laws `viewer_auto_*`, `auto_view_none`).
+- `src/core/onboard.bend`: the first-run tour (pure: the steps, each a title, words that depend on the client (`Ob.body(k, days, i)`, k 0 window, 1 web, 2 phone: controls differ) and a target (`sidebar`/`add`/`head`/`settings`; phones none; `U.Tour.target` drops `head` unless a thread's own header is on screen (`Tour.head`: its timeline shows, not Settings, a room, a remote chat or a bot, whatever thread is still selected under them)); the thread buttons are plain sentences naming tools.bend's labels (`Tools.label`, tied in test/onboard_test.bend); the Tailscale words follow Settings' row (`Tail.*` in client.bend, all four clients, read the hub's own report, info `tailscale`: off (the flag), checking, unavailable (no tailnet address or the bind failed), reachable (its own tailnet listener, or the main one already covers the address, `--host 0.0.0.0`: `Tailnet.covered`); the report rides with the pairing link in `Net.link` (`Tailnet.report*` in core/tailnet.bend), and the link stays a separate fact; a hub too old to report is read by its pairing link); the step on screen `Ob.at(ready, done, raw)`, `Ob.next`/`Ob.back`/`Ob.skip`, `Ob.forward` reads Done on the last; the keys `Ob.dom`/`Ob.sym`, one policy for all clients; laws `onboard_*`). client.bend's `Tour.*` keeps the step in the scratch `@tour` (digits: came up by itself; `m`+digits: asked for from Settings' "Show the tour") and the one fact that outlives it as the hub setting `onboard.done` (skip and Done set it, `ob-open` shows it again). A tour that came up by itself waits until this connection's log has arrived (`@sync`, set by `Ui.reset`, cleared by `Ui.online` and by `Ui.unsync`, which the web calls after putting its saved log back (`App.unsync`) and bridge.js after loading the phone's saved state (`Hubs.stale`): a cached state is not current; laws `onboard_cache_unsynced`, `onboard_phone_cache_unsynced`) and closes when the hub says done, even after it advanced and even from another client; a hand-opened one stays until ended. Leaving puts the keyboard in a field of the view on screen (`Tour.focus`: a room's, a remote chat's, an open thread's composer), else nowhere. Actions `ob-next`/`ob-back`/`ob-skip`/`ob-open` (routed before the action table in `Ui.act`). Window: `Lay.tour` (dims all but the target, a card whose words scroll (the wheel over it, `Tour.wheel`, `@tour.sc`, the card's `ob-scroll` hit carries the overflow) within what the window leaves after the always-visible buttons; where not even two lines fit the card is compact: the title joins the text, and under about 100 px tall the card is cut by the window while the keys still work; hits are `ob-`) and nui.bend's `Tour.event` (modal: paste and drop go nowhere, blur/focus still processed, every physical key (keycode, `WKey.kc`) pressed while it is up stays in quarantine (`@q.<keycode>`, `Held.*`) until its release, whichever way the tour closes; a blur keeps it. win.c asks for XKB detectable auto-repeat and, where the server lacks it, ignores a release while `XQueryKeymap` still shows the key down (`win_key_down`), and on FocusIn reports the releases it missed (`win_keys_missed`); a release carries its press's keysym; laws `held_*` (nothing in quarantine passes everything through); `xpoke hold`/`holdx KEY MS` test it); web: `View.tour` (a real dialog: host.js makes the page inert, traps Tab, blocks other keys, ctrl/meta combos, paste and drop; every `KeyboardEvent.code` pressed while it is up, modified ones too, has its repeats dropped after it closes, with their keypress and input, until keyup or a fresh keydown; keys through app.bend's `tour_key`, focus restored on close; the card scrolls; class `tour-<target>` lifts the target in style.css); phones: the `tour` object in `Mob.screen` (the focused hub's), a sheet in SwiftUI (`TourSheet`, scrolls) and a dialog in Compose (dismiss = skip, same as iOS), each shown only when nothing else is presented: Bend leaves the step out of the screen model while it knows of another overlay (`Mob.covered`: error, menus, delete/rename/remove, Settings, Find, folders, forms, viewer, diff, terminal, history menu, routine form); iOS also waits until no view controller is presented over the root (`Presented.none`, `tourWait`), Android until the app's own dialogs are gone (`Overlay`/`Overlaid()`) and the hubs screen is shut. Test: `test/onboard_test.bend`.
 - Renaming threads (client.bend's `Ren.*`, all four clients): any thread's menu has Rename (`row-rename`; laws `menu_renames_*`), and a click on the thread's title in the window's or the web's header starts it. `@ren` names the thread and `@f.title` holds the text; the window (`Ren.field` in layout.bend, focus alias `thread-title`) and the web (`View.title.k`) edit it in the header, the phones in a dialog (`renaming` in screen.bend; `rename-save` with `id\u001ftitle`, routed by its hub). `rename-save` sends `thread.rename`, `rename-no` cancels. The hub trims a title and ignores a blank one (hub.bend's `Rename.changes`, law `rename_blank_nothing`); a far thread's rename goes to its machine (`Fr.methods`). Test: `test/sidebar_test.bend`.
 - `src/core/once.bend`: lists that show each thing once (pure: items keyed by what they stand for, the first of each key kept; laws `once_distinct`, `once_keeps`). The bot lists key a bot here by its id and one elsewhere by its name at its machine's link id (`BU.key`, `BT.Member.key`): the sidebar (`BU.rows`), the room picker (`BU.picks`) and the phone over every paired hub (`Hubs.bots`); laws `bot_rows_once`, `bot_picks_once`, `hubs_bots_once`. Test: `test/botlist_test.bend`.
 - `src/core/notice.bend`: which ended turns alert the person, and under which key (pure; one alert per room exchange across hubs, failures, asks and the person's own work kept; laws `notice_*`). Used by the hub's APNs push (`src/server/push.bend`) and the phone's alerts (`src/mobile/notify.bend`). See "Notifications" in `docs/bots.md`. Test: `test/notice_test.bend`.

LAWS.bend

@@ -14,6 +14,7 @@ import ./src/core/hub.bend as H
 import ./src/core/refs.bend as RF
 import ./src/core/todo.bend as TD
 import ./src/core/apikeys.bend as AK
+import ./src/core/onboard.bend as OBD
 import ./src/core/fm.bend as FMG
 import ./src/core/acp.bend as AC
 import ./src/core/mcp.bend as MC
@@ -4527,3 +4528,201 @@ law qr_link_none:
 # no pairing link, no code
 law pair_qr_none:
   {U.Pair.qr.ready(Map.new(&2, String)) == False{} : Bool}
+# The first-run tour (core/onboard.bend). Every step has a title, a known
+# target and words for the window, the web and the phones.
+law onboard_steps_sound:
+  {OBD.Ob.sound() == True{} : Bool}
+
+# next and back stay within the steps for every number from 0 to 14 (past
+# the end they clamp), a step on screen goes forward by next and (past the
+# first) back by back
+law onboard_nav_every_step:
+  {OBD.Ob.nav(14n) == True{} : Bool}
+
+law onboard_back_floor:
+  {OBD.Ob.back(0n) == 0n : Nat}
+
+law onboard_next_step:
+  {OBD.Ob.next(2n) == 3n : Nat}
+
+law onboard_back_step:
+  {OBD.Ob.back(3n) == 2n : Nat}
+
+# next from the last step ends it, and the end stays the end
+law onboard_next_ends:
+  {OBD.Ob.live(OBD.Ob.next(8n)) == False{} : Bool}
+
+law onboard_end_stays:
+  {OBD.Ob.next(OBD.Ob.count()) == OBD.Ob.count() : Nat}
+
+# skip ends it from anywhere
+law onboard_skip_ends:
+  {OBD.Ob.live(OBD.Ob.skip()) == False{} : Bool}
+
+# a tour that came up by itself waits for this connection's state
+law onboard_waits:
+  for done: Bool
+  {OBD.Ob.at(False{}, done, "") == OBD.Ob.count() : Nat}
+
+# a first run shows the first step; once done it never shows by itself
+law onboard_fresh_first:
+  {OBD.Ob.at(True{}, False{}, "") == 0n : Nat}
+
+law onboard_done_quiet:
+  {OBD.Ob.at(True{}, True{}, "") == OBD.Ob.count() : Nat}
+
+# one that came up by itself and was moved on keeps its step, and closes
+# when the hub says it is done (from another client too)
+law onboard_auto_moved:
+  {OBD.Ob.at(True{}, False{}, OBD.Ob.raw(False{}, 4n)) == 4n : Nat}
+
+law onboard_done_closes_auto:
+  {OBD.Ob.at(True{}, True{}, OBD.Ob.raw(False{}, 5n)) == OBD.Ob.count() : Nat}
+
+# one asked for by hand shows whatever the hub says, offline too
+law onboard_hand_stays:
+  {OBD.Ob.at(True{}, True{}, OBD.Ob.raw(True{}, 5n)) == 5n : Nat}
+
+law onboard_hand_offline:
+  {OBD.Ob.at(False{}, False{}, OBD.Ob.raw(True{}, 2n)) == 2n : Nat}
+
+law onboard_wild_ends:
+  {OBD.Ob.at(True{}, False{}, "99") == OBD.Ob.count() : Nat}
+
+# phones point at nothing
+law onboard_phone_no_target:
+  {OBD.Ob.target(2n, 3n) == "" : String}
+
+# one policy for the keys, in the window and the web
+law onboard_keys:
+  {OBD.Ob.dom("Enter") ++ OBD.Ob.dom("ArrowLeft") ++ OBD.Ob.dom("Escape") ++ OBD.Ob.dom("a") == "ob-nextob-backob-skip" : String}
+
+law onboard_syms:
+  {OBD.Ob.sym(65293) ++ OBD.Ob.sym(65361) ++ OBD.Ob.sym(65307) ++ OBD.Ob.sym(97) == "ob-nextob-backob-skip" : String}
+
+# the client: a state not yet current shows nothing; skipping sets the
+# hub's setting; a done from elsewhere closes a tour that was moved on;
+# the Settings button shows it again after it was done
+def OnbUi.log() -> M.State:
+  M.State.replay([M.ProjectCreated{"p1", "p", "/p", 1n}], M.State.empty())
+
+def OnbUi.done() -> M.State:
+  M.State.replay([M.ProjectCreated{"p1", "p", "/p", 1n}, M.SettingSet{"onboard.done", "1", 2n}], M.State.empty())
+
+def OnbUi.synced(st: M.State) -> U.Ui:
+  U.Ui.scratch_set(U.Ui.adopt.raw(U.Ui.init(1n), st), "@sync", "1")
+
+def OnbUi.after(a: U.Act) -> U.Ui:
+  match a:
+    case U.Act{u, _}:
+      u
+
+law onboard_unsynced_hidden:
+  {U.Tour.at(U.Ui.adopt.raw(U.Ui.init(1n), OnbUi.log())) == OBD.Ob.count() : Nat}
+
+law onboard_synced_shows:
+  {U.Tour.at(OnbUi.synced(OnbUi.log())) == 0n : Nat}
+
+law onboard_finish_sets_done:
+  {U.Tour.done(U.Ui.state(OnbUi.after(U.Ui.act(OnbUi.synced(OnbUi.log()), "ob-skip", "")))) == True{} : Bool}
+
+law onboard_elsewhere_closes:
+  {U.Tour.at(U.Ui.adopt.raw(OnbUi.after(U.Ui.act(OnbUi.synced(OnbUi.log()), "ob-next", "")), OnbUi.done())) == OBD.Ob.count() : Nat}
+
+law onboard_reopen:
+  {U.Tour.at(OnbUi.after(U.Ui.act(OnbUi.synced(OnbUi.done()), "ob-open", ""))) == 0n : Nat}
+
+# State put back from a cache (a page's saved log, a phone's saved state) is
+# not this connection's: only a live log shows the tour
+def OnbUi.live() -> U.Ui:
+  U.Ui.recv.k(0n, U.Ui.init(1n), U.Seq.demo("log", [C.Change.encode(M.ProjectCreated{"p1", "p", "/p", 1n})]))
+
+def OnbUi.phone() -> Hb.Hubs:
+  Hb.Hubs{"c", 1n, "h", [Hb.Hub{"h", OnbUi.live()}]}
+
+law onboard_live_log_shows:
+  {U.Tour.at(OnbUi.live()) == 0n : Nat}
+
+law onboard_cache_unsynced:
+  {U.Tour.at(U.Ui.unsync(OnbUi.live())) == OBD.Ob.count() : Nat}
+
+law onboard_phone_cache_unsynced:
+  {U.Tour.at(Hb.Hubs.ui(Hb.Hubs.stale(OnbUi.phone()), "h")) == OBD.Ob.count() : Nat}
+
+# the keyboard goes back to, and the head is pointed at, only what is on
+# screen: a thread selected under a room, a remote chat, a bot's view or
+# Settings is not
+def OnbUi.thread() -> U.Ui:
+  U.Bots.sel.set(OnbUi.live(), "t1")
+
+def OnbUi.step(u: U.Ui, s: String) -> U.Ui:
+  U.Ui.scratch_set(u, "@tour", s)
+
+law onboard_focus_thread:
+  {U.Tour.focus(OnbUi.thread()) == "composer" : String}
+
+law onboard_focus_none:
+  {U.Tour.focus(OnbUi.live()) == "" : String}
+
+law onboard_focus_remote:
+  {U.Tour.focus(U.Bots.views(OnbUi.thread(), "", "", "x")) == "remote-send" : String}
+
+law onboard_focus_room:
+  {U.Tour.focus.k(False{}, True{}, "", True{}) == "room-post" : String}
+
+law onboard_focus_settings:
+  {U.Tour.focus(U.Ui.flag_on(OnbUi.thread(), "settings")) == "" : String}
+
+law onboard_head_thread:
+  {U.Tour.target(0n, OnbUi.step(OnbUi.thread(), "m3")) == "head" : String}
+
+law onboard_head_remote:
+  {U.Tour.target(0n, OnbUi.step(U.Bots.views(OnbUi.thread(), "", "", "x"), "m3")) == "" : String}
+
+law onboard_head_settings:
+  {U.Tour.target(0n, OnbUi.step(U.Ui.flag_on(OnbUi.thread(), "settings"), "m3")) == "" : String}
+
+# keys pressed while the tour is up stay quarantined until let go, however
+# the tour closes, until their release
+def OnbN.n() -> N.Nui:
+  N.Nui.init(U.Ui.init(1n), 800, 600)
+
+law held_set_has:
+  {N.Held.has(N.Nui.ui(N.Held.set(OnbN.n(), 36)), 36) == True{} : Bool}
+
+law held_other_key:
+  {N.Held.has(N.Nui.ui(N.Held.set(OnbN.n(), 36)), 38) == False{} : Bool}
+
+law held_let_frees:
+  {N.Held.has(N.Nui.ui(N.Held.let(N.Held.set(OnbN.n(), 36), 36)), 36) == False{} : Bool}
+
+# with nothing in quarantine every key press and release goes through as it
+# always did
+law held_empty_passes_press:
+  {N.Nui.event.t(False{}, OnbN.n(), W.WKey{97, 97, 0, True{}, 38}) == N.Nui.event.go(False{}, OnbN.n(), W.WKey{97, 97, 0, True{}, 38}) : N.Step}
+
+law held_empty_passes_release:
+  {N.Nui.event.t(False{}, OnbN.n(), W.WKey{97, 0, 0, False{}, 38}) == N.Nui.event.go(False{}, N.Held.let(OnbN.n(), 38), W.WKey{97, 0, 0, False{}, 38}) : N.Step}
+
+law held_none_at_first:
+  {N.Held.has(N.Nui.ui(OnbN.n()), 36) == False{} : Bool}
+
+law held_swallowed_without_tour:
+  {N.Nui.event.t(False{}, N.Held.set(OnbN.n(), 36), W.WKey{65293, 0, 0, True{}, 36}) == N.Step{N.Held.set(OnbN.n(), 36), Nil{}, False{}} : N.Step}
+
+# the wheel over the tour's card scrolls two lines a notch within what
+# overflows
+law tour_scroll_down:
+  {N.Tour.scroll(0n, 5n, False{}) == 2n : Nat}
+
+law tour_scroll_down_stops:
+  {N.Tour.scroll(4n, 5n, False{}) == 5n : Nat}
+
+law tour_scroll_up:
+  {N.Tour.scroll(3n, 5n, True{}) == 1n : Nat}
+
+law tour_scroll_up_stops:
+  {N.Tour.scroll(1n, 5n, True{}) == 0n : Nat}
+
+law tour_scroll_none:
+  {N.Tour.scroll(0n, 0n, False{}) == 0n : Nat}

PROOF.bend

@@ -6519,3 +6519,144 @@ def Laws.qr_link_none():
   {==}
 def Laws.pair_qr_none():
   {==}
+
+def Laws.onboard_steps_sound():
+  {==}
+
+def Laws.onboard_nav_every_step():
+  {==}
+
+def Laws.onboard_back_floor():
+  {==}
+
+def Laws.onboard_next_step():
+  {==}
+
+def Laws.onboard_back_step():
+  {==}
+
+def Laws.onboard_next_ends():
+  {==}
+
+def Laws.onboard_end_stays():
+  {==}
+
+def Laws.onboard_skip_ends():
+  {==}
+
+def Laws.onboard_fresh_first():
+  {==}
+
+def Laws.onboard_done_quiet():
+  {==}
+
+def Laws.onboard_auto_moved():
+  {==}
+
+def Laws.onboard_done_closes_auto():
+  {==}
+
+def Laws.onboard_hand_stays():
+  {==}
+
+def Laws.onboard_hand_offline():
+  {==}
+
+def Laws.onboard_wild_ends():
+  {==}
+
+def Laws.onboard_phone_no_target():
+  {==}
+
+def Laws.onboard_keys():
+  {==}
+
+def Laws.onboard_syms():
+  {==}
+
+def Laws.onboard_unsynced_hidden():
+  {==}
+
+def Laws.onboard_synced_shows():
+  {==}
+
+def Laws.onboard_finish_sets_done():
+  {==}
+
+def Laws.onboard_elsewhere_closes():
+  {==}
+
+def Laws.onboard_reopen():
+  {==}
+
+def Laws.onboard_waits(done):
+  {==}
+
+def Laws.onboard_live_log_shows():
+  {==}
+
+def Laws.onboard_cache_unsynced():
+  {==}
+
+def Laws.onboard_phone_cache_unsynced():
+  {==}
+
+def Laws.onboard_focus_thread():
+  {==}
+
+def Laws.onboard_focus_none():
+  {==}
+
+def Laws.onboard_focus_remote():
+  {==}
+
+def Laws.onboard_focus_room():
+  {==}
+
+def Laws.onboard_focus_settings():
+  {==}
+
+def Laws.onboard_head_thread():
+  {==}
+
+def Laws.onboard_head_remote():
+  {==}
+
+def Laws.onboard_head_settings():
+  {==}
+
+def Laws.held_set_has():
+  {==}
+
+def Laws.held_other_key():
+  {==}
+
+def Laws.held_let_frees():
+  {==}
+
+def Laws.held_empty_passes_press():
+  {==}
+
+def Laws.held_empty_passes_release():
+  {==}
+
+def Laws.held_none_at_first():
+  {==}
+
+def Laws.held_swallowed_without_tour():
+  {==}
+
+def Laws.tour_scroll_down():
+  {==}
+
+def Laws.tour_scroll_down_stops():
+  {==}
+
+def Laws.tour_scroll_up():
+  {==}
+
+def Laws.tour_scroll_up_stops():
+  {==}
+
+def Laws.tour_scroll_none():
+  {==}

mobile/android/app/src/main/java/dev/backplane/mobile/Bots.kt

@@ -547,6 +547,7 @@ private fun SettingsTab(m: AppModel, b: BotView, st: BotSettings) {
         HorizontalDivider(Modifier.padding(top = 16.dp))
         TextButton(onClick = { deleting = true }) { Text("Delete bot", color = MaterialTheme.colorScheme.error) }
     }
+    if (deleting) Overlaid()
     if (deleting) AlertDialog(
         onDismissRequest = { deleting = false },
         title = { Text("Delete ${b.name}?") },