Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .flangrc
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ script.proof-record:check = bootstrap/flang run-script seed:freshness --what pro
script.record-source:check = bootstrap/flang io scripts/guards/record-follows-its-source.fscript --plan Проверка
script.record-source:forgery = bootstrap/flang io scripts/guards/record-follows-its-source.fscript --plan Подлог
script.checker:check = bootstrap/flang io flang/proof/checker/tests/run.fscript --max-steps 4000000000 --timeout 600000
script.plan-rules:probe = bootstrap/flang io flang/proof/probes/plan-rules-asked/run.fscript --plan Binary
script.translation:check = sh flang/translation/run.sh
script.proved-share:check = bootstrap/flang io flang/proof/share-measure.fscript --max-steps 4000000000 --timeout 900000 -- --set corpus
script.proved-share:forgery = bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000
Expand Down
120 changes: 120 additions & 0 deletions docs/tasks/7706-the-check-command-never-asks-the-plan-judge.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,120 @@
---
номер: 7706
заголовок: Команда «check» идёт своей дорогой и судью планов на ней не спрашивают — двенадцать подделок отвечают кодом 0
статус: свободна
приоритет: P1
исполнитель: —
ветка: —
команда: первая
карта: Что мешает больше всего
рядом: 8398
нужность: тот же двоичный на том же файле: «test» отвергает подделку, «check» принимает её молча
---

# 7706. Команда «check» идёт своей дорогой и судью планов на ней не спрашивают

Правила над объявлением `план` написаны (`flang/self/io.flang`, модуль
«Проверка планов»), ввезены в замыкание и вызываются из
`«Проверить связанное»`. Но `flang check` идёт НЕ через неё: дорогу он
повторяет своим кодом в `repl_check_sources`
(`flang/src/emit/c/flang_repl.c`), вызов за вызовом, — и вызова планов в этом
списке нет.

Это ровно та же порода, что задача 7101 у процессов: слой едет в двоичном
пассажиром. Разбор задачи — в
[`docs/zettel/a-rule-inside-the-binary-is-not-a-rule-the-binary-asks.md`](../zettel/a-rule-inside-the-binary-is-not-a-rule-the-binary-asks.md).

## Шаги воспроизведения

1. Один и тот же файл двум судьям одного и того же двоичного:
`bootstrap/flang check flang/test/fixtures/plany/01-dvazhdy.flang`
и `bootstrap/flang test flang/test/fixtures/plany/01-dvazhdy.flang`.
2. Смотреть код возврата и есть ли в выводе `FLANG_PLAN`.
3. Спросить двоичный, есть ли в нём вызов:
`grep -c 'Проверить планы' bootstrap/flang_repl.c` и
`grep -c 'compiler_flang_proverit_plany(' bootstrap/compiler_flang.c`.

## Что происходит

```
$ bootstrap/flang check flang/test/fixtures/plany/01-dvazhdy.flang
модуль «План дважды»: функций 2, из них с доказанным завершением 2; типов 4
… проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет код 0

$ bootstrap/flang test flang/test/fixtures/plany/01-dvazhdy.flang
FLANG_PLAN в файле …/01-dvazhdy.flang, строка 25, столбец 1:
план «Работа» объявлен дважды код 1

$ grep -c 'Проверить планы' bootstrap/flang_repl.c
0
$ grep -c 'compiler_flang_proverit_plany(' bootstrap/compiler_flang.c
4
```

Четыре вхождения в напечатанном компиляторе — объявление, два вызова
(`«Проверить связанное»` и `«Замечания до ядра»`) и строка таблицы вызова по
имени. В `flang_repl.c` — ни одного, и так было всегда:
`git log --all -S 'Проверить планы' -- flang/src/emit/c/flang_repl.c` пуст.

Версия: flang 0.7.23. Дата прогона: 4 октября 2026.

## Что должно быть

Код 1 и названное сообщение правила на каждой из двенадцати подделок
`flang/test/fixtures/plany/01`…`12`, код 0 на целом образце `00`, и на
образце `13` — одно замечание проверки типов, а не два.

Числа и сообщения не предсказаны: вставка тихого вызова
`«Проверить планы»` сделана в копии дерева, двоичный пересобран, ответы сняты
прогоном и лежат построчно в
[`flang/proof/probes/plan-rules-asked/expected.tsv`](../../flang/proof/probes/plan-rules-asked/expected.tsv).

Заодно обязана перестать врать строка отчёта: в списке «ПРОВЕРЕНО» у
`--быстро` названы процессы и не названы планы (`flang_repl.c`, строка 8721).
Поверхность `plans` при этом УЖЕ стоит среди судимых («Все судимые ключи» в
`flang/self/bootstrap/compiler.flang`), поэтому фраза «сверены НЕ ДО КОНЦА»
не печатается вовсе — и ответ на подделке совпадает с ответом на целой
программе знак в знак. После правки эта запись станет правдой; сегодня она
ложь.

## Обходной путь

Есть: `flang test <файл>` на том же двоичном правила планов спрашивает и
подделку отвергает. Для файлов без примеров это чистая проверка.

## Когда задача сделана

1. `bootstrap/flang io flang/proof/probes/plan-rules-asked/run.fscript --plan Binary`
отвечает кодом 0: `plan-rules-asked: проб 29, разошлось 0`. Сегодня эта же
команда даёт код 1 и `разошлось 12` — проба и различает исправленный
двоичный от нынешнего.
2. Проба позвана не только короткой командой `plan-rules:probe`, но и шагом в
`.github/workflows/binary.yml` рядом с соседними наборами проб. Шаг
ставится ТЕМ ЖЕ коммитом, что и правка: до неё он красный.
3. Живые программы дерева с объявлением `план` по-прежнему проходят
`bootstrap/flang check`: правила не отвергают верное. Это уже замерено на
правленом двоичном: из 268 программ дерева с таким объявлением ответ
сменили РОВНО двенадцать — сами подделки. Таблица — в задаче 8398,
раздел «Правила не отвергают верное».

4. Дорогу `repl_check_sources` делят `flang check` и оболочка
(`repl_check`), поэтому одна вставка закрывает обе. Третий и четвёртый
судьи того же двоичного правила УЖЕ спрашивают: `flang test` и
`flang io` без `--на-веру` отвергают подделку сами
(`io … 03-sostoyanie-neizvestno.flang --plan Работа` → код 3,
«замечаний проверки 1, первое — FLANG_PLAN: состояние плана «Работа» —
неизвестный тип «Хода»»).

## Где живёт правка

`flang/src/emit/c/flang_repl.c`, функция `repl_check_sources`: тихий вызов
`«Проверить планы»` со слитыми в общий список бедами, рядом с таким же
вызовом процессов. Содержимое этого файла печать берёт из дерева
(`«Файл оболочки»` в `flang/self/emit-c.flang` читает его как
«исходник оболочки»), поэтому ПЕРЕПЕЧАТКА САМОСБОРНОЙ ЧАСТИ НЕ НУЖНА:
`bootstrap/compiler_flang.c` уже несёт и правила, и их вызов из
`«Проверить связанное»`. Доезжает правка той же вставкой в парную копию
`bootstrap/flang_repl.c` и `make -C bootstrap`.

Список «ПРОВЕРЕНО» у `--быстро` живёт в том же файле (строка 8721) — и его
правка перепечатки тоже не требует.
Loading
Loading