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

Гипотеза про адресацию по содержимому не работает у нас — и не из-за хешей

Важное уточнение к content-addressing: препятствие оказалось не там, где ожидалось.

Импорт в flang сливает всё в плоское пространство имён. Объявления импортированного модуля попадают в тот же плоский список, что и свои. Квалифицированных имён нет. Значит две версии одной библиотеки не слинкуются при любой схеме адресации — хеши тут ни при чём, мешает то, что у имени негде жить.

Плоскость идёт до самого низа. Генератор C заводит один именователь на всю программу; печать в цель тоже плоская. Поэтому квалифицированные имена стоят 14 287 строк — столько занимают все генераторы кода (flang/src/emit/), и каждый придётся трогать.

Попутная поправка к моей же ошибке. Я говорил, что связывания модулей на flang нет. Неверно: оно есть, и с августа 2026 живёт своим слоем — flang/self/link.flang, 1 382 строк, 135 функций, сверяется побайтово на 232 программах дерева. Прежде оно жило внутри flang/self/bootstrap/compiler.flang, где от него осталось 681 строка точек входа (сторож чисел: не про сегодняшнее дерево — замер того захода). Ошибочная оценка с поправкой ценнее молчания, поэтому записана, а не стёрта.

Найденная дыра, отдельная от всего. При связывании теоремы берутся только из входного файла: импортировали модуль — доказанные о нём теоремы не приехали. Пока проектов на flang мало, это незаметно; при библиотеке чужого кода это означает, что доказательства не переиспользуются вообще.

Связано: content-addressing, unison-measured, hash-inside-names-outside, what-goes-into-the-hash