refactor(translation): the matcher suite is a proved plan with 32 probes - #310
Merged
Merged
Conversation
flang/translation/run.sh (214 lines of shell) is gone; the same work is now flang/translation/run.fscript, a plan the kernel proves: 15 obligations, all 15 proved, so the shortcut runs without --trust. Nine probes that lived only in the body of PR 298 are written in: five on the list-filter rule and four on the measure-guard allowance. The expectations are measured, not predicted - every one answered exactly what that block said it would, so the suite grew from 23 probes to 32 and all 32 match. What proves the move is right: the 32 triples (name, expected code, required word) were taken by instrument from both files - from run.sh by parsing its probe calls, from the plan by running its probe-table function - and they are identical. Both run green on one tree: 32 probes, zero divergences, code 0. Negative control, three forgeries: a number in the printed C of the traffic light (500 -> 501), one rule cut out of PRINT-RULES.tsv, and a number in the printed C of the declared measure (1.0 -> 2.0). On each one both go red with code 1 and name the same place. Two differences are deliberate and written in the file. A diverged closed list no longer stops the run before the first probe - it becomes complaint number one and the probes still run. A forgery that fails to build now reddens its own probe by name instead of aborting the whole run. CI calls the plan by its shortcut and takes the binary from the shared cache the way its neighbours do, because a plan needs the binary; the forgery probe greps for the plan's complaint line. The counted marks in this workflow follow the shell file that left.
The translation suite moved from shell to a plan, so the numbers it is counted in move with it: one shell file and 214 shell lines less, one file less outside flang. Taken by instrument (inventory:languages for the table, prose-numbers-guard for the marks), not by hand: docs/tree-inventory.md shell row 56 / 9875 -> 55 / 9661, title 193 -> 192 docs/javascript-inventory.md 193 -> 192 .github/workflows/binary.yml shell 50 / 9558 -> 49 / 9344, total 193 -> 192 .github/workflows/ci.yml shell files 50 -> 49 After it: inventory:check code 0, prose-numbers-guard 209 marks of 209 agree. scripts/ledgers/proved-share-ledger.txt takes a row for the new plan: 15 written, 15 proved, 0 on a grid, 0 declared, 0 without a verdict. The verdict was taken by flang check --proof on this tree, not assumed. docs/four-coverages.md pointed at the removed run.sh; the link now names run.fscript, so links:check stays at 88 broken paths of 7130 - the same count as the base of this branch. Not touched, because they belong to other cells: scripts/four-coverages.fscript still reads and runs flang/translation/run.sh, so section 4 of that report will print "NOT TAKEN" until its owner renames the path; docs/adr/0030 line 273 still names the shell command in prose.
The suite is a plan now, so the job builds the seed on a cache miss. Ten minutes were the budget of a shell run that needed only cc; its neighbour guards-selftest, which builds the same seed, asks for twenty.
the-homeless-god
force-pushed
the
a/translation-run-to-plan
branch
from
October 4, 2026 16:47
b47703d to
321eef5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что сделано
flang/translation/run.sh(214 строк оболочки) снят. То же гоняетflang/translation/run.fscript— план, приговор которого доказан ядром:утверждений 15: доказано 15, сетка 0, объявлено, не доказано 0, и потому ярлыкидёт без
--на-веру.Вместе с переносом вписаны девять опытов, лежавших только в теле PR 298 (пять
на правило
отфильтровать, четыре на поблажку сторожу меры). Их автор не мог ихвписать:
run.shбыл не его. Ожидания — замер, а не предсказание: каждыйпрогнан, и каждый ответил ровно то, что названо в том блоке. Набор вырос с 23
опытов до 32, все 32 сошлись.
translation:check, код 0flang check --proofRULES[]timeна рабочей машинеЧем доказан перенос
Тройки совпали знак в знак. «Что, ожидаемый код, обязательное слово» сняты
ПРИБОРОМ у обоих файлов на одном дереве — у
run.shразбором его вызововopyt,у плана прогоном функции
«Опыты», — иdiffобеих выписок пуст: 32 строки,одни и те же имена, коды и слова.
Оба зелены на одном дереве:
run.sh→ИТОГ: опытов 32, все сошлись с ожиданием, код 0; план →перевод: закрытый список 41 правил, опытов 32, все сошлись с ожиданием, код 0.Отрицательный контроль, три подлога — на каждом оба краснеют кодом 1 и
называют ОДНО место:
run.shsvetofor.c: 500 → 501 (как в CI)· честная пара с разбором … ответил кодом 1, код 1PRINT-RULES.tsv: вынуто правилосвёртка· закрытый список разошёлся — … только в matcher.c: свёртка, код 1declared_measure_at_the_boundary.c: 1.0 → 2.0Третий подлог нарочно бьёт по ОДНОМУ ИЗ ДЕВЯТИ НОВЫХ опытов: иначе краснота не
показывала бы, что новые опыты работают, а не просто написаны.
Два отличия, названные нарочно
Они записаны в шапке плана, а не оставлены на догадку:
здесь он становится бедой номер один, а опыты всё равно прогоняются. Код тот
же 1, сведений больше.
run.shобрывала весь прогон; здесь она краснит СВОЙ опыт поимённо, аостальные досчитываются.
Где оболочка осталась, и почему
Оболочка осталась ровно там, где она прибор, а не судья: сборка сличителя
(
cc), правка честной пары в подделку (sed/awk) и запуск сличителя. Судитплан: разбор ответа, сверка закрытого списка, сборка опыта из частей и каждое
ожидание проверяются примерами на месте и обязательствами, которые считает
ядро. Прелюдия оболочки (пути, четыре прибора правки, 46 образцов) пишется ОДИН
раз в временный каталог и подключается каждым опытом — иначе протокол плана
раздувался бы в 178 КБ на зелёном прогоне вместо 37 КБ.
Заслоны
proved-share-vs-treewho-calls-the-guardsbinary.yml)guards-without-forgery-probeprose-numbers-guardinventory:checkfile-extensions:checklintпланаlinks:checkСчётные приметы, сдвинутые этой правкой (сняты прибором, не рукой): таблица
оболочки
56 / 9875 → 55 / 9661, «файлов вне flang»193 → 192в трёх местах,«файлов
*.sh»50 → 49в двух.Чего не сделано, и это чужое
scripts/four-coverages.fscriptчитает и запускаетflang/translation/run.sh(
«Translation suite», строки 26, 43-44) и считает опыты по строкамopyt. После этого PR раздел 4 того отчёта напечатает «НЕ СНЯТО». Файл немой — не правил; владельцу нужно переписать путь на
run.fscript, а счётопытов — на поле
«опытов»ответа плана.docs/adr/0030, строка 273 называетsh flang/translation/run.shв прозезаголовка Ш4. ADR — запись о прошлом,
links:checkеё не судит; правка завладельцем
docs/**.docs/four-coverages.mdправлен ровно в одном месте: мёртвая ссылка наснятый
run.shпереписана наrun.fscript, чтобыlinks:checkне вырос.Ветка пересобрана над стволом дважды
Ствол ушёл на 41 коммит пока работа шла, и дважды — в счётные приметы оболочки
(другой перенос снял
version-derivations-guard.shи ещё один скрипт). ЧислаНЕ переписаны руками поверх конфликта: при каждом столкновении взята версия
ствола, а затем прибор (
prose-numbers-guard,inventory:languages) назвалразошедшееся заново, и правлено ровно названное. Прогон плана и три подлога
перемерены на пересобранном дереве — ответы те же.