C-u before an eval marks a form so the program stops when it runs (DISCUSS.md 9). The mark arrives as a position in a separate :pause field and is applied to the Ast after parsing: splicing text into the source would move every line and column after it, and the error overlays, the layout, the break loop's frame locations and DWARF all read those. Ast.mark_pause puts a (pause) call at whatever starts at that position -- wrapping a sub-expression in a do, or going to the front of a defn's body, since a declaration cannot be wrapped. A position that matches nothing is refused rather than installed unmarked, which would report a breakpoint that is not there. It sticks with no extra state: the marked declaration is what goes into the session, so an ordinary C-c C-c over the same form clears it. The daemon half only; the Emacs command and its overlay are not built. HANDOFF-f2.md has the rest, in order.
143 lines
9.7 KiB
Markdown
143 lines
9.7 KiB
Markdown
# Handoff: `pause` marking from Emacs (DISCUSS.md §9)
|
||
|
||
The daemon half is built and works end to end over the wire. The Emacs half is **not** built.
|
||
Nothing half-written was left behind: `dune build` is clean and there is no new test.
|
||
|
||
## The design, as it stands after reading the code
|
||
|
||
`C-u` before an eval marks a form so the program stops when that form runs. The mark is **not**
|
||
spliced into the source text — that would move every line and column after the insertion, and the
|
||
error overlays, `layout`, the break loop's frame locations and DWARF all read those. Instead the
|
||
editor sends a **position** beside the code:
|
||
|
||
```
|
||
(:op "eval" :code "(defn step [] i64 ...)" :file "/x/y.flan" :pause (LINE COL))
|
||
```
|
||
|
||
The daemon parses and `Load`s as usual, then walks the resulting `Ast.decl list` and puts a
|
||
`(pause)` call at whatever *starts* at that position. `(pause)` is an ordinary prelude function
|
||
(`error` under a `restart-case` with a `continue` clause), so an instrumented body is just a body
|
||
that calls one more function, and the break loop it lands in is the one an unhandled condition
|
||
already builds. Nothing in the compiler changes.
|
||
|
||
It **sticks** with no extra machinery: the marked declaration is what goes into `Session.t.decls`,
|
||
so it stays marked until an evaluation replaces it — an ordinary `C-c C-c` over the same form with
|
||
no `:pause`, or `C-c C-k` over the buffer. That is §9's settled behaviour and it costs one
|
||
statement that was already there.
|
||
|
||
### What §9 left out or got slightly wrong
|
||
|
||
- **§9 says "send the top-level form with that span replaced by `(do (pause) <span>)`".** That
|
||
wrapping is right for a sub-expression but *impossible* for the first of its three targets: a
|
||
whole top-level `defn` is a declaration, and `(do (pause) (defn ...))` is not an expression.
|
||
Marking a whole `defn` therefore means *stopping on entry*, and the call goes at the front of
|
||
`fbody`. `Ast.mark_pause` does both, chosen by what the position lands on.
|
||
- **§9 does not say the mark can be refused.** It has to be: a position that matches nothing must
|
||
be an error, because installing an unmarked body and answering `ok` reports a breakpoint that is
|
||
not there — the silent-success failure the session refuses everywhere else.
|
||
- **Desugaring makes locations non-unique.** `parse.ml` gives several nested nodes the same
|
||
location (`when` becomes an `If` whose branch is a `Do` at the `when`'s own position — lines 141,
|
||
164, 651, 654). The walk is pre-order and stops at the first hit, so the outermost node at that
|
||
position wins, which is the one the editor pointed at.
|
||
- **The third target ("the form point is inside") needs no new daemon work** — it is the same
|
||
position field, computed differently in Emacs.
|
||
|
||
## What was built, file by file
|
||
|
||
All four are **working** (built, and exercised against a real daemon and a real running program by
|
||
hand — see "How it was checked").
|
||
|
||
- **`lib/ast.ml`** — new section at the end:
|
||
- `map_children : (expr -> expr) -> expr -> expr`, an exhaustive one-level rebuild. Exhaustive on
|
||
purpose: a missing constructor is a form you silently cannot stop inside.
|
||
- `pause_call : Loc.t -> expr` — `(pause)` at a given location.
|
||
- `mark_pause : line:int -> col:int -> decl list -> decl list option` — pre-order, first hit wins,
|
||
`None` when nothing is at that position. The synthesized `Do`/`Call` take the target's own
|
||
location, never `Loc.unknown`, because DWARF and the break loop's frame location read it.
|
||
- **`lib/wire.ml`** — `pos_field form key`, reading `(LINE COL)` as a pair of ints; `None` for
|
||
anything else, the same narrowness as `int_field`.
|
||
- **`lib/session.ml`** — `eval` takes `?pause:(int * int)`. It is applied **after**
|
||
`Load.qualify_decl`, so a package that defines a `pause` of its own cannot capture the
|
||
synthesized call, and a position that matches nothing is a `Loc.fail` naming the position.
|
||
- **`lib/dev.ml`** — `eval` takes `~pause`, `handle` reads `:pause` off the request, and a
|
||
successful install echoes `:pause "LINE:COL"` back so an editor marks the buffer only for a mark
|
||
the session actually applied. With no `:pause` in the request, every byte of the old behaviour is
|
||
unchanged.
|
||
|
||
## How it was checked
|
||
|
||
A daemon over `test/programs/dev-loop.flan`, driven by a raw socket client:
|
||
|
||
- eval of `step` with `:pause (1 1)` → `(:status "ok" … :pause "1:1")`, and a later `describe`
|
||
came back `:stopped t :condition "Pause"` — the program stopped, on the prelude's own condition.
|
||
- `:pause (1 999)` → `(:status "error" :message "nothing to pause at line 1, column 999 of the form
|
||
sent")`.
|
||
- a plain re-eval of the same form → accepted.
|
||
|
||
`dune build` is clean. **`dune test` was not run** (budget). The changes are additive: the new
|
||
session argument is optional and the new reply field only appears when `:pause` was sent, so no
|
||
existing path changes shape — but the suite should be run first thing next session anyway. Note
|
||
`test_dev.ml`'s first block is separately known-flaky (a socket bind race, ~1 in 4).
|
||
|
||
## What remains, in order
|
||
|
||
1. **`lib/dev.ml`, `eval_expr`** — accept `:pause` for `C-u C-x C-e` (§9's "last expression").
|
||
Two parts. (a) `lib/session.ml`'s `eval_expr` should take `?(pause = false)` and wrap
|
||
`Parse.expr form` in `Do [Ast.pause_call loc; e]` before `Check.expression`. (b) `eval_expr`'s
|
||
`wait` loop in `dev.ml` returns `error "the program did not reach a frame boundary…"` after 5s,
|
||
which is exactly what a thunk that stopped in the break loop will do — so it would report the
|
||
working feature as a failure. Make `wait` three-way (`` `Value | `Stopped | `Timeout ``) and
|
||
check `state t = Stopped` **only when a pause was requested**: `test_dev.ml:519–560` already
|
||
asserts the current timeout shape for the no-pause case (`"an expression that stopped inside a
|
||
break answered anyway"`), and that must stay byte-identical.
|
||
Use `:pause t` here, not `(LINE COL)`: `flan-eval-last-sexp` sends a raw `buffer-substring`
|
||
with no line padding (unlike `flan-dev--text`), so buffer coordinates do not survive that path.
|
||
2. **`emacs/flan-dev.el`, `flan-dev--eval`** — take an optional pause position and put
|
||
`:pause (LINE COL)` on the request. The column is a **1-based byte offset**, per the comment
|
||
above `flan-dev--position`: `(1+ (- (position-bytes pos) (position-bytes (line-beginning-position))))`,
|
||
*not* `current-column`. The line is the buffer's own line, which already works because
|
||
`flan-dev--text` pads with leading newlines.
|
||
3. **`emacs/flan-dev.el`, `flan-eval-defun`** — `(interactive "P")`. `C-u` marks the innermost form
|
||
point is inside (`backward-up-list`, falling back to the defun's start when point is not nested);
|
||
`C-u C-u` marks the top-level form itself, i.e. stop on entry. That plus item 1 covers §9's three
|
||
targets with no new keybinding — `emacs/flan-mode.el` needs no change.
|
||
4. **`emacs/flan-dev.el`, the visual indication** — a `flan-dev-pause-face` overlay over the marked
|
||
form's bounds, drawn **only** when the reply carries `:pause`, tagged with a `flan-dev-pause`
|
||
property. Copy the shape of the error overlays (`flan-dev--show-error`) but *not* their lifetime:
|
||
a pause mark is an annotation on the program, not feedback about one command, so it must survive
|
||
`pre-command-hook`. Remove overlays intersecting the sent region on every accepted plain eval,
|
||
and over the whole buffer in `flan-eval-buffer` — that is the visible half of "cleared by an
|
||
ordinary `C-c C-c`".
|
||
5. **`test/programs/dev-pause.flan`** — new, shaped like `dev-break.flan`'s tail so the marked
|
||
function keeps being called: `(dotimes [i 4000] (agent/wait 5) (set ticks (step)))`.
|
||
`dev-loop.flan` calls `step` only four times, which is too tight.
|
||
6. **`test/test_dev.ml`** — a block in the style of the break-loop block (its own daemon, its own
|
||
program, its own output buffer). Assert both halves: mark `step`'s `(+ ticks 1)` sub-expression
|
||
→ await `:stopped t` with a condition containing `Pause` → `break` lists `continue` → then
|
||
**re-eval `step` plainly, take `continue`, and confirm it runs on without stopping again**. The
|
||
second assertion is the one that tests the settled "it sticks until evaluated plainly" decision
|
||
and the one most likely to be skipped.
|
||
7. **`emacs/test-flan-dev.el`** — the elisp side, once items 2–4 exist.
|
||
|
||
## Decisions made that were not already settled
|
||
|
||
- **The mark is not a field on `Ast`.** It is an ordinary `(pause)` call spliced into the tree. A
|
||
`paused : bool` on `Ast.expr` would have to be threaded through `Check`, `Tast` and `Emit` for a
|
||
feature the prelude already implements as a function.
|
||
- **No parallel `paused` list on `Session.t`.** The spliced declaration in `t.decls` *is* the state
|
||
that makes the mark stick; a second `(name * position) list` would be a second source of truth
|
||
that drifts the first time some path replaces `decls` without touching it. Clearing then falls out
|
||
for free — any plain eval replaces the stored declaration with an unmarked one.
|
||
- **Marking a whole `defn` means stopping on entry**, since it cannot be wrapped (above).
|
||
- **A position matching nothing is refused**, rather than installed unmarked (above).
|
||
- **The splice happens after qualification**, so a package's own `pause` cannot capture it.
|
||
- **The reply echoes `:pause "LINE:COL"`** so the editor draws its overlay off the daemon's
|
||
confirmation and can never claim a mark that was refused.
|
||
|
||
## Tried and abandoned
|
||
|
||
- Nothing failed outright. Worth recording: the worktree this was done in was created **485 commits
|
||
behind** `dev-loop` (at `2c232dd`, before `lib/dev.ml` existed at all) and had to be
|
||
`git reset --hard` to the branch tip before any of the files named in the task existed. Check
|
||
`git log` against `dev-loop` before starting in a fresh worktree.
|