Эталон отстаёт от свидетеля, который уехал, — и отставание надо мерить, а не оговаривать

Когда одна ветка пишет эталон на самом языке, а другая в это же время правит свидетеля, слияние проходит без единого конфликта: файлы разные, строки не спорят. Красной становится СВЕРКА, и не на одной программе, а на всех сразу.

За сборку work/svodka3 это случилось ПЯТЬ раз подряд с одним и тем же эталоном ядра доказательства и по одной и той же причине.

Чем подтверждено. flang/self/proofterm.flang писался под свидетеля своего основания. На собранном дереве побайтовая сверка дала 249 расхождений из 249 — то есть ни одной совпавшей программы. Ни одно из них не было про доказательство: свидетель завёл в ответе четвёртое поле (отчёт о снятии предусловий), и оно разошлось на КАЖДОЙ программе, потому что печатается всегда.

Дальше зазор снимался кусками, и каждый кусок мерился прогоном:

Семь оставшихся — это три куска САМОГО ядра, которых у эталона нет: начальная алгебра встроенного списка (3 программы), принцип по отрезку нат (2 программы и 1 отказ), точные десятичные с правилом остатка (1 программа).

Что из этого следует для сборки. Число расхождений — это не «насколько плохо», а УКАЗАТЕЛЬ, куда смотреть. Расхождение на всех программах сразу почти никогда не про решение: так выглядит лишнее или недостающее ПОЛЕ в общем ответе. Расхождение на семи из двухсот сорока девяти — наоборот, всегда про решение, и чинится не текстом, а переносом правила.

Как остановиться честно. Дописать три куска ядра — это разработка, а не сборка, и наполовину перенесённый принцип отвечал бы «доказано» там, где свидетель отвечает «отвергнуто». Поэтому зазор не смягчён допуском, а НАЗВАН: в flang/test/self-proofterm.test.mjs лежит список из семи имён с причиной у каждого, и сверка сличает его целиком — deepEqual списка имён, а не порог «не больше семи». Разойдётся восьмая — красно. Сойдётся одна из семи — тоже красно, потому что тогда врёт список.

Разница между «допуском» и «названным зазором» ровно эта: допуск гаснет молча, названный зазор краснеет в обе стороны и закрывается только пустым списком.

Шестой случай, 18 августа: отстал эталон ГЕНЕРАТОРА КОДА, и упала неподвижная точка

Пять первых случаев были про эталон ядра доказательства, и отставал он от новой ВОЗМОЖНОСТИ свидетеля. Шестой другой в двух отношениях, и оба важны.

Отставание от оптимизации, а не от возможности. Свидетельский генератор C (flang/src/emit/c.mjs) научили встраивать простые действия вместо вызова рантайма, а эталон (flang/self/emit-c.flang) за ним не пошёл. Ни одной новой возможности не появилось — поведение напечатанного кода то же самое. Разошлись только байты.

Цена оказалась выше, чем у пяти предыдущих вместе. Побайтовая сверка — это и есть критерий неподвижной точки, поэтому отставание уронило не сверку одного модуля, а ГЛАВНОЕ утверждение проекта:

$ FTS_REQUIRE_TOOLCHAINS=c node --test flang/test/self-bootstrap.test.mjs
tests 29   pass 25   fail 4

Строки «неподвижная точка сошлась: 7 файлов совпали побайтово» в выводе нет. Падают четыре проверки, и у всех одна причина:

Чем подтверждено. Прогон 18 августа на github/main 83a0b5d5, 574 166 мс, /home/b/tmp-flang/bootstrap-run.log. Независимо воспроизведено дважды.

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

Чем ограничено. Это не довод против оптимизации и не довод за откат. Это довод за то, чтобы правка генератора кода в свидетеле и в эталоне ехала одним коммитом, — потому что поймать её может только самый долгий прогон набора (десять минут), и в промежутке ствол стоит красным.

