Merge branch 'worktree-agent-a26b9a22ff124dd1a' into dev-loop
This commit is contained in:
commit
122ca45ebd
34
NEXT.md
34
NEXT.md
@ -151,18 +151,23 @@ path is hand-written and header-checked, not left to the opt-in `FLAN_RAYLIB_H`
|
||||
has no `FLAN_RAYLIB_H` and still has to draw. An enum value has to be added by hand whatever happens — the importer
|
||||
generates functions and only functions.
|
||||
|
||||
### Still not started: frame rollback, `PORTING.md` Tier 1 item 6
|
||||
### Landed: frame rollback, `PORTING.md` Tier 1 item 6
|
||||
|
||||
The last item on that list, and the only one of Tier 1 that has not moved. Not a language feature: `restart-case`,
|
||||
struct assignment and fixed-arrays-as-values are all built. What is missing is the worked example —
|
||||
`snapshot`/`restore` callbacks beside the `continue` restart, the way `sand.flan` is the worked example for the
|
||||
loop — plus a headless case on the `dune test` path. `bounds-condition.flan` shows an abandoned frame leaving
|
||||
half-written state behind; this is what finishes that thought, and a bad index has landed in `continue` rather than
|
||||
`exit(134)` since this morning, so it is worth more than it was.
|
||||
`test/programs/frame-rollback.flan`, with three acceptance rows beside `bounds-condition.flan`'s (plain, `-O0`,
|
||||
dev). Nothing was added to the language, which was the premise: `snapshot` is `(set grid-backup grid)` and
|
||||
`(set world-backup world)`, `restore` is the same two the other way, and that is the whole of what `engine.clj`
|
||||
spends an `IntGrid` walk on and `engine.lisp` spends `sb-mop:class-slots` on.
|
||||
|
||||
One thing to get right rather than discover: an *answered* bounds failure runs the function's defers, because it
|
||||
leaves through the same unwind path a `return` does. A restore has to be ordered against them deliberately, and
|
||||
getting it wrong is silent rather than loud.
|
||||
**The ordering against defers was the decision.** Restore lives in the `continue` clause, so it is the last write
|
||||
on the abandoned path and needs no agreement with any defer that ran on the way out. The rejected alternative —
|
||||
restore in a `defer` inside the frame function — is the silent one: a defer runs on the ordinary return path too,
|
||||
so it rolls back the frames that *succeeded*, and nothing reports that as an error. The test pins the ordering with
|
||||
a counter inside the snapshot and a counter outside it rather than in prose, and carries a negative control (the
|
||||
same bad frame, a `continue` that only counts) because "state equals snapshot" passes trivially on a program that
|
||||
wrote nothing.
|
||||
|
||||
One edge left in the file's header comment rather than here: the snapshot covers plain values only. A defer that
|
||||
frees a resource the snapshot holds a pointer to means restore resurrects a dangling one.
|
||||
|
||||
### Landed: sand.flan is the game the other ports are
|
||||
|
||||
@ -300,10 +305,11 @@ Tier 0 is finished, and so is item 5. **The watch for a running program is done*
|
||||
built (a pushed table, the watch buffer, inline ghost text) and the `spy-num` half landed 2026-09-13: a hot-loop slot
|
||||
keeps count/min/max/last/mean, the write path does no formatting, and the window is since the editor's last tick
|
||||
rather than cumulative, which is a deliberate divergence from `watch.clj` argued in `BUILT.md`, "A hot loop keeps
|
||||
five numbers, and the window is the editor's". So of Tier 1 **item 6 is the next one**: **frame rollback as a worked
|
||||
example** — `snapshot`/`restore` callbacks beside the `continue` restart, which is
|
||||
now genuinely reachable from a bad index and so is worth more than it was yesterday. `bounds-condition.flan` shows an
|
||||
abandoned frame leaving half-written state behind; rollback is what finishes that thought.
|
||||
five numbers, and the window is the editor's". **Item 6 landed the same day**:
|
||||
`test/programs/frame-rollback.flan` is the worked example — `snapshot` at the top of the frame, `restore` in the
|
||||
`continue` clause — and `bounds-condition.flan`'s half-written abandoned frame is the thought it finishes. That was
|
||||
the last Tier 1 item anyone was going to move. Items 7 (`drop`), 8 (generics) and 9 (`(read-edn T bytes)`) are still
|
||||
on that list and still deferred with reasons written beside each; none is a blocker for this game.
|
||||
|
||||
**What `PORTING.md` says NOT to build, with evidence:** escaping closures (one capture site, fixed by one parameter),
|
||||
`Handle`/pools, `Result`/`try`, `handler-case`, `loop`/`recur` and tail calls, user allocators, structural typing —
|
||||
|
||||
40
PORTING.md
40
PORTING.md
@ -307,6 +307,13 @@ another name. Two things are missing behind it:
|
||||
arrays are values, so `(set backup grid)` is the whole of `snapshot!` and there is no
|
||||
`sb-mop:class-slots` walk to write. It just has to be written.
|
||||
|
||||
> **Done, 2026-09-13.** Written, in `test/programs/frame-rollback.flan`:
|
||||
> `snapshot` at the top of the frame, `restore` in the `continue` clause,
|
||||
> over one fixed array and one struct — `engine.clj`'s grids plus
|
||||
> `engine.lisp`'s shallow copy of the state object, two `set`s here because
|
||||
> both are values. The ordering against defers is the decision in it, and
|
||||
> item 6 below records it. Three acceptance rows, plain, `-O0` and dev.
|
||||
|
||||
2. **A bounds failure is not a condition.** `runtime/flan_rt.c` `flan_bounds_fail` prints
|
||||
and calls `rt_die`, which is `exit(134)`. No handler runs, no restart is offered, and
|
||||
`lib/dev.ml` answers every subsequent request with "the program exited; restart flan
|
||||
@ -543,11 +550,34 @@ not compete for the same slot.
|
||||
accumulator is reached by the same plain `declare-c` the scalars use, so the `(watch
|
||||
"hp" hp)` form is still unbuilt and still only wanted for composites.
|
||||
|
||||
6. **Frame rollback in the engine pattern.** Not a language feature — the pieces are all
|
||||
there (`restart-case`, struct assignment, fixed arrays as values). What is missing is
|
||||
the worked example showing `snapshot`/`restore` callbacks alongside the `continue`
|
||||
restart, the way `sand.flan` is the worked example for the loop. A page of code and a
|
||||
test program, and the "never restarting" claim gets materially stronger.
|
||||
6. ~~**Frame rollback in the engine pattern.**~~ **Done, 2026-09-13.** Not a language
|
||||
feature and nothing was added to the language: `test/programs/frame-rollback.flan` is
|
||||
the worked example, `snapshot` at the top of the frame and `restore` in the `continue`
|
||||
clause, over one fixed array and one struct. Two `set`s each way. That is the whole
|
||||
claim about values — `engine.clj` walks every `IntGrid` and `engine.lisp` walks
|
||||
`sb-mop:class-slots`, and here there is nothing to walk.
|
||||
|
||||
**The ordering against defers was the decision, and both orderings compile.** An
|
||||
*answered* bounds failure runs the abandoned function's defers, innermost-first,
|
||||
**before** the restart clause body starts (item 4 above, `spec-conditions.md` §5). So:
|
||||
|
||||
- **`restore` in the `continue` clause** — chosen. It is the last write on the
|
||||
abandoned path and therefore needs no agreement with what any defer did on the way
|
||||
out. A defer that writes into the snapshotted state is simply overwritten, which is
|
||||
what "the frame did not happen" means.
|
||||
- `restore` in a `defer` inside the frame function — rejected, **and it is the silent
|
||||
one**. A defer runs on the ordinary return path too, so that version rolls back the
|
||||
frames that *succeeded*. Nothing errors; the game stops advancing.
|
||||
|
||||
The test pins the ordering with two numbers rather than asserting it in prose: a
|
||||
counter inside the snapshot, written by the frame's defer, reads its pre-frame value,
|
||||
while a counter outside the snapshot proves the defer ran. And there is a negative
|
||||
control — the same bad frame with a `continue` that only counts — because "state
|
||||
equals snapshot" passes trivially on a program that wrote nothing.
|
||||
|
||||
One edge worth carrying: **the snapshot covers plain values only.** If a defer frees a
|
||||
resource and the snapshot holds a pointer or handle to it, restore resurrects a
|
||||
dangling one. Value state in the snapshot, resources in the defers, no overlap.
|
||||
|
||||
7. **`drop`, or recursive teardown.** Unblocks `(Vec T)` where `T` owns a `Vec`, which is
|
||||
`game.lisp`'s tileset shape exactly. Fixed arrays sidestep it at this size, so this is
|
||||
|
||||
207
test/programs/frame-rollback.flan
Normal file
207
test/programs/frame-rollback.flan
Normal file
@ -0,0 +1,207 @@
|
||||
;;;; Frame rollback: the half of the frame loop that `continue` does not do.
|
||||
;;;;
|
||||
;;;; PORTING.md Tier 1 item 6. Not a language feature — restart-case, struct
|
||||
;;;; assignment and fixed-arrays-as-values are all built. This is the worked
|
||||
;;;; example, the way sand.flan is the worked example for the loop itself.
|
||||
;;;;
|
||||
;;;; Both reference hosts survive a bad frame and keep the window open, and
|
||||
;;;; both do it the same way underneath: engine.clj's `run-game!` snapshots
|
||||
;;;; every IntGrid at the top of the frame, catches Throwable and restores;
|
||||
;;;; engine.lisp's `run-frame` wraps update and draw in a restart-case whose
|
||||
;;;; `retry-frame`, `skip-frame` and `reinit` each roll the grids *and* a MOP
|
||||
;;;; shallow copy of the state object back. Flan already had the restart-case
|
||||
;;;; and, since a bad index signals BoundsError rather than calling exit(134),
|
||||
;;;; already lands in `continue` instead of ending the session. What it did
|
||||
;;;; not have was the rollback — so an abandoned frame left the grid
|
||||
;;;; half-written, which is bounds-condition.flan's last line (`10 99 12 13`)
|
||||
;;;; read as a bug rather than as a result.
|
||||
;;;;
|
||||
;;;; **A restart is not a transaction** (spec-conditions.md §5). A transfer
|
||||
;;;; runs defers and moves control; it does not undo. Nothing here is a
|
||||
;;;; mechanism the compiler provides, and that is the point: rollback is a
|
||||
;;;; discipline the author writes, and in Flan it is two lines, because a
|
||||
;;;; fixed array and a struct are values. `(set backup grid)` is the whole of
|
||||
;;;; snapshot! — no walk, no sb-mop:class-slots, no per-cell copy loop.
|
||||
;;;;
|
||||
;;;; ── The ordering decision, which is the reason to read this file ──
|
||||
;;;;
|
||||
;;;; An *answered* bounds failure runs the abandoned function's defers, because
|
||||
;;;; it leaves through the same unwind path a `return` does, and those defers
|
||||
;;;; run innermost-first **before** the restart clause body starts. So a
|
||||
;;;; snapshot has to be ordered against them deliberately, and both orderings
|
||||
;;;; compile:
|
||||
;;;;
|
||||
;;;; - **restore in the restart clause** — chosen. It is the last write on
|
||||
;;;; the abandoned path, so it needs no agreement with what any defer did
|
||||
;;;; on the way out. A defer that writes into the snapshotted state is
|
||||
;;;; simply overwritten, which is what "the frame did not happen" means.
|
||||
;;;; - restore in a `defer` inside the frame function — **rejected, and it is
|
||||
;;;; the silent one.** A defer runs on the ordinary return path too, so
|
||||
;;;; that version rolls back the frames that *succeeded*. Nothing errors;
|
||||
;;;; the game just stops advancing.
|
||||
;;;;
|
||||
;;;; `tick` below is the discriminator. It is written by update-frame's defer,
|
||||
;;;; it lives inside the snapshot, and after an abandoned frame it reads as its
|
||||
;;;; pre-frame value while `tails` — which lives outside the snapshot — proves
|
||||
;;;; the defer ran. Only the chosen ordering produces that pair.
|
||||
;;;;
|
||||
;;;; **The snapshot covers plain values only.** If a defer frees a resource and
|
||||
;;;; the snapshot holds a pointer or a handle to it, restore resurrects a
|
||||
;;;; dangling one. Value state in the snapshot, resources in the defers, and
|
||||
;;;; no overlap between them.
|
||||
;;;;
|
||||
;;;; ── What is asserted ──
|
||||
;;;;
|
||||
;;;; Frame 2 is the negative control and it is what makes frame 3 mean
|
||||
;;;; anything: the same bad frame, the same snapshot taken, and a `continue`
|
||||
;;;; clause that only counts. It leaves drift 3. Frame 3 restores and leaves
|
||||
;;;; drift 0. Without the control, "state equals snapshot" would pass on a
|
||||
;;;; program that never wrote anything and never restored anything.
|
||||
|
||||
;;; The state the engine owns: one grid of cells, and one struct of scalars.
|
||||
;;; Two shapes on purpose — engine.clj rolls back grids, engine.lisp rolls
|
||||
;;; back grids *and* a copy of the state object, and in Flan each is one `set`.
|
||||
(defstruct World [placed i32 brush i32])
|
||||
|
||||
(defvar grid [8 i32])
|
||||
(defvar world World)
|
||||
|
||||
;;; The snapshot. Same types, same declarations; there is nothing else to it.
|
||||
(defvar grid-backup [8 i32])
|
||||
(defvar world-backup World)
|
||||
|
||||
;;; Evidence, and it has to live *outside* the snapshot or restore rolls back
|
||||
;;; the proof along with the state. `writes` counts the mutations a frame made
|
||||
;;; before it failed, `tails` counts the defers that ran on the way out.
|
||||
(defvar frames i64)
|
||||
(defvar skipped i64)
|
||||
(defvar writes i64)
|
||||
(defvar tails i64)
|
||||
|
||||
;;; Handlers cannot see the locals of the function that established them —
|
||||
;;; check.ml refuses a capture by name and says to use a global — so the
|
||||
;;; condition's numbers land up here too.
|
||||
(defvar low i64)
|
||||
(defvar length i64)
|
||||
|
||||
;;; ── snapshot and restore ──────────────────────────────────────────────
|
||||
;;; The whole of it. A fixed array copies on assignment and so does a struct
|
||||
;;; (values.flan), so these are two stores each and the cost is the size of
|
||||
;;; the state, not the shape of it.
|
||||
|
||||
(defn snapshot [] ()
|
||||
(set grid-backup grid)
|
||||
(set world-backup world))
|
||||
|
||||
(defn restore [] ()
|
||||
(set grid grid-backup)
|
||||
(set world world-backup))
|
||||
|
||||
;;; How far the live state has drifted from the snapshot: the assertion this
|
||||
;;; program exists to make. Counted rather than compared with `=`, because
|
||||
;;; `=` is numeric and enum only — there is no structural equality in the
|
||||
;;; surface language, and a hand-written walk is what a game would write too.
|
||||
(defn drift [] i64
|
||||
(let [d (i64 0)]
|
||||
(dotimes [i 8]
|
||||
(when (!= (at grid i) (at grid-backup i)) (set d (+ d 1))))
|
||||
(when (!= (.placed world) (.placed world-backup)) (set d (+ d 1)))
|
||||
(when (!= (.brush world) (.brush world-backup)) (set d (+ d 1)))
|
||||
d))
|
||||
|
||||
(defn show [name string n i64] ()
|
||||
(print name) (print " ") (print n) (println ""))
|
||||
|
||||
(defn dump [] ()
|
||||
(print (at grid 0)) (print " ") (print (at grid 3)) (print " ")
|
||||
(print (at grid 7)) (print " ") (print (.placed world)) (println ""))
|
||||
|
||||
;;; ── the frame ─────────────────────────────────────────────────────────
|
||||
|
||||
;;; The engine's tail write. It runs on every exit path — the good one and the
|
||||
;;; abandoned one — and it writes into the snapshotted state deliberately, so
|
||||
;;; that cell 7 discriminates the two orderings. `tails` does not, which is why
|
||||
;;; it is a separate counter.
|
||||
(defn tick [] ()
|
||||
(set (at grid 7) (+ (at grid 7) 1))
|
||||
(set tails (+ tails 1)))
|
||||
|
||||
;;; Mutate first, fail second: the half-written frame this whole file is about.
|
||||
;;; `col` is a mouse column in the real thing — game.clj computes it straight
|
||||
;;; from the pointer with no check anywhere, which is how an ordinary session
|
||||
;;; walks into this by moving one pixel outside the window.
|
||||
(defn update-frame [col i32] ()
|
||||
(defer (tick))
|
||||
(set (.placed world) (+ (.placed world) 1))
|
||||
(set (at grid 0) (+ (at grid 0) 1))
|
||||
(set writes (+ writes 1))
|
||||
(set (at grid col) 5))
|
||||
|
||||
;;; The frame loop, without the rollback. sand.flan's shape exactly, and the
|
||||
;;; negative control: the snapshot is taken and then ignored.
|
||||
(defn frame-no-rollback [col i32] ()
|
||||
(snapshot)
|
||||
(restart-case
|
||||
(do (update-frame col)
|
||||
(set frames (+ frames 1)))
|
||||
(continue [] (set skipped (+ skipped 1)))))
|
||||
|
||||
;;; And with it. One line more, in one place, and it is the *last* thing on the
|
||||
;;; abandoned path rather than the first.
|
||||
(defn frame [col i32] ()
|
||||
(snapshot)
|
||||
(restart-case
|
||||
(do (update-frame col)
|
||||
(set frames (+ frames 1)))
|
||||
(continue [] (restore)
|
||||
(set skipped (+ skipped 1)))))
|
||||
|
||||
(defn main [] i32
|
||||
(set (.brush world) 1)
|
||||
|
||||
(handler-bind
|
||||
[(BoundsError [c]
|
||||
(set low (.low c))
|
||||
(set length (.length c))
|
||||
;; Abandon the frame. The transfer crosses update-frame, running its
|
||||
;; defer, and lands in the clause of the restart-case one frame out.
|
||||
(invoke-restart 'continue))]
|
||||
|
||||
;; Frame 1: in bounds. The handler never runs, the frame finishes, and the
|
||||
;; defer runs on the ordinary return path — which is exactly why restore
|
||||
;; must not live in a defer: this frame's work has to survive.
|
||||
(frame 3)
|
||||
(dump) ; 1 5 1 1
|
||||
(show "drift" (drift)) ; 1 5 1 1 vs the zeroed snapshot: 4
|
||||
|
||||
;; Frame 2: out of bounds, and nothing rolls back. The frame is abandoned
|
||||
;; and the session survives — that much `continue` already gave us — but
|
||||
;; the state is the frame's leftovers: cell 0 bumped, placed bumped, the
|
||||
;; defer's tick landed, and the write that failed never happened.
|
||||
(frame-no-rollback 9)
|
||||
(dump) ; 2 5 2 2
|
||||
(show "drift" (drift)) ; 3 — and this is the bug
|
||||
|
||||
;; Frame 3: the same bad index, the same snapshot, restore in the clause.
|
||||
(frame 9)
|
||||
(dump) ; 2 5 2 2 — frame 2's state, intact
|
||||
(show "drift" (drift)) ; 0
|
||||
|
||||
;; The ordering, in two numbers. `tails` is 3, so update-frame's defer ran
|
||||
;; on the abandoned path as well as the good one; cell 7 is back at 2, so
|
||||
;; the restore happened *after* it. Had restore run first — in a defer
|
||||
;; registered *below* `(defer (tick))`, since defers run innermost-first
|
||||
;; and the later registration is the inner one — cell 7 would read 3 and
|
||||
;; drift above would have read 1, which is the quiet kind of wrong.
|
||||
(show "tails" tails) ; 3
|
||||
(show "tick" (i64 (at grid 7))) ; 2
|
||||
|
||||
;; Three frames, two of them bad; one finished, two were abandoned; three
|
||||
;; mutations were made before the failures, of which only frame 1's
|
||||
;; survives. And the condition carried the real numbers both times.
|
||||
(show "frames" frames) ; 1
|
||||
(show "skipped" skipped) ; 2
|
||||
(show "writes" writes) ; 3
|
||||
(show "low" low) ; 9
|
||||
(show "length" length)) ; 8
|
||||
0)
|
||||
@ -1237,6 +1237,46 @@ let () =
|
||||
outputs ~dev:true "a bad index is a condition, dev"
|
||||
"programs/bounds-condition.flan" bounds_cond_out;
|
||||
|
||||
(* And the half that finishes that thought. bounds-condition.flan's last
|
||||
line is `10 99 12 13` — an abandoned frame's leftovers — and a restart
|
||||
undoes none of it, because a restart is not a transaction
|
||||
(spec-conditions.md §5). So rollback is written rather than provided,
|
||||
and frame-rollback.flan is the worked example: snapshot at the top of
|
||||
the frame, restore in the `continue` clause, over one fixed array and
|
||||
one struct, which is engine.clj's grids plus engine.lisp's shallow copy
|
||||
of the state object and is two `set`s here because both are values.
|
||||
|
||||
The rows to read are the three drifts. Frame 1 is in bounds and leaves
|
||||
drift 4 against a zeroed snapshot — work that must survive. Frame 2 is
|
||||
the negative control: the same bad index, the same snapshot taken, and
|
||||
a `continue` that only counts, leaving drift 3. Without it "state equals
|
||||
snapshot" would pass on a program that wrote nothing. Frame 3 restores
|
||||
and leaves drift 0.
|
||||
|
||||
`tails 3` and `tick 2` are the ordering, and they are the pair no other
|
||||
ordering produces. An answered bounds failure runs the abandoned
|
||||
function's defers — innermost-first, before the clause body — so
|
||||
update-frame's defer ran on all three frames (tails 3) and wrote into
|
||||
the snapshotted cell 7, and cell 7 still reads its pre-frame 2 because
|
||||
restore is the last write on that path. Restore in a defer instead
|
||||
would read tick 3 here, and would also roll back frame 1, which nothing
|
||||
reports as an error.
|
||||
|
||||
Three rows for the reason the bounds rows above have three: -O0 pins
|
||||
that the transfer does not depend on optimisation, and the dev build
|
||||
pins that a call through a cell and a shadow-stack frame per call does
|
||||
not change where it lands. *)
|
||||
let rollback_out =
|
||||
"1 5 1 1\ndrift 4\n2 5 2 2\ndrift 3\n2 5 2 2\ndrift 0\n\
|
||||
tails 3\ntick 2\nframes 1\nskipped 2\nwrites 3\nlow 9\nlength 8\n"
|
||||
in
|
||||
outputs "an abandoned frame rolls back" "programs/frame-rollback.flan"
|
||||
rollback_out;
|
||||
outputs ~opt:"-O0" "an abandoned frame rolls back, -O0"
|
||||
"programs/frame-rollback.flan" rollback_out;
|
||||
outputs ~dev:true "an abandoned frame rolls back, dev"
|
||||
"programs/frame-rollback.flan" rollback_out;
|
||||
|
||||
(* ── Packages: the link follows the program ────────────────────────
|
||||
A package's C and linker arguments used to come with the import,
|
||||
whatever [main] did — which is what made sand's two halves two files
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user