Семя в bootstrap/ отстаёт от исходников ядра, и разница видна прямо в отказе: четыре вида цели против пяти

make -C bootstrap собирает компилятор из закоммиченного C, и этот C в дереве СТАРШЕ исходников, из которых он печатается. Проверяется одной командой:

sh scripts/raskrutka.sh --check
  • bootstrap/compiler_flang.c: в дереве 19 462 385 байт, печать даёт 19 598 492
  • bootstrap/compiler_flang.h: в дереве  3 872 372 байт, печать даёт  3 901 886

Чем это кусает того, кто пишет утверждения. Собранный из дерева двоичный знает ЧЕТЫРЕ вида цели и так и говорит в отказе: «правил четыре — „не меньше 0“, „не больше конечного литерала“, „не больше терма“ и „равно“». flang/self/proof-kernel.flang знает ПЯТЬ: там есть «вхождение по построению» — цель вида Л содержит Э. Пока семя не перепечатано, всякое утверждение про вхождение читается как «сетка», хотя ядро его закрывает.

Замер на двух модулях библиотеки: тем же деревом, но двоичным из сегодняшних исходников, доказано 16 утверждений вместо 14. Обе добавки — «вставка удлиняет список ровно на один» у «Вставить по порядку» и у «Вставить по»; закрываются индукцией, читающей постусловие вызванной функции, и старому двоичному это не по силам.

Учит вот чему. Отчёт «доказано ядром N» имеет смысл только вместе с ответом на вопрос, ЧЕМ считали. Считать надо двумя двоичными — собранным и свежим — и разницу называть, иначе работа выглядит слабее, чем она есть, либо сильнее. Прогон raskrutka.sh --check стоит десяти минут и делается один раз в начале.

Чем подтверждено. Ветка vypusk/utv-lists на основании df055a6b, 20 августа. Расхождение существовало ДО работы — проверено на самом основании.

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

Связано: left-fold-is-blocked-because-the-fold-rule-does-not-read-the-callee-postcondition, porting-a-rule-means-porting-its-refusal-text

20 августа отставание перешло черту: семя перестало РАЗБИРАТЬ исходники

Прежде разница была в силе ядра — семя доказывало меньше. Теперь семя bootstrap/ на github/main = 7e8495ec не разбирает flang/self/interpret.flang вовсе:

LC_ALL=C.UTF-8 ./bootstrap/flang check flang/self/interpret.flang
FLANG_PARSE, строка 2801, столбец 98: неожиданное 'по'

Строка 2801 — символ по коду «код», встроенная форма, приехавшая в ствол слиянием ветки svod/simvol. Слово charFromCode в bootstrap/compiler_flang.c не встречается ни разу, а сам семенной C перепечатан ПОЗЖЕ слияния (коммит 6b1017d8, 14:07) — то есть печатали его с ветки, где формы ещё не было, и после слияния не перепечатали.

Следствие: sh scripts/raskrutka.sh на стволе не проходит вовсе — 29 замечаний, печать отменена. Круг раскрутки разорван: собрать компилятор из его собственных исходников закоммиченным семенем нельзя.

Как развязано. Двоичный из чужой рабочей копии, где форма уже была (/srv/flang-rabota/simvol-po-kodu/bootstrap/flang, версия 0.5.0), напечатал семя из сегодняшних исходников; дальше семя держит себя само. Два шага: FLANG=… sh scripts/raskrutka.sh → make -C bootstrap → sh scripts/raskrutka.sh → make -C bootstrap.

Чему учит. Слияние ветки, трогающей лексер или парсер, обязано нести перепечатку семени в том же своде. Иначе разрыв замечает не сверка, а первый, кто попробует пересобрать компилятор, — и развязывать ему нечем, если чужой копии с нужным двоичным рядом не окажется.

Заодно это объясняет расхождение в замерах: node benchmarks/proof-cost/schyot-20.mjs закоммиченным семенем даёт 9 содержательных из 20, а перепечатанным из тех же исходников — 10. Разницу целиком даёт файл 03 «Вписать»: правило «вхождение по построению» в семени отсутствовало.

25 августа 2026: разрыв вырос до двух видов

Правило 11 «строгий порядок по построению» влито в ядро (918225f8): исходник называет девять видов цели, семя по-прежнему семь. Отставание не только воспроизводится — оно накапливается: каждое новое правило ядра увеличивает разрыв, пока не пройдёт перепечатка.

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

24 августа 2026: разрыв тот же, но уже шесть видов цели против семи

Отставание не разовое, оно воспроизводится. Исходник ядра называет семь видов цели, напечатанное семя — шесть:

grep -o 'правил семь\|правил шесть' flang/self/proof-kernel.flang   → правил семь
grep -o 'правил семь\|правил шесть' bootstrap/compiler_flang.c      → правил шесть

Не хватает семени правила «начинается с». Кусает это ровно так, как описано выше: обещание результат начинается с "н" у «Имя степени» (flang/self/bounded.flang) собранный из дерева двоичный числит объявленным, и по его отказу это выглядит дырой ядра, хотя правило в ядре есть. Всякий вердикт о цели вида «начинается с», снятый до перепечатки семени, читать нельзя.

Чем подтверждено. Ветка b/self-bounded над 462a24cf; двоичный собран make -C bootstrap CFLAGS='-std=c99 -O2' -j8 (2 мин 32 с); дословный отказ снят пробой с заведомо непроходящей теоремой в /srv/tmp/w-self-bounded/proba/otkazy.flang.