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

Набранное число расходится между страницами; подставленное — не может

Проверка, которая сверяет НАБРАННОЕ число с деревом, ловит расхождение задним числом и только там, куда её вписали. Проверка, которая подставляет число ИЗ замера, отменяет сам класс беды: разойтись двум страницам не в чем, потому что число одно.

Чем подтверждено. Число функций корпуса на сайте flang за восемь коммитов (с 73304b11 по 2b0af23f, 17–18 августа 2026) было набрано шестью разными значениями: 7997, 8016, 8018, 8047, 8159, 8490. Опубликованная страница в этот момент называла 8018 на главной и 8490 на роадмапе — владелец увидел два числа об одном на одном сайте. Дерево в тот же час считало 8535 (node flang/scripts/proof-ledger.mjs).

Проверка в дереве при этом была и работала: node docs/site/site-numbers.mjs --check собирал фразу из замера и требовал найти её в тексте буква в букву. Она краснела — 24 раза на четырёх страницах — и всё равно не помогала: чинить её значило править одно и то же число в четырёх местах руками, а между правкой и следующим замером сайт публиковался.

Что сделано вместо. Замер снимается одной командой в один файл (docs/site/numbers.json, 33 числа), в тексте страницы стоит подстановка вида {{корпус.функций}}, значение ставит сборка сайта. Проверка перемеряет дерево заново и сверяет с файлом — то есть сторожит ОДНО место, а не двадцать четыре. Правка «числа догнали дерево» стала одной командой вместо двадцати четырёх правок текста.

Чем ограничено. Дорогой замер нельзя считать при сборке: свод корпуса — это загрузка всего дерева языка, 52 с на этой машине, а сборка сайта обязана идти без зависимостей и укладываться в доли секунды. Поэтому файл чисел лежит в репозитории, и его свежесть держит отдельная проверка, а не сама сборка. Между коммитом, сдвинувшим корпус, и перезапуском замера файл отстаёт — ровно как любой снимок; ловится это красной проверкой, а не автоматически.

Отдельно: подстановка НЕ работает внутри блоков кода и внутри ` код `. Иначе страницу про сами подстановки написать нечем — пример превратился бы в число.

Признак класса. Если одно и то же число стоит в тексте больше одного раза — это не «дубль», это будущее расхождение. Считать надо, сколько МЕСТ, а не сколько чисел: два места одного числа расходятся не «если», а «когда».

Подстановки хватило только там, куда её довели. Сплошной прогон всех набранных руками чисел на страницах сайта дал восемь расхождений с деревом против нуля у подставленных:

страницасказанопрогон дал
operations.*: итог отчётадоказано 6, сетка 47доказано 20, сетка 33
case-studies.*: итог отчёта службыутверждений 7, сетка 2утверждений 24, сетка 17
case-studies.*: строк на flang / на Node1743 / 4191746 / 421
case-studies.*: plan-network.flang198201
getting-started.ru: печать в C264 365 Б268 375 Б
getting-started.ru: печать в Rust126 815 Б126 827 Б
getting-started.md: печать в C266 373 Б268 219 Б
packages.*: вес пакета discount1 554 Б4 343 Б

Последнее было не «на сколько-то байт», а качественно: страница объясняла, почему пакет МЕНЬШЕ исходника «обратимо сжатый», а сжатие из формата убрали, и пакет стал больше исходника. Число протухло вместе с доводом, который оно подпирало.

Мораль для набранного числа: если рядом с ним стоит объяснение «потому что», то протухнет и объяснение, а его никакая сверка не поймает.

Дополнение 20 августа 2026: подстановка врала всем сайтом сразу, и сторож молчал

Поправка к обещанию заметки. Здесь стояло, что подставленные числа разойтись не могут, «потому что число одно». Это верно про расхождение страниц МЕЖДУ СОБОЙ и неверно про расхождение с деревом. Одно число — это одно место, где можно соврать всем страницам сразу, и ровно это и случилось.

Что померено. После удаления реализации на JavaScript (fe8e8a37) файл docs/site/numbers.json отстал от дерева на каждом числе о корпусе:

ключстояло в файледерево на github/main 5ec0cb03
корпус.функций99169409
корпус.тотальных79367494
корпус.обычных19801915
корпус.файлов277279
носители.композиция73816972
носители.структура446414
утверждения.высказано409394
утверждения.доказано239225
сторож.мест110113

Дерево считано node flang/scripts/proof-ledger.mjs --json двоичным 0.5.1, 279 файлов, отчёт вышел у 244.

Почему это не поймали. Свежесть файла держал ./ярлык числа:проверка, и он живёт в том же модуле, что измеритель: docs/site/site-numbers.mjs ввозит покрытие() из docs/site/surfaces-run.mjs, а тот — удалённые flang/src/lexer.mjs и flang/src/parser.mjs. Проверка не покраснела про числа — она умерла на ввозе, тем же ERR_MODULE_NOT_FOUND, что и сборка сайта. Красное «числа отстали» и красное «модуля нет» в отчёте выглядят одинаково красным, и первое потерялось за вторым.

Признак класса. Проверка свежести, живущая в одном модуле с измерителем, падает вместе с ним — и падает МОЛЧА про свой предмет. Отличать надо два вопроса: «измеритель работает?» и «число свежее?». Пока ответ на первый берётся из того же ввоза, что и ответ на второй, второго вопроса просто не существует. Тот же класс, что checks-that-stopped-comparing, но вход другой: там проверка перестала сравнивать и зеленела, здесь перестала запускаться и краснела не о том.

Второе следствие, важнее первого. Один сломанный измеритель портит числа не на одной странице, а на всех сразу, и тем полнее, чем лучше доведена подстановка. Цена подстановки названа честно: она меняет двадцать четыре тихих расхождения на одно громкое — но только если это одно кто-то слышит.

Чем ограничено. Числа выше поправлены в docs/site/numbers.json разовым прогоном по сохранённому отчёту, а не командой ./ярлык числа: та по-прежнему не запускается. Три ключа поправить было нечем и они оставлены как есть — словарь.* (мерит surfaces-run.mjs), цели.* (считает файлы flang/src/emit/*.mjs, которых теперь ноль, и посчитал бы ноль целей) и корпус.безПроверок (двоичный не печатает мест частичных форм).

Связано: a-number-without-a-named-measure, renaming-a-file-silently-disables-the-guard, a-hand-written-list-outlives-the-tree, checks-that-stopped-comparing, four-pieces-of-javascript