Два ядра, выросшие порознь от одной точки, текстом не сливаются
Если две ветки правят ОДИН И ТОТ ЖЕ решающий модуль, каждая переписывая его устройство, слияние перестаёт быть слиянием текста и становится написанием третьего модуля. Развести это дешёвой правкой конфликтов нельзя, и попытка даёт файл, который загружается, зеленеет на части проверок и врёт на остальных.
Чем подтверждено. Сборка work/svodka3, ветка work/indukciya-vstroennyh против дерева. Обе выросли от 8203f39, обе правят flang/proof/reduce.mjs:
| дерево | ветка | |
|---|---|---|
| решающих правил | 3 (дно, потолок, тождество) | 4 (дно, тождество, порядок, разбор выбора) |
подпись свести | 4 довода (заключение, допущения, объявления, определения) | 2 |
нормализовать | 2 довода (с развёрткой определений) | 1 |
| источники фактов | тип, встроенная форма, свёртка, умножение, вес | тип |
| носителей индукции | 2 (сумма, отрезок нат) | 3 (сумма, список, признак) |
55 конфликтов в десяти файлах. Попытка свести их по одному дала синтаксическую ошибку в трёх файлах сразу и свести, у которого половина тела из одного лианажа, половина из другого.
Почему это не «дорого», а «мимо». Слияние текста отвечает на вопрос «какие строки оставить». Здесь вопрос другой: какое ядро у языка. У него один ответ, и дать его может только тот, кто напишет третье ядро целиком — с обоими наборами правил, одной подписью и одним прогоном по всему корпусу утверждений.
Как это видно ЗАРАНЕЕ, до первого конфликта. Три признака, каждый — команда из одной строки:
- разошлась ПОДПИСЬ решающей функции (
git diff base..A -- файл | grep '^[+-]export function'); - разошлась таблица правил или её версия (
ПРАВИЛА,ПРАВИЛО); - обе ветки завели по новому обходу над одной структурой.
Один признак — обычное слияние. Два — считать заранее. Три — не сливать, а заказывать.
Чем ограничено. Это про РЕШАЮЩИЕ модули — те, чей ответ уезжает в вердикт. У эталонов на flang (flang/self/*.flang) свойство ровно обратное: они сверяются со свидетелем побайтово, и слить их можно всегда — сверка сама скажет, где разошлось. Восемь таких слияний в этой же сборке прошли по одному прогону каждое.
Поправка от 18 августа 2026. Абзац выше неверен как общее правило. Побайтовая сверка спасает эталон, отставший от свидетеля, — но она ничего не говорит о случае, когда ДВЕ ветки переписали одного и того же эталона по-разному. Тогда эталон ведёт себя ровно как решающий модуль, и сверка не помогает: сравнивать нечего, пока файл не собран.
Померено при сведении веток в один ствол: flang/self/proof-kernel.flang разошёлся со стволом у ЧЕТЫРЁХ веток сразу — work/length-remembers, work/substring-rule, work/index-base-word, work/concurrency-twin. У всех четырёх одинаковый размер расхождения: 18 спорных кусков, 474 строки, плюс proofterm.flang (6 кусков, 116 строк) и proof-initial.flang (2 куска, 24 строки). Из 18 кусков 10 — чистое переименование («Шаг разбора при сведении» → «Шаг разбора ядра», «Состояние» → «Состояние ядра», «Узел ничто» → «Нет программы»), а оставшиеся 8 — разные ответы на один вопрос: подпись «Свести после счёта» в ветке принимает «счёт»: «Счёт цели», в стволе — «сочтено»: признак, и ствол при этом перенёс целые блоки из proof-initial.flang в proof-kernel.flang, а ветка правила их на месте.
Проверка «переименование или нет» стоит одну команду и отвечает за секунду: применить карту переименований к стороне ветки и сравнить со стороной ствола. Совпало — механическая правка; не совпало у половины кусков — заказывать перебазирование, а не сливать.
Признак, добавленный к трём прежним: одна и та же пара файлов конфликтует одинаковым числом кусков у НЕСКОЛЬКИХ веток сразу. Это значит, что разошлись не ветки между собой, а ствол со всеми ими, и чинить это по одной ветке — платить одну и ту же цену столько раз, сколько веток.
Связано: silent-merge-conflicts, checks-that-stopped-comparing, byte-for-byte-comparison, a-removal-must-turn-a-test-red