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

Закоммиченная точка раскрутки отстала от исходников на одну форму языка, и из-за этого двоичный компилятор не проверяет три своих собственных модуля

flang/self/lexer.flang знает форму символ по коду ЧИСЛО (charFromCode, четыре вхождения в таблицах слов). В bootstrap/compiler_flang.c строки charFromCode нет ни одной. Значит собранный из точки раскрутки двоичный компилятор эту форму не разбирает:

flang check проба.flang
FLANG_PARSE, строка 6, столбец 10: не разобрана конструкция: неожиданное 'по'

Тем же отказом падает flang check flang/self/interpret.flang (строка 2801, символ по коду «код»), а за ним — всё, что через него ввозится: flang check flang/self/conc.flang даёт 21 отказ вида «тотальная функция … вызывает неизвестную функцию «Знач по ключу»», и flang test на нём отвечает «примеры не запускались — программа не прошла проверку».

Практическое следствие, из-за которого это стоит отдельной заметки. Слой процессов сейчас не проверяется ничем: категорную поверхность и процессы двоичный не судит по построению (говорит об этом прямо и отвечает кодом 2), а эталон планировщика flang/self/conc.flang тем же двоичным не проверяется из-за устаревшего семени. Реализации на JavaScript больше нет (коммит fe8e8a37), npm test не запускается вовсе — scripts/preflight.mjs ввозит удалённый flang/src/targets.mjs. То есть правку в планировщик сегодня нечем проверить прогоном, и это надо знать до того, как её начать.

Чем подтверждено. Ветка u/ssylka на основании github/main 7e8495ec, bootstrap/ без единой правки в рабочем дереве, двоичный собран make -C bootstrap, flang --version → 0.5.1. Все четыре отказа получены прогоном.

Круг разомкнут — проверено прогоном, а не выведено. flang emit flang/self/bootstrap/compiler.flang --target c --out КАТАЛОГ идёт 10 минут 3 секунды и не печатает ни одного файла: тот же FLANG_PARSE, строка 2801 на символ по коду, за ним каскад «неизвестный тип «Знач»», «неизвестный тип «Итог прогона»», и сверх того FLANG_RECURSION_LIMIT — «Беды ядра» съели 40 000 001 виток из 40 000 000. Двоичный не воспроизводит сам себя.

Чем лечится — и здесь курица с яйцом. Перепечатывает точку раскрутки сам двоичный (sh scripts/raskrutka.sh), а печатать он должен compiler.flang, в замыкание которого входит interpret.flang — тот самый файл, который он не разбирает. Руками bootstrap/** не правится: это семь напечатанных файлов, сверяемых байт в байт. Значит либо форма символ по коду уезжает из interpret.flang до перепечатки, либо семя поднимается тем же обходным путём, каким поднимали предел шагов (раздел «КАК ПОДНЯТЬ ПРЕДЕЛ» в scripts/raskrutka.sh): собрать промежуточный двоичный руками и печатать им.

Связано: typed-process-reference-is-already-expressible, bootstrap-circle-is-broken-but-the-binary-cannot-check-itself

Отставание повторилось 20 августа, и стоило оно двух разных бед

Беда первая: семя судит программы не теми правилами, что написаны в дереве. На github/main (d8bc4306) семя перепечатано коммитом 440800ad в 21:45, а ядро доказательств правили тремя слияниями ПОСЛЕ — в 21:53, 21:58 и 21:59. Видно это вердиктами: на flang/test/fixtures/poddelka-svyortka-shagom.flang двоичный из закоммиченного семени говорит про «нулей ровно столько, сколько элементов» — «сетка», а двоичный, перепечатанный из тех же исходников, — «доказано». Два утверждения корпуса доказаны в дереве и не доказаны в двоичном.

Беда вторая: на одном коммите перепечатка невозможна вовсе. На 702a3602 (тогдашняя голова main) scripts/raskrutka.sh требует потолка 200 млн шагов, а закоммиченное bootstrap/flang_runtime.h держит 40 млн: слияние вернуло старое семя, оставив новое число в скрипте. Печать зовёт проверку, шаг «Беды ядра» съедает больше 40 млн и обрывается; обрыв тянет каскад «неизвестный тип», и печатается тридцать замечаний, из которых по делу — первое.

Как выбраться. Рецепт из шапки scripts/raskrutka.sh работает: скопировать bootstrap/*.c *.h Makefile в каталог вне дерева, поправить там #define FL_MAX_STEPS, собрать и печатать FLANG=<путь> sh scripts/raskrutka.sh. Проверено прогоном 20 августа.

Чему учит. «Собрал из bootstrap/ и прогнал» не значит «прогнал тем, что написано в дереве». Всякий замер доказуемости обязан называть, ИЗ ЧЕГО собран двоичный, а слияние, тронувшее flang/self/, обязано кончаться перепечаткой семени — иначе следующий замер меряет вчерашнее ядро.

Связано: closedness-check-guarded-only-the-induction-branch