flang 0.7.15 — Калькулятор снят из чекера: гейт независимой проверки закрыт

Калькулятор снят из чекера: гейт независимой проверки закрыт

Что появилось

• ГЕЙТ Г7 ЗАКРЫТ. Из чекера убран ход, который ДОКАЗЫВАЛ утверждение, вычисляя его, вместо того чтобы проигрывать записанные шаги. Убран в обеих точках: сняв его в одной, работу немедленно подхватывала вторая (дверь половина_закрыта, тождественны на глубине 6), и проверка грепом по имени печатала при этом ноль. Сторож подлога отделён от вычислителя и остался на месте. Тождество знак в знак и замкнутый счёт сохранены.
• Проверка гейта на калькулятор больше НЕ ГРЕП ПО ИМЕНИ, а прогон по живой паре исходник+запись (flang/proof/чекер/пробы/записи/Ч365/П1-цель-не-равенство). Две ∀-цели там доказуемы только переписыванием тела законами, ходов в записи нет ни одного — честный чекер обязан оставить их на слове ядра и назвать поимённо. Ловушка ДВУСТОРОННЯЯ: третья цель закрывается тождеством знак в знак и обязана остаться закрытой, иначе проверку брал бы и чекер, сломанный до состояния «ничего не доказываю». Переименование функции обойти проверку больше не может.
• Прибор доказуемости sh scripts/доказуемость.sh гоняет ЧЕТЫРЕ проверки и печатает все четыре числами, каким бы ни был исход предыдущих. Прежде он замыкался накоротко: провалилась первая — остальные не гонялись вовсе. Сторож, который не гоняется, не сторож.
• Манифест набора подделок flang/proof/подделки/НАБОР.tsv — 31 строка, класс каждой подтверждён чтением шапки исходника. Храповик ХРАПОВИК.txt держит два числа: сколько подделок объявлено и сколько мест их честных половин проиграно. Проверка 4 краснеет, если набор ослаб. Одна подделка при сверке оказалась не того класса, каким числилась.
• Ведомость правил вывода flang/proof/ПРАВИЛА-ВЫВОДА.tsv — 71 строка в ДВУХ нотациях, логической и категорной, сверенная с кодом ядра построчно. Согласие нотаций проверяемо, а не декларативно: каждая посылка пронумерована, и категорная запись обязана назвать её место. Четыре сторожа с восемью пробами на подлог. Решение ADR-0022: факт о типе едет в записи выводом, а не именем правила и не аксиомой.
• Файл настроек .flangrc и выбор языка вывода (решение ADR-0024). Пары «ключ = значение», не JSON и не программа: файл читается до того, как язык готов говорить. Старшинство: довод, среда, файл проекта, файл дома, локаль, умолчание. Подъём обрывается на первой примете, поэтому дальний файл не перекрывает ближний.
• Оболочка печатает отпечаток своей сборки второй строкой flang --version: восемь знаков sha256 самого исходника оболочки. Взято у iex: дополнение по Tab, .очистить, история между запусками файлом, вставка без мельтешения (замер на одной вставке: 90 перерисовок было, 10 стало).
• Десятая цель печати — TypeScript. Оба README и сторож обещаний печати считают десять.

Что изменилось

• Знаменатель доли СУЖЕН решением ADR-0023: из него вынесены места, недостижимые в принципе — обязательства записи, которую чекер отвергает целиком. Вынос идёт по ДВУМ признакам сразу, объявлению манифестом И измеренному отказу чекера: по одному замеру порча записи растила бы долю. Доля 517 / 651 = 79,42 % против 517 / 665 = 77,74 % прежней меры. Числитель не изменился ни на место, баланс печатается и сверяется.
• Комментарии сняты из 58 файлов на flang, минус 7429 строк. Код каждого файла сверен без комментариев байт-в-байт, вывод flang check и flang test --ledger — знак в знак до и после.
• Битых ссылок в дереве 1947 → 18. Сторож научен отличать запись о прошлом (сделанная задача, датированный отчёт) от обещания о настоящем, и число пропущенного печатает в вердикте, а не прячет. Список исключений при этом не раздут, а сокращён: 373 строки → 171.
• Тело выпуска на GitHub печатается из docs/release-notes.json, а не из строки в конвейере. У 0.7.14 на 93 коммита приходилось 168 знаков тела. Выпуск без записанных заметок теперь отвергается.
• .claude и AGENTS.md переехали в .ai/, README.ru.md — в docs/. Корень отделяет язык от оснастки.
• Версия больше не живёт в package.json: он печатается из scripts/emit-package.flang.

Что сломалось

