[v0.4] Release program: general formal programming, verified production compilation, and models/reasoning #15

Activity

1. humuhumu33

   added this to the LexLean v0.4 milestone on Oct 13, 2026
2. humuhumu33

   added this to LexLeanon Oct 13, 2026
3. github-project-automation

   moved this to Todo in LexLeanon Oct 13, 2026
4. afflom commented on Oct 15, 2026

   

   afflom

   on Oct 15, 2026 – with Claude

   MemberAuthor

   More actions

   The completion plan for the 0.5.0 release, which continues this program, is #106.

   ---

   Generated by Claude Code
5. afflom commented on Oct 17, 2026

   

   afflom

   on Oct 17, 2026 – with Claude

   MemberAuthor

   More actions

   v0.4 status, 2026-10-17 03:00Z, from the maintainer. main is c3905e7c (register 393). Landed since the last update: #158 (integer order and fold laws, #117), #146 (certificate E as data, #89 stage 1), #159 (bdd as parts of one run, #131), #153 (stdlib member 1, #92). Main's push runs on 097b9b97 and ccd37ec7 are green; the one on c3905e7c is running.

   Open v0.4 issues and what stands between each and close

   Issue	State	Owner	Next
   #89 certificates as data	stage 1 merged; stage 3 (A) draft #157, text generator deleted on the branch; stage 2 (B) branch claude/issue-89-certificate-b, no new library lemmas needed; stage 4 (audit module and the no-Lean-template gate) not started	contributor sessions for 2 and 3, maintainer for 4	A and B land, then stage 4 (the gate cannot be armed while a template remains)
   #91 runtime generated from the calculus	stage 1 merged; stage 2 part 1 is #155 (derived rows by Lean's reserved-name actions), needs main merged	@humuhumu33	scalar items, the Item proofs, stage 3 (loop, memory model), stage 4; a second session for the package-scaffolding slice is proposed on #91 and not answered
   #92 compiler authored in LexLean	stdlib member 1 merged (#153); pilot (axiom-output parser, BS-01) is #160, ready, CI running; source packages (#161, PR #162, draft) is the missing mechanism for a project to import the stdlib; the effects boundary waits on #91 stage 4	@humuhumu33 for stdlib, contributor sessions for the pilot and packages, maintainer for the boundary	#160 and #162 land; then more stdlib members, then compiler components under differential
   #30 language models	slice 1 (tokenizers, LM-01..LM-03, LM-13) is #82, CI running, moves the language-1.2 identity; context windows, generators, classifiers, adapters, composition follow	@humuhumu33	#82 lands, then the next slices
   #32 model/reasoning stdlib and PrismPM application	blocked on #30 and on #161 (its DoD needs locked packages)	none yet	after those
   #105 collection templates as loops	step 1 merged; steps 2 and 3b wait on #91 stage 3's loop	@humuhumu33	after #91 stage 3
   #149 refuse the data form under 1.2	last: every data form must be migrated first	maintainer	after #89, #91
   #33, #34, #15	close last: the vv extensions, the closure examples and documentation, the release	maintainer	after everything above

   What limits the pace. Each landing is two hours of CI, and every PR that moves the language-1.2 identity (#82, #162, later #91 stage 2 and 3) makes every other PR with 1.2 records regenerate once. The org has 20 concurrent runner jobs, shared across repositories. The rules in force: a PR merges on a green head that contains main and carries a review from someone other than its author (the maintainer records one for sessions' PRs, and approves hh's formally); contributors push a draft PR at most about every 90 minutes; #159's bdd parts took the rest leg from 111 to 23 minutes, so the longest path of a ready run is now the Atlas side.

   Not in the v0.4 path. #150 (#118), #151 (#114), #68 stay open as v0.5 or stale; I carry them after the wave above.

   ---

   Generated by Claude Code
6. afflom commented on Oct 17, 2026

   

   afflom

   on Oct 17, 2026 – with Claude

   MemberAuthor

   More actions

   v0.4 status, 2026-10-17 10:10Z, from the maintainer. main is ea0a4eda (register 402). Since the 03:05Z update: #82 (tokenizers, slice 1 of #30: LM-01..LM-03, LM-13), #160 (the axiom-output parser as a certified production root, BS-01, step 4 of #92) and #162 (source packages, PK-01..PK-04, most of #161) are merged, each on a green head that contained main, with a review recorded; the main push runs on c3905e7c, d22266b3 and 8a844674 are green (the one on ea0a4eda is next). Earlier today: #158, #146, #159, #153.

   Issue	State now	Next
   #89 certificates as data	stage 1 merged (E). Stage 3 (A, #157): the text generator is deleted on its branch; it is merging main and regenerating after #162. Stage 2 (B, #163, draft): all 76 certificates built as data and isDefEq-equal, no library growth; it follows A. Stage 4 (audit module and the gate) is mine, after both	A ready, then B, then stage 4
   #91 runtime from the calculus	stage 1 merged; stage 2 part 1 is #155 (hh): green on its head (26 of 26), needs main merged once more because #162 landed	hh merges main and regenerates; then scalar items, stage 3, stage 4
   #92 compiler in LexLean	stdlib member 1 (#153) and the pilot (#160) merged; PK-05 (the pilot imports the stdlib, the vendored copy deleted) is a small PR from the #161 session, preparing now; the effects boundary waits on #91 stage 4; #164 records a Windows rustc-stack finding from the pilot	PK-05, more stdlib members (hh), then compiler components
   #161 source packages	#162 merged; closes with PK-05	PK-05 PR
   #30 language models	slice 1 merged; context windows, generators, classifiers, adapters, composition follow	hh
   #32	unblocked by #161 once PK-05 lands, still needs #30	after #30
   #105, #149, #33, #34, #15	unchanged: wait on #91 stage 3, the data-form migrations, and everything above	last

   What costs time: every landing is about two hours of CI and every identity move (#82, #162, and #155 next) makes every other PR with language-1.2 records regenerate once. Both contributor sessions on #89 and the #161 session are merging main now; no more identity moves are planned before A and B land except #155's.

   ---

   Generated by Claude Code
7. afflom commented on Oct 17, 2026

   

   afflom

   on Oct 17, 2026 – with Claude

   MemberAuthor

   More actions

   v0.4 status and plan, 2026-10-17 17:00Z, from the maintainer. main is 243f0c73 (register 403: #165 merged, which closes #161). The owner's instruction today: complete the release asap; #68 is completed with the other pull requests and all v0.4 work; #131 (CI cost) is critical. What that changed:

   1. CI cost (#131), decided with the owner: the two-tier gate, #166. A merged PR cost about 1,450 runner-minutes on the 20 shared jobs: about 2.7 runs of about 500 (a draft push already paid the host matrix, examples and every bdd row, about 300) plus a full re-run on main of a tree a PR run had just passed. #166 adds a plan job: a draft runs the rest leg only (about 23 runner-minutes), a ready PR and a push to main run the whole gate, and a push to main that merges a head whose tree it equals, when a PR run of that head passed every job, runs nothing and names the run. Estimated 1,450 to about 600 per merged PR. The draft run of #166 itself already shows the plan on a real runner (plan, then only rest). It lands right after #155 (a CI-only change merged on a verified local merge, announced, backstopped by the push run). Rule for all contributor sessions, from now: keep a PR a draft until its head is final and contains main; mark it ready once; I merge only a head that contains main.

   2. One train instead of five regenerations. Every PR that moves the language-1.2 ID makes every other regenerate (about three hours of writers plus two of CI each). I regenerated #155 on the combined identity myself at hh's request (5a04afd1, 63dd4c08…, register 404); its run is in progress. The identity-moving or record-moving PRs in flight ride in one integration branch, one regeneration, one CI run, after #155 lands: certificate A (#157) and B (#163), #151 (widening conversions, SM-32), #150 (dyadic decoding, MD-13), #68 (explicit byte literals, owner decision), and #91 slice 1 (package scaffolding as generated output, with #105 step 3b; hh agreed on #91). One contributor session each, hand-written work only; #150, #151 are pushed (train/dyadic, train/widening), the others report next. Each PR is still reviewed against its issue's DoD and merged as its commits land.

   Item	State	Next
   #155 (hh, #91 stage 2 part 1)	regenerated and pushed 5a04afd1; full gate running	formal approval, merge on green
   #166 (#131)	draft run proves the plan job; full run next	merge after #155
   #161	closed (PK-05, #165)
   #89	A (#157), B (#163): hand-written parts being finished; stage 4 (audit module and the gate) mine, after both	train
   #92	stdlib member 1, pilot, PK-05 merged; effects boundary waits on #91 stage 4	more stdlib members (hh)
   #91	stage 2 part 1 in flight; slice 1 started by a second session	stages 2 to 4: 7 to 13 serial landings by hh's count (comment on #91), each a regeneration
   #30, #32	slice 1 merged; hh's issue-30-language-model branch holds the next slices	after #30
   #105	step 3b rides with #91 slice 1; steps 2 and 3 after #91 stage 3
   #149, #33, #34, #15	unchanged: last
   #68, #150, #151	owner decision: in v0.4 (milestone set); drafts; in the train

   What bounds the date. Not CI any more, once #166 lands: the #91 chain (7 to 13 serial landings, each a regeneration and a gate run of about 90 minutes if the pool is free, after which #105 and #92's compiler components follow). I will state a date when hh posts the ItemDef measurement and the stage 3 count; I will not guess one. What shortens it: (a) fewer, larger #91 PRs where the proofs allow (hh's low end is 7), (b) trains for everything else, as above, (c) the regeneration as one command, which I will make if a second landing needs it.

   ---

   Generated by Claude Code