flang 0.7.24 — Линтер в языке, памятка ядра и три закрытые дыры в доказательствах

Линтер в языке, памятка ядра и три закрытые дыры в доказательствах

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

• flang lint — длина строки и глубина ветвлений, пределы из .flangrc. Ключи max-line-length и max-conditional-depth, поведение задаёт lint (refuse — отказывать). Заслон перед пушем судит только вашу правку: добавленная строка не длиннее предела, тронутая функция не глубже. Дерево пределам не отвечает, и ведомости долга нет по решению ADR-0053: flang lint по дереву находит 32 342 строки длиннее 120 знаков и 1365 функций глубже 2 — в 703 файлах из 1301 (снято 3 октября 2026). Правка этого выпуска убрала из своих строк 77 длинных, остальное осталось как было.
• Короткие команды живут в файле настроек. flang run-script <имя> берёт строку из .flangrc; ярлыки больше не прячутся в отдельном скрипте, и flang run-script без имени печатает, какие есть.
• Профиль библиотеки в .flangrc. Программа видит те модули стандартной библиотеки, которые назвал профиль, — замыкание меньше, а имена не сталкиваются.
• Памятка ядра: за один прогон чистый вызов считается один раз. Ускоряет проверку доказательств и печать семени; в напечатанном C памятка стоит обёрткой вокруг трёх функций ядра.
• Литерал-блок """ снимает общий отступ продолжений (ADR-0052). Длинный текст больше не обязан начинаться с нулевого столбца, и длинная строка в коде перестала быть выбором между пределом строки и правдой.
• В библиотеке появились длинное деление с остатком, НОД и точные рациональные. Деление и НОД стоят в bignum.flang — на 0.7.23 там не было ни того, ни другого; обязательств у него по-прежнему 9, новые функции постусловий не несут. rationals.flang — новый файл: дроби на длинных целых, 17 функций и 13 обязательств (сокращение, четыре действия, сравнение, гармоническая сумма). fmath.flang тоже новый, но это не функции, а четыре утверждения о неотрицательности длины и суммы; ни один файл дерева на них пока не ссылается.
• Доказательство словами: рассуждение пишется предложениями, посылки — допущениями (ADR-0050). Шаг называет правило ядра, а не номер строки.
• Сторож забытых времянок проверок. Неотслеживаемый каталог .flang-storozh-* или файл с «probe» в имени, оставшийся в дереве после снятого прогона, краснеет кодом 1 с путём; шесть мест, где времянка обязана лежать в дереве (компилятор ищет ввозимые модули относительно файла), сторож называет сам с причиной.
• Решение о точных целых записано, а отсутствие их держится пробой (ADR-0036, задача 1908). Числа в языке по-прежнему IEEE-754 double, и целые точны до 2⁵³−1. Набор flang/proof/probes/exact-integer/ каждым прогоном CI показывает, что точного целого в языке нет: литерал 42 остаётся числом, кольцевых правил для него у ядра нет. Проба покраснеет в тот день, когда появится, — и это её работа.

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

• Независимая проверяющая программа переигрывает больше. Шаги «по предположению» из посылок утверждения, шаги по свойству, ссылки между файлами, проекции полей, типы модулей и наборы зависимостей — как их видит сборщик, — и то, что ядро доказывает в ваших программах, а не только в дереве языка.
• Тождество над открытым термом больше не объявляется ложью (4850). Ход «подставить терм вместо самого себя» принимается без вычисления, а терм, который нельзя вычислить, уходит в «не взялся» (код 3), а не в расхождение (код 1): место, которого прогон не взялся проверять, — не ложь.
• У независимого сверщика появился ключ --строго. Он спрашивает не «не противоречит ли запись исходнику», а «доказано ли САМО»: обязательство должно быть хотя бы одно И каждое числиться доказанным, иначе исход 3 с названной причиной. На девяти программах набора строгих проб шесть ответов «ноль» стали «три» — включая запись к программе с ложным постусловием, которой прежде ноль давали все три прибора.
• Запись доказательства, отставшая от исходника, отвергается, а сама проверяющая программа пересобирается, если её исходник новее двоичного: старый двоичный больше не судит новый исходник молча.
• Вердикт дерева — ДОКАЗУЕМ, и набор проб под ним вырос. Доля, переигранная независимым проверяющим, стоит на 100,00 % — 650 обязательств из 650; порог вердикта ровно 100 %, и он взят. Против 0.7.23 выросло не число доли, а набор, которым она держится: подделок в манифесте 36 → 38, проб на подлог 575 → 631, честных проб 274 → 315, вынесенных недостижимых мест 27 → 30, и храповик набора поднят вместе с ними. Четыре проверки вердикта: калькулятор из проверяющей программы снят, доля не ниже порога, набор проб пройден, набор не ослаб. Снято io scripts/provability.fscript --plan Verdict: по 0.7.23 — прогон CI 29 сентября 2026 на main, по 0.7.24 — прогон 3 октября 2026 на ветке выпуска.
• Оснастка переехала с shell и Python на планы flang. Сторожа, пробы и приборы счёта теперь планы; заслон перед пушем запрещает рост shell, Python и лишнего markdown, а CI судит сообщение коммита по уговору (префикс, длина заголовка, только ASCII).
• Справочник и сайт переписаны простыми словами. README говорит, что язык делает и как его поставить; docs/DESCRIPTION.md больше не привязан к выпуску («описание соответствует 0.7.23» убрано) и не печатает числа, меняющиеся от сборки к сборке. Датированных отчётов в дереве больше нет — кроме двух в docs/archive/, на которые ссылается ROADMAP; из docs/ за выпуск ушло 418 файлов.
• Дата из числа дней верна ниже года один. Поправка, написанная для усечения, срабатывала второй раз под делением-полом, и день −719834 давал −719833. Круг «дни → дата → дни» сходится теперь на 1038 днях подряд у границы эры, на 7240 днях шагом 1009 и на 4000 псевдослучайных — расхождений 0.
• Отпечаток семени находит свой коммит по содержимому. Прежде он называл sha, умиравший при переносе ветки, и быстрая сверка отказывала словами «коммит дереву неизвестен»: четыре из пяти значений за двое суток были мертвы. Теперь на красном пути прибор ищет самый молодой свод, чьи входы печати сходятся с отпечатком файл в файл, и правит одну строку ключом --perekommit.
• Проводник flangtutor принимает верные ответы. Значение урока читается из stdout, а не вместе с потоком ошибок, куда идёт вердикт доказанности; список слов языка в проводнике догнал таблицу лексера (649 фраз против 647), и проба проводника зелена целиком.
• Кириллических путей в дереве 5 вместо 67 (вне flang/proof — 4 вместо 66). Остаток назван в ведомости с доводом: четыре файла в flang/test называет сам flang/self, и имена уезжают в семя дословно, а letters.фп — проба расширения. Транслитные имена из flang/self тоже ушли: пять файлов (zapis.flang → proof-record.flang и ещё четыре) названы по-английски. Сторож отвечает «кириллица в путях: 5, все в ведомости — новых нет», код 0.

$ flang run-script cyrillic:check
кириллица в путях: 5, все в ведомости — новых нет                 код 0

• Заслоны роста судят правку, а не состояние дерева. Переименование файла больше не выглядит для них новым файлом: git --numstat отдаёт слитый путь docs/{прежний => новый}, и заслоны приводят его к новому пути. Порог схожести — 50 % (поправка к ADR-0053).
• Сторож кириллицы смотрит весь путь, а не последнее звено. Латинское имя файла в кириллическом каталоге прежде проходило молча; теперь приговор называет путь целиком.
• flangtutor выбирает локаль и awk прогоном. На машине, где /usr/bin/awk — это mawk, урок приходил мусором: mawk режет закрывающую «»» по байту. Теперь пара «локаль + awk» проверяется на целость UTF-8, а годной пары нет — краска снимается, и текст остаётся целым.
• Заслоны перестали врать молчанием. Заслон перед пушем обрывал проверку, молчащую дольше 200 с, и отвечал «проверки не запущены»: на выпускном диапазоне так не прогонялась ни одна из его 21 проверки (lint:growth молчит ~290 с). Предел молчания теперь 900 с. Сам заслон длинных строк просил у git весь дифф и упирался в предел вывода 1 МиБ на напечатанном семени из 685 001 строки — теперь он просит только те пять расширений, которые линтер умеет читать, и это проверено отрицательным контролем: без приставки :(top) путь не совпадает ни с чем и заслон зеленел бы молча.

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

• Теорема, гипотезы которой нет у утверждения, отвергается (5311). Раньше такая теорема доказывала утверждение слабее объявленного; программы, где это проходило, станут красными — и правильно.
• Завершаемость видит вызов через функцию-значение (3870). Функция, которая считалась тотальной только потому, что вызов шёл через значение, тотальной больше не считается.
• Постусловие с таких что цитируется только после снятия ограничения (4573): ссылка на него до снятия больше не принимается.
• Три кода отказа и указатель заметок получили английские имена. Кто сверялся со старыми строками кодов — поправить сверку.
• Приборы на shell и Python убраны (scripts/target-census.sh, Python-приборы доли доказанного). То же считают планы flang; старые пути вызова не работают.
• Пуш встаёт на линтере, если добавленная строка длиннее предела или тронутая функция глубже: пределы берутся из .flangrc дерева, а не из привычки.
• flang test отвечает кодом 3, когда блоки «прогон» не исполнены. Прежде файл с блоками прогон давал код 0 и слова «примеров 2, прошло 2» — заведомо ложное ожидание в блоке проходило молча. Теперь рядом со счётом примеров стоит строка «блоков «прогон» N, исполнено 0», а исход — «сделано, но проверено не всё». Сборочный сценарий, читавший ноль, станет красным, и правильно: блоки по-прежнему не исполняются (планировщик вне замыкания двоичного, задача 1104).
• 153 коротких команды живут в .flangrc и носят английские имена. В 0.7.23 ярлыков в файле настроек не было ни одного. Кто звал прежние русские имена, зовёт теперь английские: подсчёты:проверка → counts:check, тесты → tests, столкновения:проверка → link-collisions:check.

---

A linter in the language, a kernel memo, and three closed soundness holes

What appeared

• flang lint — line length and conditional depth, limits read from .flangrc. The keys are max-line-length and max-conditional-depth, and lint (refuse) says what to do about a violation. The pre-push gate judges your change only: an added line must fit the limit, a touched function must not be deeper. The tree does not meet the limits and no debt ledger is kept — that is the decision of ADR-0053: flang lint over the tree finds 32342 lines longer than 120 characters and 1365 functions nested deeper than 2, across 703 of 1301 files (measured 3 October 2026). This release's own change took 77 long lines out of the lines it touched and left the rest of the debt where it was.
• Short commands live in the settings file. flang run-script <name> takes its line from .flangrc; shortcuts no longer hide in a separate script, and flang run-script with no name prints the ones there are.
• A library profile in .flangrc. A program sees the standard-library modules the profile names: a smaller closure and no name clashes.
• A kernel memo: within one run a pure call is computed once. It speeds up proof checking and the seed print; in the printed C the memo is a wrapper around three kernel functions.
• The block literal """ strips the common indentation of its continuation lines (ADR-0052). Long text no longer has to start at column zero, and a long line in code is no longer a choice between the line limit and the truth.
• The library gained long division with remainder, gcd and exact rationals. The division and the gcd live in bignum.flang -- at 0.7.23 it had neither; its obligations are still 9, the new functions carry no postconditions. rationals.flang is a new file: fractions over long integers, 17 functions and 13 obligations (reduction, the four operations, comparison, a harmonic sum). fmath.flang is new as well, but it holds no functions -- four standalone statements about the length and the sum being non-negative, and nothing in the tree cites them yet.
• Reasoning in sentences: a proof is written as sentences, premises as assumptions (ADR-0050). A step names the kernel rule, not a line number.
• A guard for forgotten temporaries of checks. An untracked .flang-storozh-* directory, or a file with "probe" in its name, left in the tree after a killed run is reported with its path and exit code 1; the six places where a temporary has to live in the tree (the compiler resolves imported modules relative to the file) are named by the guard itself, with the reason.
• The decision about exact integers is written down, and their absence is held by a probe (ADR-0036, task 1908). Numbers in the language are still IEEE-754 doubles, and integers are exact up to 2^53-1. The set flang/proof/probes/exact-integer/ shows on every CI run that there is no exact integer in the language: the literal 42 stays a number and the kernel has no ring rules for it. The probe will turn red on the day one appears, and that is its job.