• Доля с прежними выпусками несравнима второй раз подряд: 0.7.14 сменил числитель, 0.7.15 сужает знаменатель. Обе меры печатаются с разбивкой, и баланс знаменателя сверяется прибором.
• flang package не работает ни на одном входе с 29 августа: вызов с одним доводом при функции о двух. Найдено прогоном, починка — одна строка, доедет следующей перепечаткой семени (задача 3401).
• Поиск модулей поднимается выше корня дерева, и файл-предок каталогом выше побивает библиотеку языка. Дыра названа и померена: 20 имён затеняемы, 5 затенений живых. Сторож scripts/module-origin-guard.sh её видит, починка в двоичном ждёт перепечатки (задача 3127).
• Вердикт по-прежнему НЕ ДОКАЗУЕМ: три проверки из четырёх сошлись, доля 79,42 % при пороге 95 %.

---

The calculator is gone from the checker: the independent-verification gate is closed

What appeared

• GATE G7 IS CLOSED. The step that PROVED a claim by computing it, instead of replaying the recorded moves, is gone from the checker. Gone from both places: removing it from one, the work was immediately picked up by the second (the половина_закрыта door, тождественны at depth 6), while a grep-by-name check printed zero. The forgery sentinel has been separated from the prover and stays. Sign-for-sign identity and closed arithmetic are kept.
• The gate's calculator check is NO LONGER A GREP BY NAME but a run against a live source+record pair. Two of its goals are provable only by rewriting the body through laws, and the record holds no moves at all, so an honest checker must leave them on the kernel's word and name them. The trap is TWO-SIDED: a third goal closes by sign-for-sign identity and must stay closed, otherwise a checker broken down to «I prove nothing» would pass too. Renaming a function can no longer evade the check.
• sh scripts/доказуемость.sh now runs FOUR checks and prints all four with numbers, whatever the earlier ones answered. It used to short-circuit. A sentinel that does not run is not a sentinel.
• A manifest of the forgery set, 31 rows, each class confirmed by reading the source header. A ratchet holds two numbers: how many forgeries are declared, and how many places of their honest halves are replayed. Check 4 goes red if the set weakens.
• A ledger of derivation rules, 71 rows in TWO notations, logical and categorical, checked against the kernel code row by row. Notation agreement is verifiable, not declared: each premise is numbered and the categorical form must name its position. Four sentinels with eight forgery probes. Decision ADR-0022: a type fact travels in the record as a DERIVATION, not as a rule name and not as an axiom.
• A settings file .flangrc and a choice of output language (ADR-0024). Key = value pairs, not JSON and not a program: the file is read before the language is ready to speak. Precedence: argument, environment, project file, home file, locale, default. The walk up stops at the first marker, so a distant file cannot override a near one.
• The shell prints its own build fingerprint as the second line of flang --version. Borrowed from iex: Tab completion, .clear, history across runs, paste without flicker (measured on one paste: 90 redraws before, 10 after).
• A tenth emit target, TypeScript. Both READMEs and the emit-promises sentinel count ten.

What changed

• The share denominator is NARROWED by ADR-0023: places unreachable in principle are taken out — the obligations of a record the checker rejects whole. Removal requires TWO signals at once, a manifest declaration AND a measured rejection: on one signal alone, corrupting a record would raise the share. The share is 517 / 651 = 79.42 % against 517 / 665 = 77.74 % under the old measure. The numerator did not change by a single place, and the balance is printed and checked.
• Comments removed from 58 flang files, 7429 lines fewer. Each file's code compared without comments byte for byte; flang check and flang test --ledger identical before and after.
• Broken links in the tree: 1947 → 18. The sentinel now tells a record of the past (a completed task, a dated report) from a promise about the present, and prints how many it skipped rather than hiding it. The exception list shrank rather than grew: 373 rows → 171.
• The GitHub release body is printed from docs/release-notes.json instead of a string in the pipeline. Version 0.7.14 had 168 characters of body for 93 commits. A release with no recorded notes is now refused.
• .claude and AGENTS.md moved to .ai/, README.ru.md to docs/.
• The version no longer lives in package.json: that file is printed from scripts/emit-package.flang.

What broke

• The share is incomparable with earlier releases for the second time running: 0.7.14 changed the numerator, 0.7.15 narrows the denominator. Both measures print a breakdown, and the denominator balance is verified by an instrument.
• flang package has been broken on every input since 29 August: a one-argument call against a two-argument function. Found by a run; the fix is one line and ships with the next seed reprint.
• Module lookup walks above the tree root, and an ancestor file one directory up beats the language library. The hole is named and measured: 20 names shadowable, 5 live shadowings. A sentinel sees it; the fix in the binary awaits a reprint.
• The verdict is still NOT PROVABLE: three checks of four agree, the share is 79.42 % against a 95 % threshold.

---

Страница выпусков: по-русски · in English.

Архив flang-0.7.15-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.