Repository navigation
flang 0.7.25 — Точное целое и точное дробное, предел потомку от поручения, страница реестра
Точное целое и точное дробное, предел потомку от поручения, страница реестра
Что появилось
- Точное целое — свой тип, не новое имя числа (ADR-0036; задачи 1908, 1412, 1413).
точное целоескладывается, вычитается, умножается и сравнивается без потолка 2^53; значение — список разрядов по основанию 2^22 без знака, канон (без старших нулей) держится при каждом действии, литерал не в каноне отвергается типизатором. Разрядное сложение напечатано во все десять целей печати. Ассоциативность сложения над ним доказывается правилом ядра — первым правилом кольца, у которого есть лемма в Lean и подлоги в пробах. - Точное дробное (ADR-0062; задача 5243). Пара точных целых — числитель над знаменателем, — сокращаемая при каждом действии;
плюс,минус,умножить на,делить наи порядок перекрёстным умножением; записанный литерал проверяется на канон (пара, канонические половины, непустой знаменатель, сокращённость); ниже нуля и деление на нулевую дробь — отказыFLANG_PROPERTYсвоим словом; счислоиточное целоене смешивается. Набор пробexact-fraction: 26 из 26, старое семя отвергает все 26. - Остаток над точным целым (
остаток от; задача 5245): шаг генератора glibc считается точно там, где double округляет произведение 1103515245·8388607. - Предел потомку называет поручение, а не хозяин (ADR-0061): поручение «Запустить процесс с пределом» (память в КиБ, срок в мс) и отклик «Процесс оборван», который приносит напечатанное до обрыва. Два стенда — предел памяти и смерть узла — переписаны с оболочки на планы.
- Страница реестра пакетов печатается из ведомости и выкладывается на Pages (ADR-0059): реестр — ведомость имён, а не склад кода.
checkспрашивает судью планов: двенадцать подложных планов, которые раньше проходили проверку, теперь отвергаются.- Экспериментальный каталог
flang/experimental/: русская морфология для силлогизмов и демо, которое заполняет словарь и судит текст. - У каждого приёма сверщика — теорема в Lean либо строка долга (ADR-0064; задача 4791). Список приёмов
шаг_выводаснимается сchecker.cприбором, а не пишется прозой: приёмов 83, в приёмке Lean 78, пять стоят строками долга с номером задачи. Н6 и О9, девять дней жившие без теоремы, вошли в приёмку; сторожlean-rules:checkидёт на каждый пуш и краснеет в обе стороны, его три подлога — в CI. Побочно закрыта дыра: разбор случаев принимал ложное постусловие, подставляя условие текстом под связыватель; сверщик теперь отказывает.
Что изменилось
- Напечатанный Makefile называет заголовки каждого объекта (задача 7182): правка
.hпересобирает зависящие объекты; до семени это доехало второй печатью подряд — печать Makefile принадлежит печатнику, а не исходникам. - Семя перепечатано пять раз за двое суток, цена одной печати на gpu — 79–83 минуты (ведомость
docs/reprint-ledger.tsvдополнена пятью строками); отпечаток входов печати называет коммит-источник семени. - ADR «предел чужому процессу» получил номер 0061 — номер 0056 на стволе уже занят замерами кванторов; семь ссылок переехали.
- 122 добавленные строки длиннее 120 знаков укорочены без обхода сторожа роста: списки разборщика разорваны после запятых, куски таблиц лексера разнесены, примеры стендов и трёх сторожей переехали на функции-близнецы, описывающие ответ списком; значения примеров сняты прогоном.
- Отчёт С-2 сторожа ведомости правил называет число правил одной строкой, а разбивку по ADR — следующей; строка С-6 о бюджете checker.c короче на семь слов.
- Страница дорожной карты — датированный план до 1.0. Таблица помесячно с октября 2026 по апрель 2027, вехи 0.7.25, 0.8, 0.9 и 1.0, семь условий выпуска 1.0 и то, что решено не делать; прежний текст без дат снят.
- ADR-0067 о двоичных выпусках — предложено, кода нет. Выпуск будет нести готовые двоичные для четырёх троек с одним
SHA256SUMS; пять задач (7959, 8128, 1710, 1504, 1098) и пять решений ждут владельца. Имена из решения, которых в исходниках нет, стоят в реестре «объявлено, не сделано».
Что сломалось
- Над двумя точными целыми отказ деления теперь перечисляет четыре действия, а не три: «плюс», «минус», «умножить на» и «остаток от». Пробы, ждавшие прежнее слово, пересняты.
- Дробь не входит ни в одну из десяти целей печати — эмиттеры её не знают; программа с
точное дробноепечатается только толкователем. Ключевого слова для целой части дроби нет;docs/flang/SPEC.mdиDESCRIPTION.mdне описывают ни точного целого, ни дробного — долг назван в ADR-0062 §6.
Exact integer and exact fraction, a child's limit named by the order, the registry page
What appeared
- The exact integer is a type of its own, not a new name for number (ADR-0036; tasks 1908, 1412, 1413).
exact integeradds, subtracts, multiplies and compares without the 2^53 ceiling; a value is a list of base-2^22 digits without sign, the canon (no leading zeros) holds at every action, a non-canonical literal is refused by the typechecker. Digit addition is printed into all ten targets. The associativity of its addition is proved by a kernel rule, the first ring rule with a Lean lemma and forgery probes. - The exact fraction (ADR-0062; task 5243). A pair of exact integers, numerator over denominator, reduced at every action;
plus,minus,times,divided byand the order by cross multiplication; a written literal is checked for canon (a pair, canonical halves, non-empty denominator, reduced); below zero and division by the zero fraction areFLANG_PROPERTYrefusals by word; it does not mix withnumberorexact integer. Probe setexact-fraction: 26 of 26; the previous seed refuses all 26. - The remainder over exact integers (
остаток от; task 5245): the glibc generator step is exact where double rounds the product 1103515245*8388607. - A child's limit is named by the order, not by the host (ADR-0061): the order 'run a process with a limit' (memory in KiB, time in ms) and the reply 'process cut off', which carries what was printed before the cut. Two benches, the memory limit and the node death, move from shell to plans.
- The package registry page is printed from the ledger and published on Pages (ADR-0059): the registry is a ledger of names, not a store of code.
checkasks the plan judge: twelve forged plans that used to pass are refused.- The experimental directory
flang/experimental/: Russian morphology for syllogisms and a demo that fills the dictionary and judges a text. - Every checker move has a Lean theorem or a debt row (ADR-0064; task 4791). The list of
шаг_выводаmoves is taken fromchecker.cby an instrument, not written in prose: 83 moves, 78 in the Lean acceptance, five stand as debt rows with a task number. Н6 and О9, nine days without a theorem, enter the acceptance; thelean-rules:checkguard runs on every push, goes red both ways, and its three forgeries run in CI. A hole closed on the way: a case split accepted a false postcondition by pasting the condition as text under a binder; the checker now refuses.
What changed
- The printed Makefile names each object's headers (task 7182): editing a
.hrebuilds the dependent objects; it reached the seed only on the second print in a row, because the Makefile is printed by the printer, not by the sources. - The seed was reprinted five times in two days, one print on gpu costs 79-83 minutes (five rows added to
docs/reprint-ledger.tsv); the print fingerprint names the commit the seed came from. - The 'limit for a foreign process' decision is ADR-0061 — number 0056 on the trunk was already taken by the quantifier measurements; seven references moved.
- 122 added lines longer than 120 characters were shortened without bypassing the growth guard: parser lists broken after commas, lexer table pieces split, bench and guard examples moved to twin functions that render the answer as a list; example values are measured, not predicted.
- The C-2 report of the rule-ledger guard names the rule count on one line and the per-ADR breakdown on the next; the C-6 line about the checker.c budget is seven words shorter.
- The roadmap page is a dated plan to 1.0. A month-by-month table from October 2026 to April 2027, milestones 0.7.25, 0.8, 0.9 and 1.0, seven conditions for 1.0 and what is ruled out; the undated text is gone.
- ADR-0067 on binary releases is proposed, no code. A release will ship binaries for four triples with one
SHA256SUMS; five tasks (7959, 8128, 1710, 1504, 1098) and five decisions await the owner. The names of the decision that no source knows stand in the register of names declared and not made.
What broke
- The division refusal over two exact integers now lists four actions, not three: plus, minus, times and remainder. Probes expecting the old word are re-taken.
- The fraction enters none of the ten print targets — the emitters do not know it; a program with
exact fractionruns only in the interpreter. There is no keyword for the integer part of a fraction;docs/flang/SPEC.mdandDESCRIPTION.mddescribe neither exact type — the debt is named in ADR-0062 §6.
Страница выпусков: по-русски · in English.
Архив flang-0.7.25-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.