What changed

• The independent checker replays more. By-assumption steps from the statement's premises, property steps, citations across files, field projections, module types and dependency sets as the linker sees them, and what the kernel proves in your programs, not only in the language's own tree.
• An identity over an open term is no longer called a lie (4850). The move "substitute a term for itself" is accepted without evaluating anything, and a term that cannot be evaluated is reported as a place the run did not undertake (code 3) instead of a disagreement (code 1): a place the run did not check is not a lie.
• The independent checker has a strict key. It asks something else than the default: not "does the record contradict the source" but "is it proved at all". At least one obligation is required and every one of them must count as proved, otherwise the outcome is 3 with the reason named. On the nine programs of the strict probe set six answers of zero turned into three - the record for a program with a false postcondition among them, the one all three instruments used to accept with zero.
• A proof record that lags behind its source is refused, and the checker rebuilds itself when its source is newer than its binary: an old binary no longer judges new source silently.
• The tree's verdict is PROVABLE, and the probe suite under it has grown. The share replayed by the independent checker stands at 100.00 % — 650 obligations out of 650; the verdict's threshold is exactly 100 %, and the share meets it. Against 0.7.23 it is not the share that grew but the suite that holds it up: forgeries in the manifest 36 -> 38, forgery probes 575 -> 631, honest probes 274 -> 315, unreachable places carried out 27 -> 30, and the ratchet was raised with them. The verdict's four checks: the calculator is out of the checking program, the share is at or above the threshold, the probe suite passes, and the suite has not weakened. Measured by io scripts/provability.fscript --plan Verdict: for 0.7.23 the CI run of 29 September 2026 on main, for 0.7.24 the run of 3 October 2026 on the release branch.
• The tooling moved off shell and Python onto flang plans. Guards, probes and counting instruments are plans now; the pre-push gate refuses growth of shell, Python and stray markdown, and CI judges the commit message against the convention (prefix, subject length, ASCII only).
• The guide and the site are written in plain words. The README says what the language does and how to install it; docs/DESCRIPTION.md is no longer pinned to a release (the line "this description matches 0.7.23" is gone) and no longer prints numbers that change from build to build. No dated reports are left in the tree except two under docs/archive/, which the ROADMAP cites; 418 files left docs/ over this release.
• A date from a day count is right below year one. A correction written for truncation fired a second time under floor division, and day -719834 gave -719833. The round trip days -> date -> days now agrees on 1038 consecutive days at the era boundary, on 7240 days with step 1009 and on 4000 pseudorandom ones - zero disagreements.
• The seed fingerprint finds its own commit by content. It used to name a sha that died in a rebase, and the fast check refused with "the commit is unknown to the tree": four of five values over two days were dead. On the red path the instrument now looks for the youngest commit whose print inputs match the fingerprint file for file, and the --perekommit key rewrites that one line.
• The flangtutor guide accepts correct answers. A lesson's value is read from stdout alone, not together with the error stream that carries the proof verdict; the guide's list of language words caught up with the lexer table (649 phrases against 647), and the guide's probe is green as a whole.
• Five Cyrillic paths in the tree instead of 67 (four instead of 66 outside flang/proof). What is left is named in the ledger with a reason: four files in flang/test are named by flang/self itself and travel into the seed verbatim, and letters.фп is an extension fixture. The transliterated names in flang/self are gone as well: five files (zapis.flang -> proof-record.flang and four more) now carry English names. The guard answers "5 paths, all in the ledger — none new", exit 0.
• The growth gates judge the change, not the state of the tree. A rename no longer looks like a new file to them: git --numstat reports a fused path docs/{old => new}, and the gates resolve it to the new path. The similarity threshold is 50 % (an amendment to ADR-0053).
• The Cyrillic-name guard looks at the whole path, not the last segment. A Latin file name inside a Cyrillic directory used to pass in silence; the verdict now names the full path.
• flangtutor picks its locale and its awk by a run. On a machine where /usr/bin/awk is mawk the lesson arrived as garbage: mawk cuts the closing guillemet by byte. The pair (locale, awk) is now checked for keeping UTF-8 whole, and if no pair qualifies, painting is dropped and the text stays whole.
• The gates stopped lying by silence. The pre-push gate killed a check that stayed silent longer than 200 s and answered "checks not run": on this release's range not one of its 21 checks ran (lint:growth is silent for about 290 s). The silence budget is 900 s now. The line-length gate itself asked git for the whole diff and hit the 1 MiB output cap on a printed seed of 685001 lines -- it now asks only for the five extensions the linter reads, and that is held by a negative control: without the :(top) prefix the pathspec matches nothing and the gate would have gone quietly green.

