Repository navigation
spec(t27f): petal J JOBS -- job list, timeline and badge from job_kind.t27 - #12303
Conversation
…d.t27 (Closes #12302, Refs #12173) Petal J (row 9 of petal_viz_plan.t27) answers: which lab jobs are queued, running or done, and of what kind? specs/t27f/petal_jobs_viz.t27 shows six lab jobs. The views read one VizState: a list (gate, class, state now), a timeline (one cell per job and tick) and a badge (queued, running and done counts plus the truth label). Gate words, classes, offers and next moves come from job_kind.t27 (ljk_gate_word, ljk_gate_class, ljk_node_takes, ljk_offer, ljk_next) and the agreement verdict from proof.t27 job_verdict. job_kind keeps no state table, so the states are derived, never stored: - QUEUED while ljk_offer does not place the job or before its lease tick; - RUNNING while ljk_next says WAIT or RETRY; - DONE once ljk_next says ADMIT or VOID. The receipt arrivals and lease ticks are a recorded petal-side fixture; the header says so. The inputs are the tick (stepper) and the node scenario (param). A scenario other than the recorded one is a what-if, so the badge reads DEMO; the recorded scenario returns VERIFIED. pjv_reps equals pvp_reps(9) = 772, and viz_plan_ok holds. test-report: 34 of 34 pass, 0 vacuous, 1 invariant. dupe_scan: no new duplicate body. The plan is not edited. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Summary by t27-beesChecked by the t27 compilert27c parse, parse-complete and typecheck on each changed .t27 file at
Read by the modelThis PR adds a new visualization petal ( Worth a look
Read: 1 files, +1710 -0, the whole diff up to 60000 characters (the rest was not read). Head |
Closes #12302
Refs #12173
What
Petal J JOBS, row 9 of
specs/t27f/petal_viz_plan.t27. It answers: "Which lab jobs are queued, running or done, and of what kind?"One new file,
specs/t27f/petal_jobs_viz.t27. It is written againstviz_contract.t27in the order of the reference petal S and followsdocs/nona-03-manifest/VIZ-PETAL-GUIDE.md(#12282).Source, not copies. The rules come from two specs:
job_kind:ljk_gate_word,ljk_gate_classljk_node_takes,ljk_offerljk_next(ADMIT, VOID, WAIT, RETRY)proof:job_verdict,wanted_afterljk_sample_desktop,ljk_sample_laptop,ljk_sample_phoneViews. A job list, a timeline (one cell per job and tick) and a badge with queued, running and done counts, all over one
VizState. Every event goes throughviz_apply.Inputs. The tick (stepper) and the node scenario (param: recorded, laptops on battery, phones on battery).
Plan.
pjv_reps()equalspvp_reps(9)= 772, andviz_plan_okholds. The plan is not edited.Glue the petal owns, called out
job_kind.t27has no queued, running or done table, so the petal derives each state and never stores it:ljk_offerdoes not place the job, or before its lease tick;ljk_nextsays WAIT or RETRY;job_kindkeeps no receipt log, so the receipt arrivals (PJV_VOTES,PJV_TOP,PJV_SECOND) and the lease ticks (PJV_START) are a recorded fixture in the petal. The rules applied to them are the source's; the header says so.Checks
t27c test-report specs/t27f/petal_jobs_viz.t27 --specs-dir specs: 34 tests, 34 pass, 0 fail, 0 vacuous, 1 invariant.python3 tools/dupe_scan.py: no new duplicate body.🤖 Generated with Claude Code