Repository navigation
fix(repl): the refusal names imported modules instead of denying a cause - #299
Merged
Merged
Conversation
The refusal of `run` on a program with exact fractions counts the whole closure and explains it from the entry file alone, so its last line says the opposite of the truth: "all statements are proved and the refusal does not come from them". Measured with the 0.7.24 binary. `run` on the probe: code 3, "22 statements, 20 proved, 2 on the grid". The probe's own report: claims 0, obligations 2, both discharged. bignum.flang, which arrives through Rationals: 9 statements, 7 proved, 2 on the grid, 18 obligations. So both grid statements live in the imported module, not in the probe. The mechanism, by name: unproven_list in flang/src/emit/c/flang_repl.c looks for the top-level arrays claims, laws and assumed and returns 0 silently when the key is absent; it is fed by the ledger of compiler.flang:1070, which is built from "only what belongs to the file" and "obligations of the entry file". One count walks the closure, the other one file -- and the last line of the refusal will lie on every program importing a module with a grid, which is 21 of the 23 files of the library.
The verdict counts the closure, the ledger counts the input file. On a program that imports a module with open goals the first count said "grid 2" and the second said zero items, so the last line of the refusal claimed every claim was proved and the refusal came from somewhere else. Measured on the exact-fractions probe: run said 22 claims, 20 proved, grid 2; the input file ledger said 0 items; both open goals sat in flang/stdlib/bignum.flang, which arrives through Rationals. 21 of 23 library files carry open goals, so the old line lied on nearly every importing program. Now that branch walks the sources of the ledger and prints the imported paths, with one command to ask each of them by name. Only paths, no per-module numbers: a second question to the ledger per module doubled the refusal from 19.8 s to 38.3 s on the same probe, so the numbers moved to task 2400, where one pass of the ledger pays for them. Three controls on the built binary: the probe names both modules at 19.70/19.80/19.83 s; a program with its own unproved claim still gets the old by-name list and code 3; a proved program prints 42 with code 0 and not one extra line. Runtime source, so the seed carries it by seed:refresh, not a reprint.
Taken on a dirty tree the fingerprint writes "tree edited by hand" and --bystro is red by design: it is unknown what the seed was printed from. Re-taken on the clean tree it names 86040ef, and both --telo and --bystro are green: 55 inputs, 7 files, 44464329 bytes.
The patch adds 48 lines to each twin of flang_repl.c, so three marks in docs/tree-inventory.md went stale and the gate caught all three: C total 882220 -> 882316, bootstrap 830152 -> 830200, print runtimes 52183 -> 52231. The task also needed an executor named: the ledger refuses a status that is not "free" with no one behind it.
Moving the branch onto the current trunk changed the sha of the commit the seed was printed from, not its content. The instrument says so itself and offers the repair: --perekommit re-finds the commit by the print inputs, file for file. 86040ef -> ffd09f2, and --bystro is green with 55 inputs, 7 files, 44464329 bytes.
the-homeless-god
force-pushed
the
a/7080-exact-fractions-run
branch
from
October 4, 2026 14:55
150f314 to
b8523ee
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Что было не так
Счёт вердикта идёт по замыканию, а поимённая ведомость — по входному
файлу. На программе, которая ввозит модуль с открытой сеткой, первый счёт
говорил «сетка 2», второй давал ноль пунктов, и последняя строка отказа
объявляла: «ни одного пункта: утверждения доказаны все, и отказ идёт не от
них». Это ложь, и она била почти на любой ввозящей программе — сетка есть у
21 файла библиотеки из 23.
Замер пробы на точных дробях (двоичный 0.7.24):
runcheck flang/stdlib/bignum.flang --proofОба открытых пункта лежали в
flang/stdlib/bignum.flang, который приезжаетчерез
Rationals.Что сделано
Ветка «список пуст» в
unproven_detailбольше не отрицает причину: онаобходит источники ведомости и называет ввезённые модули, а дальше одной
командой предлагает спросить каждый поимённо.
Если ни пунктов, ни ввезённых модулей нет — говорится именно это, а не «всё
доказано».
Чисел по модулю здесь нет, и это измерено, а не вкус. Первый вариант
правки спрашивал ведомость о каждом модуле и печатал
bignum.flang: утверждений 9, доказано 7, сетка 2— отказ рос с 19,8 с до 38,3 с, то естьвдвое. Платить вдвое на каждом отказе за то, что человек спросит одной
командой, нельзя. Числа ушли в новую задачу 2400: там они стоят одного
прохода ведомости, а не второго.
Три контроля на собранном двоичном
42, код 0, ни одной лишней строкиЧего в ветке нет
Правка живёт в рантайме (
flang/src/emit/c/**), поэтому до двоичного онадоезжает быстрым пересевом семени, а не перепечаткой на 2,5 часа.
Отпечаток снят на чистом дереве и называет коммит:
--teloи--bystroзелены, 55 входов, 7 файлов, 44 464 329 байт.
Три числа описи дерева подняты вслед за 48 новыми строками C в каждом из
близнецов
flang_repl.c— иначе краснеютprose-numbers-guardиtree-inventory, и они честно покраснели на первом заходе.Задача 7080 — статус «сделана с оговоркой». Отдельной строкой в ней записано
то, что стоит помнить: задача 2411 «отказ за недоказанное называет
утверждения» числится
doneи закрыта честно для того, что умела — называтьутверждения входного файла. Щель была в том, что счёт вердикта шёл по
замыканию. Закрытая задача не значит закрытой щели.