What broke

• A theorem whose hypotheses the statement lacks is refused (5311). Such a theorem used to prove a statement weaker than the one declared; programs where that passed will now be red, and rightly so.
• Totality sees calls made through function values (3870). A function that counted as total only because the call went through a value no longer counts as total.
• A postcondition restricted by таких что is cited only once the restriction is discharged (4573): citing it earlier is no longer accepted.
• Three refusal codes and the note index got English names. If you matched the old code strings, fix the match.
• The shell and Python instruments are gone (scripts/target-census.sh, the Python instruments of the proved share). Flang plans count the same things; the old call paths no longer work.
• A push stops at the linter when an added line is longer than the limit or a touched function is deeper: the limits come from the tree's .flangrc, not from habit.
• flang test exits 3 when the scenario blocks have not been run. A file with прогон blocks used to exit 0 and say "2 examples, 2 passed", so a deliberately false expectation inside a block passed in silence. Next to the example count there is now a line "scenario blocks N, run 0", and the outcome is "done, but not everything was checked". A build script that read the zero will turn red, and rightly so: the blocks are still not executed (the scheduler is outside the binary's closure, task 1104).
• 153 shortcuts live in .flangrc and carry English names. At 0.7.23 the settings file held none. Whoever called the old Russian names now calls the English ones: подсчёты:проверка → counts:check, тесты → tests, столкновения:проверка → link-collisions:check.

---

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

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