flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Одна причина, названная сразу за группу, прячет остальные — и держит в долге тех, кого не держит ничто

Список долга в flang/test/rabochiy-put.test.mjs перечислял восемь модулей JavaScript, у которых сторона на flang написана и сверена, и объяснял их задержку одной причиной на всех, записанной один раз, «чтобы не повторять её семь раз»: слой на flang связывается асинхронно (linkProgramcreateRuntime), а зовут этих восьмерых синхронные src/parser.mjs и src/types.mjs.

Прогон разложил эту одну причину на три разные, и две из трёх к трём файлам не относились вовсе:

причинасколько файловчем снимается
зазор стороны на flang (отвечает иначе, чем JavaScript)1дописать правила, а не менять проводку
синхронный вызов из разбора и вывода типов5связать заранее либо разделить модуль
зависимая позиция (ввозит только сосед из первой строки)2ничем: уходят даром вместе с соседом

Три файла — ядро доказательств src/proofterm.mjs и оба модуля flang/proof/ — простояли в долге на чужом доводе. Стены у ядра не было ни дня: его зовут из bin/flang.mjs через await import, из асинхронной команды. Держал его зазор, а когда зазор закрыли, переключение вышло в одну смену двери, и два зависимых модуля ушли следом сами, не потребовав ни строки переноса.

Чем подтверждено. Цепочка ввозов снята прогоном, а не чтением: перехватчик resolve из node:module пишет пару «кто ввозит → кого» на настоящем прогоне flang check --proof. В рабочем пути flang/proof/initial.mjs ввозит ровно один файл (src/proofterm.mjs), flang/proof/reduce.mjs — два (ядро и initial), а само ядро — один (bin/flang.mjs). Ветка worktree-agent-ac8d41bfd9b3d78cf, коммит 1a8fb1dc. После переключения перепись рабочего пути: файлов 23 → 20, строк 36 019 → 29 577.

Цена переключения ядра, медиана трёх прогонов flang check --proof: euclid 1,00 → 1,41 с (×1,41, вся цена — связывание слоя), import-check 1,43 → 4,50 с (×3,15, худший по доле), самоприменённый компилятор 64,33 → 70,17 с (×1,09, худший по абсолюту). Ответ команды не изменился ни на знак: --json-вывод, поток ошибок и код возврата сличены с базовым деревом на 160 программах, расхождений 0.

Правило на будущее. Раскладка, где у группы записана одна причина, обязана называть её у каждого члена отдельно — иначе член группы, чью причину сняли, остаётся в списке молча. Проверять причину дёшево: цепочка ввозов снимается перехватчиком за минуту и отвечает «кто держит кого» числом.

Чем ограничено. Про пятерых оставшихся (bounded, conc, failures, io, monad) стена подтверждена тем же прогоном: след вызова у каждого проходит через checkTypes либо через разбор, и оба синхронны насквозь. См. the-sync-wall-costs-263-call-sites.

Связано: four-pieces-of-javascript, byte-for-byte-comparison, a-number-without-a-named-measure