Седьмой случай, 19 августа: та же правка отстала ещё у СЕМИ целей из восьми

Шестой случай починили в C, и неподвижная точка сошлась — 29 проверок из 29, 958 секунд. Красным при этом остался тот же самый долг, только у остальных семи целей печати, и увидеть его в неподвижной точке было НЕЛЬЗЯ: она проверяет ровно одну цель — C.

Правка та же: генератор кода зовёт помощника без проверки частичности там, где непустота доказана (rt.BHeadProven вместо rt.BHead). У всех восьми реализаций на JavaScript она есть — одна строка, помощникФормы(...) из flang/src/builtins.mjs. У сторон на flang она была ровно в одной:

flang/self/emit-c.flang есть остальные семь нет

Чем подтверждено. Прогон node --test flang/test/self-emit-*.test.mjs на стволе 2bfcb7d0: пять красных проверок в пяти файлах (go, java, python, rust, js), у всех одна улика —

flang/stdlib/strings.flang: flang/stroki.go разошёлся на строке 218 свидетель: "t39, e40 := rt.BHeadProven(ctx, t37)" flang: "t39, e40 := rt.BHead(ctx, t37)"

C# и Elixir молчали не потому, что у них правило было: в их корпусе сверки не попалось программы с доказанной непустотой. То есть две цели из восьми несли тот же долг, и ни одна проверка его не показывала — тот же класс, что «проверка перестала сравнивать». После переноса: 147 проверок из 147 зелены на всех восьми целях, пропущено 0.

Чему учит, сверх шестого случая. Неподвижная точка — не сторож долга генераторов кода. Она сторожит ОДНУ цель, а правка свидетеля обычно общая для восьми: помощникФормы живёт в общем файле, и в него вписали разом все восемь реализаций на JavaScript. Значит после всякой правки общего места надо гонять восемь сверок self-emit-*, а не одну неподвижную точку — она зелена и при семи отставших сторонах.

Чем ограничено. Молчание C# и Elixir — не доказательство, что там правило было не нужно: их корпус сверки просто беднее. Правило туда перенесено тем же коммитом, и молчание осталось молчанием — красным оно не стало ни до, ни после.

Восьмой случай: 264 расхождения из 264, и ни одного в журнале доставок

Эталон планировщика процессов (flang/self/conc.flang) писался на неслитой ветке против свидетеля flang/src/conc.mjs в 1666 строк; к моменту переноса свидетель уехал до 2140 (сторож чисел: не про сегодняшнее дерево — обе величины записывают размер НА ТОТ МОМЕНТ, и в этом весь довод заметки). Побайтовая сверка на сетке семян дала 264 расхождения из 264 — ни одного совпавшего исполнения, как в первом случае.

Число здесь опять оказалось указателем, а не мерой: расхождение у всех 264 шло в ХВОСТЕ итога и состояло из двух новых полей ответа (кадров и поручения), а журнал доставок — та самая часть, ради которой сетка семян и заведена, — сошёлся знак в знак у всех. Догон занял два поля и одну ветку действия; после него на той же сетке 0 расхождений, а сетка выросла с 264 исполнений до 336, потому что в корпус добавился каталог с седьмым действием.

Чему это добавляет к правилу. «Расхождение на всех программах сразу почти никогда не про решение» подтвердилось седьмой раз подряд. Полезнее самого числа оказалось место первого разошедшегося байта: оно сразу назвало, что дело в поле ответа, а не в поведении, и избавило от разбора 264 журналов.

Чем подтверждено. Ветка work/planirovshchik, node --test flang/test/self-conc.test.mjs: до догона 264/264 расхождений, после — 0 из 336 при 1889 доставках и 84 поручениях.

Смежное. Побайтовая сверка со свидетелем — главный метод проверки · Проверка, переставшая сравнивать, продолжает зеленеть · Бывают конфликты слияния, которых git не показывает · Два ядра, выросшие порознь от одной точки, текстом не сливаются