From 0ef34ac59f3d31df79e40d8395d4113f6ad83135 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Sun, 27 Sep 2026 19:42:01 +0000 Subject: [PATCH 1/4] refactor(probes): run the probe sets from plans Every probe set under flang/proof/probes now runs from an io plan (run.fscript) that reads its expected.tsv; the four shell runners are removed. Shared table walking lives in flang/proof/probes/table.fscript. Each expected.tsv keeps one header row with English column names and data rows only; the explanations moved into the owning task files. The syllogism set has two plans in one file: Binary and JavaScript. CI steps call the plans directly and carry no comments. Co-Authored-By: Claude Opus 5.5 --- ...-verdict-and-refuse-an-unproved-program.md | 4 +- ...yllogism-gets-one-surface-word-not-four.md | 6 +- docs/guide/settings.ru.md | 2 +- docs/site/cli.md | 2 +- docs/site/cli.ru.md | 2 +- ...-syllogism-should-read-like-a-syllogism.md | 218 +++++++++++++ ...2-strict-mode-tells-four-verdicts-apart.md | 111 +++++++ ...e-given-arguments-from-the-command-line.md | 28 ++ ...-by-the-binary-and-hidden-by-the-script.md | 91 ++++++ ...-verdict-and-refuse-an-unproved-program.md | 71 +++++ ...osts-screen-is-the-controlling-terminal.md | 2 +- flang/proof/probes/orders/expected.tsv | 9 + flang/proof/probes/orders/run.fscript | 190 +++--------- flang/proof/probes/run/expected.tsv | 34 +- flang/proof/probes/run/run.fscript | 54 ++++ flang/proof/probes/run/run.sh | 115 ------- flang/proof/probes/screen-size/expected.tsv | 40 +-- flang/proof/probes/screen-size/run.fscript | 245 +++------------ flang/proof/probes/screen/expected.tsv | 61 ++-- flang/proof/probes/screen/run.fscript | 237 +++----------- flang/proof/probes/strict/expected.tsv | 26 +- flang/proof/probes/strict/run.fscript | 47 +++ flang/proof/probes/strict/run.sh | 105 ------- flang/proof/probes/syllogism/expected.tsv | 56 +--- flang/proof/probes/syllogism/run.fscript | 176 +++++++++++ flang/proof/probes/syllogism/run.sh | 137 -------- flang/proof/probes/table.fscript | 292 ++++++++++++++++++ flang/proof/probes/unproven/expected.tsv | 66 ++-- flang/proof/probes/unproven/run.fscript | 67 ++++ flang/proof/probes/unproven/run.sh | 109 ------- .../scripts/run-verdict-targets-not-named.tsv | 2 - scripts/ledgers/proved-share-ledger.txt | 1 - 32 files changed, 1378 insertions(+), 1228 deletions(-) create mode 100644 flang/proof/probes/orders/expected.tsv create mode 100644 flang/proof/probes/run/run.fscript delete mode 100755 flang/proof/probes/run/run.sh create mode 100644 flang/proof/probes/strict/run.fscript delete mode 100755 flang/proof/probes/strict/run.sh create mode 100644 flang/proof/probes/syllogism/run.fscript delete mode 100755 flang/proof/probes/syllogism/run.sh create mode 100644 flang/proof/probes/table.fscript create mode 100644 flang/proof/probes/unproven/run.fscript delete mode 100644 flang/proof/probes/unproven/run.sh diff --git a/docs/adr/0045-run-and-io-print-the-verdict-and-refuse-an-unproved-program.md b/docs/adr/0045-run-and-io-print-the-verdict-and-refuse-an-unproved-program.md index bfa20c0e6..08da66e0e 100644 --- a/docs/adr/0045-run-and-io-print-the-verdict-and-refuse-an-unproved-program.md +++ b/docs/adr/0045-run-and-io-print-the-verdict-and-refuse-an-unproved-program.md @@ -17,8 +17,8 @@ **Основание:** задача 8222; замеры 17 сентября 2026 на копии `wK1` (ветка `a/8222-run-verdict`, двоичный `bootstrap/flang` 0.7.19 из семени 12 сентября): «до» — `sh flang/proof/probes/run/run.sh`, «после» — то же с `--зондом`. -**Проверяется:** `sh flang/proof/probes/run/run.sh --зондом` до перепечатки семени; -`sh flang/proof/probes/run/run.sh` — после неё и правки хозяина. +**Проверяется:** `bootstrap/flang io flang/proof/probes/run/run.fscript --plan Binary`; +до перепечатки семени проверялось толкованием исходников, `run.sh --зондом`. --- diff --git a/docs/adr/0047-a-syllogism-gets-one-surface-word-not-four.md b/docs/adr/0047-a-syllogism-gets-one-surface-word-not-four.md index 5eb0b46e6..ea0e0d6dc 100644 --- a/docs/adr/0047-a-syllogism-gets-one-surface-word-not-four.md +++ b/docs/adr/0047-a-syllogism-gets-one-surface-word-not-four.md @@ -15,9 +15,9 @@ правка ядра; [ADR-0023](0023-forgeries-live-in-a-set-not-in-the-metric-corpus.md) — набор подделок; [ADR-0045](0045-run-and-io-print-the-verdict-and-refuse-an-unproved-program.md) — вердикт при запуске. -**Проверяется:** `sh flang/proof/probes/syllogism/run.sh` (замер «до», двоичным) и -`sh flang/proof/probes/syllogism/run.sh --печатью` (замер «после», исправленным -компилятором, напечатанным в JavaScript); `./ярлык слово:занятость`. +**Проверяется:** `bootstrap/flang io flang/proof/probes/syllogism/run.fscript --plan Binary` +(двоичным) и тот же файл с `--plan JavaScript` (компилятором, напечатанным в +JavaScript; каталог печати — в `PRINTED_COMPILER`); `./ярлык слово:занятость`. **Номер сменён 22 сентября 2026:** черновик носил номер 0046, но пока партия лежала невлитой, 0046 занял ADR о переименовании каталога доказательств, влитый в ствол diff --git a/docs/guide/settings.ru.md b/docs/guide/settings.ru.md index fe33b7db2..9cd0d2449 100644 --- a/docs/guide/settings.ru.md +++ b/docs/guide/settings.ru.md @@ -128,7 +128,7 @@ allow — запустить, вердикта не считая. ``` Пробы всех исходов — `flang/proof/probes/unproven/` -(`sh flang/proof/probes/unproven/run.sh`). +(`bootstrap/flang io flang/proof/probes/unproven/run.fscript --plan Binary`). ## Где файл ищется diff --git a/docs/site/cli.md b/docs/site/cli.md index 84bdb11c6..01391b5fc 100644 --- a/docs/site/cli.md +++ b/docs/site/cli.md @@ -181,7 +181,7 @@ The key is only meaningful next to `--proof`: `flang check <файл> --стро without it exits `2`. Probes for all four outcomes and for the default are in -`flang/proof/probes/strict/` (`sh flang/proof/probes/strict/run.sh`). +`flang/proof/probes/strict/` (`bootstrap/flang io flang/proof/probes/strict/run.fscript --plan Binary`). ```bash $ flang check привет.flang diff --git a/docs/site/cli.ru.md b/docs/site/cli.ru.md index 091dcf003..f9070a80e 100644 --- a/docs/site/cli.ru.md +++ b/docs/site/cli.ru.md @@ -177,7 +177,7 @@ flang check <файл.flang> [--proof [--json] [--строго] [--записа код `2`. Пробы всех четырёх исходов и умолчания — `flang/proof/probes/strict/` -(`sh flang/proof/probes/strict/run.sh`). +(`bootstrap/flang io flang/proof/probes/strict/run.fscript --plan Binary`). ```bash $ flang check привет.flang diff --git a/docs/tasks/5309-a-syllogism-should-read-like-a-syllogism.md b/docs/tasks/5309-a-syllogism-should-read-like-a-syllogism.md index e28b21284..d06641336 100644 --- a/docs/tasks/5309-a-syllogism-should-read-like-a-syllogism.md +++ b/docs/tasks/5309-a-syllogism-should-read-like-a-syllogism.md @@ -343,3 +343,221 @@ JavaScript, — `доказано 3`, `ни одного шага`, `не пол Заодно снята устаревшая оговорка у проб размера экрана в том же файле: там стояло «ЖДЁТ ПЕРЕПЕЧАТКИ СЕМЕНИ… шаг КРАСЕН по названному долгу». Перепечатка прошла; замер 26 сентября — **сошлось 6 проб из 6**, код 0. + +## 27 сентября 2026: прогонщики проб — планы, таблицы — данные + +Прогонщик набора — план `run.fscript`; общая часть всех наборов лежит в +`flang/proof/probes/table.fscript`. Таблица `expected.tsv` — строка заголовка с +английскими именами столбцов и строки данных; прочерк `-` в ячейке значит +«ничего». Объяснения, стоявшие в шапках таблицы, прогонщика на оболочке и над +шагом CI, перенесены сюда дословно; старые имена столбцов и файлов в них — +того времени. + +Вызов: `bootstrap/flang io flang/proof/probes/syllogism/run.fscript --plan Binary`. Код 0 — сошлось всё; 1 — расхождение, и оно названо +строкой; 3 — смотреть было нечем (нет двоичного, нет таблицы, проба убита). +Переменная среды `FLANG_BIN` подменяет двоичный. + +Столбцы: `program`, `binary` (слово в ответе двоичного), `javascript` (слово в ответе компилятора, напечатанного в JavaScript). Код возврата у этого набора не сверяется, сверяется слово. + +### Что стояло в шапке таблицы + +``` +ПРОБЫ СИЛЛОГИЗМА (ADR-0047, задача 5309). + +Поля: программа, слово, которое обязано стоять в ответе ДВОИЧНОГО, слово, +которое обязано стоять в ответе НАПЕЧАТАННОГО КОМПИЛЯТОРА. Слово, а не код: +напечатанный компилятор отвечает строкой JSON, а не кодом возврата, и сверять +оба одной меркой честнее, чем двумя разными. + +── ДВА СТОЛБЦА, И ТЕПЕРЬ ОНИ ЖДУТ ОДНОГО И ТОГО ЖЕ ───────────────────────── +Слово `следует` живёт в `flang/self/lexer.flang` и `flang/self/parser.flang`, +а починка распаковки `таких что` — в `flang/self/proofterm.flang`; всё это +печатаемая часть семени, и до перепечатки двоичный слова НЕ ЗНАЛ. Столбец +«двоичный» тогда ждал от него ровно отказа разбора — это был замер «до». + +ПЕРЕПЕЧАТКА ПРОШЛА 25 сентября 2026 (выпуск 0.7.22, заход 23–25 сентября, +35 часов 45 минут), и замер «до» кончился вместе с ней: двоичный теперь несёт +и слово, и починку. Столбец «двоичный» сведён с двоичным прогоном 26 сентября +2026 на дереве `gh/dev` `d5e203b89` — сошлись все шесть строк, и в каждой +двоичный говорит ровно то же, что печатанный в JavaScript компилятор. + +ПОЧЕМУ СТОЛБЦЫ НЕ СЛИТЫ В ОДИН. Раз они совпали, таблица стала сверкой ДВУХ +РЕАЛИЗАЦИЙ на одних программах: двоичный и компилятор, напечатанный в +JavaScript (`run.sh --печатью`), обязаны отвечать одинаково. Разойдись они — +красна будет та сторона, которая ушла, и видно это будет по столбцу. Слей их +в один — и расхождение двух реализаций перестанет быть заметно вовсе. + +── ЧТО СТЕРЕЖЁТ КАЖДАЯ СТРОКА ────────────────────────────────────────────── +честный — силлогизм сахарной записью доказывается: три утверждения, все + доказаны, шаг закрыт приложением посылки; +изъятие — ФАЛЬСИФИКАТОР задачи 5309 в его переписанном виде: та же + программа без посылки. Заключение обязано перестать доказываться. + Код 0 здесь — задача не сделана; +подделка — заключение ВЕРНО («ни один человек не крылат» — правда), но из + названной посылки не следует. Отвергнуть его может только правило + приложения, и оно обязано это сделать; +цепочка — две посылки, вторая с ограничением `таких что`. До правки + `flang/self/proofterm.flang` (распаковка `expr`, ADR-0047) ядро + отвечало «ограничение «таких что» после подстановки не выведено»; + строка стережёт, чтобы оно не вернулось. A/B снято 20 сентября + 2026 на ОДНОЙ печати: та же сборка с откаченной строкой отвечает + прежним отказом, с правкой — «доказано 5»; +изъятие-жёсткое — ДЫРА, а не проверка, и стоит она здесь нарочно. Снесены и + посылка, и вывод; остаётся заключение и предикат со своим + постусловием «всякий человек смертен» — и заключение всё равно + ДОКАЗАНО, код 0. Значит в этой форме оно от посылки не зависит: + посылка и постусловие предиката говорят одно и то же дважды, а + ядро берёт постусловие. Строка ходит храповиком: пока она ждёт + «доказано», дыра открыта и названа; закроется — ожидание меняется + вместе с задачей 5309; +условный — цена закрытия той дыры. У предиката снято постусловие, и тогда + заключение выводится ТОЛЬКО через посылку (изъятие посылки роняет + его), но сама посылка становится «объявлено, не доказано», и весь + файл уходит кодом 3 со словами «доказано ПРИ УСЛОВИИ». Выбор между + этими двумя строками — не про слово поверхности, и ни один сахар + его не снимает. +``` + +### Что стояло в шапке прогонщика на оболочке + +``` +ПРОБЫ СИЛЛОГИЗМА (ADR-0047, задача 5309). + + sh flang/proof/probes/syllogism/run.sh двоичным: замер «до» + sh flang/proof/probes/syllogism/run.sh --печатью компилятором, напечатанным + в JavaScript: замер «после» + PECHAT=<каталог> sh … --печатью взять уже напечатанный компилятор оттуда, + а не печатать заново (печать — 13 минут) + +Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; +2 — не смог измерить (нет двоичного, нет таблицы, нет node). + +── ДВА ПУТИ, И ПОЧЕМУ ИХ ДВА ─────────────────────────────────────────────── +Слово поверхности `следует` живёт в печатаемой части семени +(`flang/self/lexer.flang`, `flang/self/parser.flang`), и там же живёт починка +распаковки `таких что` (`flang/self/proofterm.flang`). Правка там доезжает до +`bootstrap/flang` только полной перепечаткой. ПЕРЕПЕЧАТКА ПРОШЛА 25 сентября +2026 (выпуск 0.7.22): двоичный теперь знает и слово, и починку, и первый путь +спрашивает у него ВЕРДИКТ, а не отказ разбора. Замер «до» кончился вместе с +перепечаткой; чем он был и что показывал — в шапке expected.tsv. + +Второй путь ПЕЧАТАЕТ КОМПИЛЯТОР В JAVASCRIPT и спрашивает уже его. Теперь это +не «замер после», а ВТОРОЙ СУДЬЯ: две реализации на одних программах обязаны +отвечать одинаково, и таблица ждёт от них одних слов. Цена снята 20 сентября +2026 на машине `dev`: печать — 12 мин 50 с и 12,9 ГиБ один раз, 14,8 МБ JS; +дальше каждая проба — СЕКУНДЫ. Способ и обе его ямы описаны заметкой +docs/zettel/a-compiler-printed-to-javascript-runs-a-new-target-in-seconds.md. + +── ПОЧЕМУ НЕ ЗОНДОМ, КАК У `пробы-запуска` ──────────────────────────────── +Пробовали, и это замер, а не мнение. Зонд ведомости +(`flang/self/bootstrap/zond-k7.flang`, «Ведомость исходников», толкование +исходников нынешним двоичным) на этих же программах НЕ ДОСЧИТАЛСЯ ЗА +ОДИННАДЦАТЬ ЧАСОВ и был снят сигналом 15, пик 24,7 ГиБ — три программы разом, +19–20 сентября 2026. То есть путь дороже самой перепечатки, ради обхода +которой он заведён. Дешёвая его половина жива: разбор без доказательств +(`zond-5309.flang`, «Печать разбора исходника») — две минуты и 1 ГиБ, и +именно ею снято сличение деревьев в ADR-0047. + +Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах. +``` + +### Что стояло над шагом CI + +``` +ПРОБЫ СИЛЛОГИЗМА. Набор лежал с 20 сентября 2026 и НЕ ЗВАЛСЯ НИОТКУДА: +ни один workflow его не трогал, и 25 сентября, после перепечатки семени, +все шесть проб разошлись с таблицей молча — таблица ждала от двоичного +отказа разбора слова `следует`, а он его уже знал. Проверка, которую +никто не зовёт, ничего не проверяет; поэтому шаг здесь. Замер 26 сентября +2026: шесть проб, около двух секунд на всё — той же ценой, что соседи. +``` + +### Второй путь — план «JavaScript» + +``` +bootstrap/flang emit flang/self/bootstrap/compiler.flang --target js --no-check \ + --max-steps 200000000 --out <каталог> +PRINTED_COMPILER=<каталог> bootstrap/flang io flang/proof/probes/syllogism/run.fscript --plan JavaScript +``` + +Каталог называется полным путём. Печать компилятора план сам не запускает: +хозяин `flang io` снимает дочерний процесс на тридцатой секунде, а печать идёт +около 13 минут. Без переменной `PRINTED_COMPILER` план отвечает кодом 3 и +`FLANG_PROBE_SYLLOGISM_CANNOT_LOOK`. Запрос к напечатанному компилятору план +собирает сам и кладёт в тот же каталог файлом `request-<программа>.json`; ни +`python3`, ни оболочка для этого больше не нужны, нужен `node`. Слово ищется в +ответе целиком, а не в отдельном его поле. + +Замер 27 сентября 2026 на `gh/dev` `d88fb4efb`, двоичный собран из этого же +дерева, компилятор напечатан из него же: оба плана — проб 6, разошлось 0, код 0; +прогонщик на оболочке до правки давал те же числа обоими путями. + +### Наборы без своей задачи: экран и размер экрана + +Наборы `flang/proof/probes/screen/` и `flang/proof/probes/screen-size/` +заведены без задачи, поэтому объяснения их таблиц лежат здесь. + +Столбцы `screen`: `program`, `environment` (`terminal` или `pipe`), `keys`, +`input` (что подать клавишами; `\033` и прочее разворачивает `printf %b`), +`code`, `word`. + +``` +Пробы ЭКРАНА двоичного хозяина: поручения «Показать» и «Ждать событие». +Поля: программа, среда (терминал|труба), ключ (- — без ключей), ввод (что +подать клавишами; `-` — не подавать ничего, \033 и прочее разворачивает +printf %b), ожидаемый код возврата, слово, которое обязано стоять в выводе. + +СРЕДА ЗНАЧАЩАЯ, и в этом весь уговор: экран двоичного — управляющий терминал, +и там, где вывод уведён в трубу, в файл, в CI или под nohup, ответ обязан +остаться прежним отказом FLANG_IO_NO_SCREEN. Строка «труба» — не украшение +набора, а фальсификатор: позеленей она кодом 0, и правка молча поменяла бы +ответ всем неинтерактивным прогонам дерева. + +Терминал даёт `script -qec … /dev/null` — псевдотерминал без записи сеанса. +Клавиши подаются с задержкой в секунду: до первого «Ждать событие» терминал +ещё в построчном режиме, и знаки вроде 0x7F съела бы его же построчная +правка, не доехав до хозяина. +``` + +Столбцы `screen-size`: `program`, `environment`, `width`, `height`, `keys`, +`code`, `word`. + +``` +Пробы РАЗМЕРА ЭКРАНА двоичного хозяина: поручение «Размер экрана». +Поля: программа, среда (терминал|труба), ширина и высота псевдотерминала +(`-` — не задавать), ключ (`-` — без ключей), ожидаемый код возврата, слово, +которое обязано стоять в выводе. + +РАЗМЕР ЗАДАЁТСЯ НАБОРОМ, А НЕ БЕРЁТСЯ КАКОЙ ПРИДЁТСЯ, и это не удобство: +`script -qec … /dev/null` заводит псевдотерминал размером с родительский, а у +прогона под CI, под nohup и под этим набором родительского терминала нет — +размер вышел бы 0×0 на одной машине и 204×52 на другой, и проба сверяла бы +числа сама с собой. Здесь размер ставит `stty cols … rows …` внутри того же +псевдотерминала, и ожидаемые числа набраны рядом: сходятся они с тем, что +отдаст `stty size` в том же сеансе, знак в знак. + +ДВЕ СТРОКИ С РАЗНЫМИ ЧИСЛАМИ (80×24 и 132×50) — не повтор: одна проверяет, +что размер вообще приходит, вторая — что он ЧИТАЕТСЯ у терминала, а не +набран в хозяине. Оставь хозяин зашитые 80×24, и вторая строка покраснеет. + +СТРОКА 0×0 — ФАЛЬСИФИКАТОР ПРАВИЛА «не выдумывать 80×24»: так отвечает +терминал без рамки (и ровно так — псевдотерминал без родителя). Ответ обязан +быть отказом FLANG_IO_NO_SCREEN, а не придуманным размером; позеленей она +кодом 0, и хозяин молча врал бы всякому, кто считает кадр. + +СТРОКА «труба» стережёт совместимость: там, где вывод уведён в трубу, в файл, +в CI или под nohup, экрана нет и ответ прежний — FLANG_IO_NO_SCREEN. +Строки с `--no-screen` стерегут порядок проверок: полномочие спрашивается +ДО терминала, поэтому и в трубе, и в терминале ответ один — FLANG_IO_DENIED. +``` + +Что стояло над шагом CI «Check screen size»: + +``` +ПЕРЕПЕЧАТКИ ЖДАЛ И ДОЖДАЛСЯ. Слово «Размер экрана» заведено в словарь +22 сентября 2026, и прежний двоичный его не знал — шаг был КРАСЕН по +названному долгу. Печать прошла 25 сентября 2026 (выпуск 0.7.22); замер +26 сентября на дереве `gh/dev` `d5e203b89`: сошлось 6 проб из 6, код 0. +``` + +Набор `screen` из CI не зовётся: ему нужен псевдотерминал и 53 секунды. diff --git a/docs/tasks/5502-strict-mode-tells-four-verdicts-apart.md b/docs/tasks/5502-strict-mode-tells-four-verdicts-apart.md index ebef5a8e4..242e80c99 100644 --- a/docs/tasks/5502-strict-mode-tells-four-verdicts-apart.md +++ b/docs/tasks/5502-strict-mode-tells-four-verdicts-apart.md @@ -611,3 +611,114 @@ expected.tsv | sort -u | wc -l`). Число отстало ещё до этог ещё не закоммичена, и `sh scripts/bootstrap-reprint.sh --bystro` на нём красный (в CI этот шаг `continue-on-error`). Лечится пересъёмкой отпечатка из чистой копии после влития: `sh scripts/bootstrap-reprint.sh --otpechatok`. + +## 27 сентября 2026: пробы строгого режима идут планом + +Прогонщик набора — план `run.fscript`; общая часть всех наборов лежит в +`flang/proof/probes/table.fscript`. Таблица `expected.tsv` — строка заголовка с +английскими именами столбцов и строки данных; прочерк `-` в ячейке значит +«ничего». Объяснения, стоявшие в шапках таблицы, прогонщика на оболочке и над +шагом CI, перенесены сюда дословно; старые имена столбцов и файлов в них — +того времени. + +Вызов: `bootstrap/flang io flang/proof/probes/strict/run.fscript --plan Binary`. Код 0 — сошлось всё; 1 — расхождение, и оно названо +строкой; 3 — смотреть было нечем (нет двоичного, нет таблицы, проба убита). +Переменная среды `FLANG_BIN` подменяет двоичный. + +Столбцы: `program`, `keys`, `code`, `word`. + +### Что стояло в шапке таблицы + +``` +ЧЕТЫРЕ ИСХОДА СТРОГОГО РЕЖИМА (задача 5502, пункт 5 внешнего аудита). + +Поля: программа, ключи (через пробел, «—» — без ключей), ожидаемый код +возврата, слово, которое обязано стоять в выводе. Слово проверяется вместе с +кодом нарочно: смена причины при том же коде — тоже расхождение, а не тишина +(тот же довод, что у flang/proof/checker/tests/programs/lie-verdict.sh). + +ДВЕ ПОЛОВИНЫ ТАБЛИЦЫ, И ОБЕ ОБЯЗАТЕЛЬНЫ. +· Строки без «--строго» — УМОЛЧАНИЕ. Оно правкой 5502 не тронуто ни на знак, и + эти строки стерегут именно это: пять программ, у которых умолчание отвечает + ровно как до правки. Разъехалось умолчание — сломано всё дерево разом. +· Строки с «--строго» — сам строгий режим. Ноль в нём допустим ТОЛЬКО у + «honest.flang»: у неё у каждого утверждения вердикт «доказано». + +ФАЛЬСИФИКАТОР задачи стоит первой парой строк: «false-postcondition.flang» лжёт +постусловием («результат не больше 100» при теле «н плюс н»), и до правки ноль +ей давали ВСЕ три прибора. Даст строгий режим ноль ей снова — задача не +сделана. +``` + +### Что стояло в шапке прогонщика на оболочке + +``` +ПРОБЫ СТРОГОГО РЕЖИМА (задача 5502, пункт 5 внешнего аудита). + + sh flang/proof/probes/strict/run.sh + FLANG_BIN=<путь> sh flang/proof/probes/strict/run.sh + +Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; +2 — не смог измерить (нет двоичного, нет таблицы). + +── ЧТО ЗДЕСЬ СТЕРЕЖЁТСЯ ──────────────────────────────────────────────────── +Внешний аудит, пункт 5, требует различать четыре исхода — «доказано», +«опровергнуто», «не удалось доказать», «не поддерживается» — и запрещает +успех без независимой проверки всех обязательств. Словами все четыре были +названы и раньше; кодами возврата они не разъезжались, и два разных исхода +ехали нулём. Сборочный сценарий читает `$?`, а не слова. + +ДЫРА, СНЯТАЯ ПРОГОНОМ 19 сентября 2026 (двоичный из этого дерева). Программа +`programs/false-postcondition.flang` лжёт постусловием: обещает «результат не +больше 100» при теле `н плюс н`, и опровергается на н = 100. Ответы приборов +ДО правки: + + flang check код 0 + flang check --proof код 0 ПРОВЕРЕНО С ОПОРОЙ, И ОПОРА + НЕ СУДИЛАСЬ (спросить: --строго) + flang check --proof --строго код 4 ПРОВЕРЕНО С ОПОРОЙ + сверщик (по записи того же прогона) код 0 ПРОВЕРЕНО ВПУСТУЮ + flang run --args '{"н": 100}' код 3 не доказано: утверждений 1 + то же с --на-веру код 1 FLANG_PROPERTY: нарушено свойство + +Ноль ПОКУПАЛСЯ примером: тот же файл без строк `пример` +(`programs/false-postcondition-without-examples.flang`) давал 3 и без всякого ключа. +Пара этих двух файлов и держит разницу: одинаковая ложь, одинаковый приговор +под `--строго` — и разный в умолчании. + +── ЧЕГО ЭТОТ НАБОР НЕ ПРОВЕРЯЕТ ─────────────────────────────────────────── +Он проверяет ОДИН прибор из двух — компилятор. Вторая половина исхода живёт в +независимом сверщике (`flang/proof/checker/checker.c`): это он переигрывает +снятия предусловий и он отвечает `ПРОВЕРЕНО ВПУСТУЮ` кодом 0 на записи, где +доказанным не числится ничего. Ключ `--строго` у сверщика — отдельная работа, +и пока её нет, строка «сверщик» из таблицы выше остаётся нулём. Говорить об +этом надо вслух: строгий компилятор при мягком сверщике закрывает цепь не до +конца. + +Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах +(снято 17 сентября 2026 на соседнем наборе, `probes/run/run.sh`). +``` + +### Что стояло над шагом CI + +``` + +Аудит требует, чтобы успех был невозможен без независимой проверки всех +обязательств. Прогоном 19 сентября 2026 показано обратное: программа с +ЛОЖНЫМ постусловием («результат не больше 100» при теле «н плюс н») и +парой строк `пример` получала код 0 и от `flang check`, и от +`flang check --proof`, и от независимого сверщика разом — при том что +`flang run --на-веру` на н = 100 печатал FLANG_PROPERTY и код 1. Ноль +ПОКУПАЛСЯ примером: тот же файл без `пример` давал 3. + +Набор держит ОБЕ половины одной таблицей: строки без «--строго» стерегут +умолчание (оно правкой не тронуто ни на знак — разъедься оно, сломалось +бы всё дерево разом), строки с ключом — сами четыре исхода. Слово +проверяется вместе с кодом: смена причины при том же коде — тоже +расхождение. + +Место здесь, а не в работе `chekker`: та собирает C-сверщик БЕЗ +компилятора нарочно, а этот набор спрашивает мнение компилятора о нём +самом. Двоичный уже собран этой работой; лишней сборки нет. Замер: 20 +проб, около 2 секунд на всё. +``` diff --git a/docs/tasks/completed/4143-a-plan-cannot-be-given-arguments-from-the-command-line.md b/docs/tasks/completed/4143-a-plan-cannot-be-given-arguments-from-the-command-line.md index 78a3b9c3b..40fef2304 100644 --- a/docs/tasks/completed/4143-a-plan-cannot-be-given-arguments-from-the-command-line.md +++ b/docs/tasks/completed/4143-a-plan-cannot-be-given-arguments-from-the-command-line.md @@ -216,3 +216,31 @@ bootstrap/flang io flang/proof/probes/orders/programs/доводы.fscript --н «Прочитать доводы» списком строк, в том же порядке и без разбора». (Статус был «сделана» и до этого захода; задача просто не переехала в `completed/`.) + +## 27 сентября 2026: пробы поручений среды и доводов читают таблицу + +Прогонщик набора — план `run.fscript`; общая часть всех наборов лежит в +`flang/proof/probes/table.fscript`. Таблица `expected.tsv` — строка заголовка с +английскими именами столбцов и строки данных; прочерк `-` в ячейке значит +«ничего». Объяснения, стоявшие в шапках таблицы, прогонщика на оболочке и над +шагом CI, перенесены сюда дословно; старые имена столбцов и файлов в них — +того времени. + +Вызов: `bootstrap/flang io flang/proof/probes/orders/run.fscript --plan Binary`. Код 0 — сошлось всё; 1 — расхождение, и оно названо +строкой; 3 — смотреть было нечем (нет двоичного, нет таблицы, проба убита). +Переменная среды `FLANG_BIN` подменяет двоичный. + +Столбцы: `program`, `environment` (доводы `env`: `FOO=bar` задаёт переменную, `-u FOO` снимает), `keys`, `arguments` (то, что стоит после границы `--`), `code`, `word`. + +Прежде пробы были вписаны списком в сам прогонщик, и у каждой стояло поле +«зачем». Теперь пробы — строки `expected.tsv`, а «зачем» записано здесь, в +порядке строк таблицы: + +1. заданная переменная приходит значением; +2. незаданная переменная — отдельный отклик, а не пустая строка; +3. `--no-env` запрещает чтение среды; +4. пустое имя — свой код отказа, а не пустой ответ; +5. после `--` стоят ровно три довода плана; +6. без `--` список доводов пуст: эта строка показывает, что пятая что-то проверяет; +7. `--no-args` запрещает выдачу доводов; +8. ключи хозяина после `--` едут плану словами и командой не разбираются. diff --git a/docs/tasks/completed/5930-the-tenth-flangrc-key-is-read-by-the-binary-and-hidden-by-the-script.md b/docs/tasks/completed/5930-the-tenth-flangrc-key-is-read-by-the-binary-and-hidden-by-the-script.md index a8eecf540..d99172a41 100644 --- a/docs/tasks/completed/5930-the-tenth-flangrc-key-is-read-by-the-binary-and-hidden-by-the-script.md +++ b/docs/tasks/completed/5930-the-tenth-flangrc-key-is-read-by-the-binary-and-hidden-by-the-script.md @@ -222,3 +222,94 @@ flangrc: «разрешено» — такого значения у «недо Статус «сделана» стоял с 24 сентября 2026, но файл лежал вне `completed/`; перенесён разбором задачника 27 сентября 2026. Оставшаяся дыра — остальные девять ключей двоичный не читает — принадлежит задаче 5413. + +## 27 сентября 2026: пробы ворот недоказанного идут планом + +Прогонщик набора — план `run.fscript`; общая часть всех наборов лежит в +`flang/proof/probes/table.fscript`. Таблица `expected.tsv` — строка заголовка с +английскими именами столбцов и строки данных; прочерк `-` в ячейке значит +«ничего». Объяснения, стоявшие в шапках таблицы, прогонщика на оболочке и над +шагом CI, перенесены сюда дословно; старые имена столбцов и файлов в них — +того времени. + +Вызов: `bootstrap/flang io flang/proof/probes/unproven/run.fscript --plan Binary`. Код 0 — сошлось всё; 1 — расхождение, и оно названо +строкой; 3 — смотреть было нечем (нет двоичного, нет таблицы, проба убита). +Переменная среды `FLANG_BIN` подменяет двоичный. + +Столбцы: `program`, `command` (run или io), `settings` (строка для `.flangrc`), `environment` (значение `FLANG_UNPROVEN`), `keys`, `code`, `word`. Каждая проба идёт в своём временном каталоге с пустым файлом `.git` и своим `HOME`; каталог заводится под `FLANG_TMP`, иначе под `TMPDIR`, иначе в `/tmp`. + +### Что стояло в шапке таблицы + +``` +ПРОБЫ ВОРОТ НЕДОКАЗАННОГО: КЛЮЧ КОМАНДЫ, СРЕДА, `.flangrc` +(ADR-0045; docs/guide/settings.ru.md, раздел «Что делать с недоказанным»). + +Поля: программа, путь (run|io), строка для `.flangrc`, значение FLANG_UNPROVEN, +ключи команды, ожидаемый код возврата, слово, которое обязано стоять в выводе. +«—» в любом поле значит «ничего»: ни файла, ни переменной, ни ключей. + +СЛОВО ПРОВЕРЯЕТСЯ ВМЕСТЕ С КОДОМ НАРОЧНО, и здесь это не перестраховка, а +предмет задачи: «работает» и «работает, назвав в ответе тот ключ, который +человек набрал» — разные исходы с ОДНИМ кодом 0. Строка «--trust» в ответе на +«--trust» и есть то, ради чего задача заведена; проверять её кодом нечем. + +ЧТО ЗДЕСЬ СТЕРЕЖЁТСЯ ЦЕЛИКОМ — СТАРШИНСТВО: + ключ команды → FLANG_UNPROVEN → .flangrc проекта → .flangrc дома → умолчание. +Пара строк «недоказанное = разрешение» + «--unproven refuse» держит верхнюю +ступень (ключ бьёт файл), пара «недоказанное = разрешение» + среда «refuse» — +вторую. Первая строка таблицы держит УМОЛЧАНИЕ: без файла, без переменной и +без ключа ответ обязан остаться тем же, что в 0.7.21, знак в знак, — иначе +выпуск сломает людей второй раз подряд. + +ДВЕ СТРОКИ ПРО ПИСЬМО: «--unproven refuse» отвечает хвостом «--trust», а +«--недоказанное отказ» — хвостом «--на-веру». Ключ, которого нельзя повторить, +не переключив раскладку, и есть беда, с которой задача началась. + +СТРОКА «чепуха = что угодно» — обещание совместимости: незнакомый ключ файла +по-прежнему пропускается молча (docs/guide/settings.ru.md), и ворота при этом +остаются в умолчании. А вот НЕГОДНОЕ ЗНАЧЕНИЕ ЗНАКОМОГО ключа молчанием не +проходит: «недоказанное = разрешено» — код 2 и слова, потому что молчание тут +значит «ворота закрыты», и человек узнал бы об этом кодом 3 в чужой сборке. +``` + +### Что стояло в шапке прогонщика на оболочке + +``` +ПРОБЫ ВОРОТ НЕДОКАЗАННОГО (ADR-0045; docs/guide/settings.ru.md). + + sh flang/proof/probes/unproven/run.sh + FLANG_BIN=<путь> sh flang/proof/probes/unproven/run.sh + +Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; +2 — не смог измерить (нет двоичного, нет таблицы). + +── ЧТО ЗДЕСЬ СТЕРЕЖЁТСЯ ──────────────────────────────────────────────────── +С 0.7.21 недоказанная программа не считается вовсе (`flang/proof/probes/run` +держит это), а пропустить проверку можно ключом. Этот набор — про ДРУГОЕ: про +то, КАК человек управляет воротами и ЧТО ему на это отвечают. + + · три исхода вместо двух: отказ, предупреждение, разрешение; + · старшинство: ключ команды → FLANG_UNPROVEN → .flangrc проекта → + .flangrc дома → умолчание «отказ»; + · письмо ответа = письмо вопроса: набравший «--trust» получает в строке + «--trust», а не «--на-веру». + +── ПОЧЕМУ КАЖДАЯ ПРОБА ИДЁТ В СВОЁМ КАТАЛОГЕ, И ЗАЧЕМ В НЁМ ПУСТОЙ `.git` ── +Настройки ищутся ОТ РАБОЧЕГО КАТАЛОГА ВВЕРХ, и подъём обрывает корневая +примета. Без своей приметы проба взяла бы чужой `.flangrc` — хоть этого +дерева, хоть `/tmp/.git`, который на машине разработчика существует (замер +8 сентября 2026, шапка scripts/flangrc.sh). Пустой файл `.git` рядом с +программой обрывает подъём на первом же шаге, и проба судит РОВНО то, что +ей положено. HOME отводится в пустой каталог по той же причине: `~/.flangrc` +человека в пробу попадать не должен. + +Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах. +``` + +### Что стояло над шагом CI + +``` +Ворота недоказанного настраиваются тремя способами — ключом команды, +переменной среды и .flangrc, — и старшинство между ними названо. Проба +гоняет все три и каждую пару, иначе «ключ бьёт файл» осталось бы словами. +``` diff --git a/docs/tasks/completed/8222-run-and-io-print-the-proof-verdict-and-refuse-an-unproved-program.md b/docs/tasks/completed/8222-run-and-io-print-the-proof-verdict-and-refuse-an-unproved-program.md index e46dd132a..60a9d9f05 100644 --- a/docs/tasks/completed/8222-run-and-io-print-the-proof-verdict-and-refuse-an-unproved-program.md +++ b/docs/tasks/completed/8222-run-and-io-print-the-proof-verdict-and-refuse-an-unproved-program.md @@ -102,3 +102,74 @@ ADR нет: замеры и причины, по которым код устр | `lie.flang` | постусловие ложно, проверка даёт замечание — вердикт «не доказано» ещё до утверждений | | `plan-proved.flang` | план с доказанным утверждением, путь `flang io` | | `plan-on-trust.flang` | план с утверждением на веру, путь `flang io` | + +## 27 сентября 2026: пробы вердикта при запуске идут планом + +Прогонщик набора — план `run.fscript`; общая часть всех наборов лежит в +`flang/proof/probes/table.fscript`. Таблица `expected.tsv` — строка заголовка с +английскими именами столбцов и строки данных; прочерк `-` в ячейке значит +«ничего». Объяснения, стоявшие в шапках таблицы, прогонщика на оболочке и над +шагом CI, перенесены сюда дословно; старые имена столбцов и файлов в них — +того времени. + +Вызов: `bootstrap/flang io flang/proof/probes/run/run.fscript --plan Binary`. Код 0 — сошлось всё; 1 — расхождение, и оно названо +строкой; 3 — смотреть было нечем (нет двоичного, нет таблицы, проба убита). +Переменная среды `FLANG_BIN` подменяет двоичный. + +Столбцы: `program`, `command` (run или io), `keys`, `code`, `word`. + +### Что стояло в шапке таблицы + +``` +Пробы вердикта при запуске (ADR-0045). Поля: программа, путь (run|io), ключ +(0 — без --на-веру, 1 — с ним), ожидаемый код возврата, слово, которое обязано +стоять в выводе. У проб с ключом слово — «доказанность не считалась»: это +кусок строки «на веру», и печатают её ОБА пути (зонд — полем «вердикт», +двоичный — в поток ошибок). Одна таблица на два пути: разъедься они, разошлись +бы молча. Что вычисление состоялось, говорит код 0 рядом: отказ несёт 3. +``` + +### Что стояло в шапке прогонщика на оболочке + +``` +ПРОБЫ ВЕРДИКТА ПРИ ЗАПУСКЕ (ADR-0045, задача 8222). + + sh flang/proof/probes/run/run.sh двоичным: flang run / flang io + sh flang/proof/probes/run/run.sh --зондом толкованием исходников compiler.flang + RABOTA=<каталог> sh flang/proof/probes/run/run.sh --по-записям + сверить уже снятые записи зонда заново, не считая их второй раз: зонд + стоит десять минут и 12 ГиБ на программу, а сверка — секунды. + +Что сверяется — expected.tsv: для каждой programs код возврата и слово в +выводе. Код 0 — сошлось всё; код 1 — хоть одна проба разошлась, и она названа +строкой. Слово «не доказано» и код 3 у недоказанной programs без ключа — +это и есть фальсификатор задачи: код 0 там — ячейка провалена. + +── Два пути, и почему их два ─────────────────────────────────────────────── +Правки flang/self доезжают до двоичного только перепечаткой семени. До неё +двоичный (0.7.19) на первом пути даёт прежнее поведение — недоказанное +запускается кодом 0, — и прогон КРАСЕН по построению: это замер «до». Второй +путь толкует исходники compiler.flang зондом `flang/self/bootstrap/zond-8222.flang` +тем же двоичным: около десяти минут и 12 ГиБ на программу (образец — zond-k7, +задача 9616), и это замер «после» без перепечатки. Зондов идёт не больше трёх +разом (PARALLEL=N меняет), и запись каждого лежит в каталоге $RABOTA. + +Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах +(dash отвечает «Bad substitution» уже на ${ПАРАЛЛЕЛЬ:-3}; снято 17 сентября 2026). +``` + +### Путь толкованием исходников на план не перенесён + +Прогонщик на оболочке умел второй путь, `--зондом`: тот же двоичный толковал +исходники компилятора программой `flang/self/bootstrap/zond-8222.flang`, около +десяти минут и 12 ГиБ на программу. Путь был заведён как замер до rebuild +семени; rebuild прошёл 25 сентября 2026, и двоичный отвечает сам. Вызов одной +пробы этим путём, если он понадобится снова: + +``` +bootstrap/flang run flang/self/bootstrap/zond-8222.flang --function '«Проба запуска»' \ + --max-steps 2000000000 --args '{"путь": "grid.flang", "текст": "<исходник>", "имя": "Ответ", "на веру": false}' +``` + +Для плана вместо «Проба запуска» зовётся «Проба плана», а имя пусто. Ответ несёт +строки «вердикт: …» и «код N»; с таблицей сверяются они. diff --git a/docs/zettel/the-binary-hosts-screen-is-the-controlling-terminal.md b/docs/zettel/the-binary-hosts-screen-is-the-controlling-terminal.md index eca7a582e..608f2f225 100644 --- a/docs/zettel/the-binary-hosts-screen-is-the-controlling-terminal.md +++ b/docs/zettel/the-binary-hosts-screen-is-the-controlling-terminal.md @@ -18,7 +18,7 @@ зовёт место `"stdout"` четыре раза), стал бы в CI получать другой код отказа. **Чем подтверждено.** Ветка `a/host-ekran`, двоичный 0.7.20, пересев -`scripts/seed/seed-refresh.sh`. Набор `flang/proof/probes/screen/run.sh` — +`scripts/seed/seed-refresh.sh`. Набор `flang/proof/probes/screen/run.fscript` — 22 строки ожиданий, сошлось 22 из 22 за 52 с. Терминал в пробах даёт `script -qec … /dev/null`; клавиши подаются через секунду после старта, потому что до первого `«Ждать событие»` терминал ещё построчный и `0x7F` там — знак diff --git a/flang/proof/probes/orders/expected.tsv b/flang/proof/probes/orders/expected.tsv new file mode 100644 index 000000000..8ea60f2f5 --- /dev/null +++ b/flang/proof/probes/orders/expected.tsv @@ -0,0 +1,9 @@ +program environment keys arguments code word +environment.fscript FOO=bar - - 0 "result":"значение среды: bar" +environment.fscript -u FOO - - 0 "result":"переменной среды нет" +environment.fscript FOO=bar --no-env - 1 "code":"FLANG_IO_DENIED","message":"хозяину запрещено читать среду" +empty-name.fscript - - - 1 "code":"FLANG_IO_ENV","message":"поручению нужно непустое имя переменной" +arguments.fscript - --на-веру раз два три 0 "result":"доводов 3: раз|два|три" +arguments.fscript - --на-веру - 0 "result":"доводов 0: " +arguments.fscript - --на-веру --no-args раз 1 "code":"FLANG_IO_DENIED","message":"хозяину запрещено читать доводы" +arguments.fscript - --на-веру --no-net --plan Икс 0 "result":"доводов 3: --no-net|--plan|Икс" diff --git a/flang/proof/probes/orders/run.fscript b/flang/proof/probes/orders/run.fscript index 7013cf62d..3cad62f1d 100644 --- a/flang/proof/probes/orders/run.fscript +++ b/flang/proof/probes/orders/run.fscript @@ -1,166 +1,60 @@ -модуль «Проверка двух поручений» +модуль «Пробы поручений среды и доводов» -объект «Проба» - «зачем»: строка - «команда»: строка - «ждём»: число - «слово»: строка +использует «Таблица проб» из "../table.fscript" -тотальная функция «Корень» - возвращает строка - пример «до корня дерева три шага вверх» - ожидается "../../../.." - "../../../.." - -тотальная функция «Пробы» - возвращает список «Проба» - обеспечивает «проб ровно восемь» (длина результат) равен 8 - [запись «Проба» с «зачем» равным "заданная переменная приходит значением" и «команда» равным "env FOO=bar bootstrap/flang io flang/proof/probes/orders/programs/environment.fscript" и «ждём» равным 0 и «слово» равным "\"result\":\"значение среды: bar\"", - запись «Проба» с «зачем» равным "незаданная переменная — ОТДЕЛЬНЫЙ отклик, а не пустая строка" и «команда» равным "env -u FOO bootstrap/flang io flang/proof/probes/orders/programs/environment.fscript" и «ждём» равным 0 и «слово» равным "\"result\":\"переменной среды нет\"", - запись «Проба» с «зачем» равным "--no-env запрещает чтение среды" и «команда» равным "env FOO=bar bootstrap/flang io flang/proof/probes/orders/programs/environment.fscript --no-env" и «ждём» равным 1 и «слово» равным "\"code\":\"FLANG_IO_DENIED\",\"message\":\"хозяину запрещено читать среду\"", - запись «Проба» с «зачем» равным "пустое имя — свой код отказа, а не пустой ответ" и «команда» равным "bootstrap/flang io flang/proof/probes/orders/programs/empty-name.fscript" и «ждём» равным 1 и «слово» равным "\"code\":\"FLANG_IO_ENV\",\"message\":\"поручению нужно непустое имя переменной\"", - запись «Проба» с «зачем» равным "после «--» стоят ровно три довода плана" и «команда» равным "bootstrap/flang io flang/proof/probes/orders/programs/arguments.fscript --на-веру -- раз два три" и «ждём» равным 0 и «слово» равным "\"result\":\"доводов 3: раз|два|три\"", - запись «Проба» с «зачем» равным "ЗУБЫ: без «--» список доводов пуст" и «команда» равным "bootstrap/flang io flang/proof/probes/orders/programs/arguments.fscript --на-веру" и «ждём» равным 0 и «слово» равным "\"result\":\"доводов 0: \"", - запись «Проба» с «зачем» равным "--no-args запрещает выдачу доводов" и «команда» равным "bootstrap/flang io flang/proof/probes/orders/programs/arguments.fscript --на-веру --no-args -- раз" и «ждём» равным 1 и «слово» равным "\"code\":\"FLANG_IO_DENIED\",\"message\":\"хозяину запрещено читать доводы\"", - запись «Проба» с «зачем» равным "ключи хозяина ПОСЛЕ «--» едут плану словами и командой не разбираются" и «команда» равным "bootstrap/flang io flang/proof/probes/orders/programs/arguments.fscript --на-веру -- --no-net --plan Икс" и «ждём» равным 0 и «слово» равным "\"result\":\"доводов 3: --no-net|--plan|Икс\""] - -тотальная функция «Названа ли программа» - принимает имя: строка, пробы: список «Проба» - возвращает признак - пример «имя стоит в команде одной из проб» - дано имя равно "environment.fscript" - дано пробы равно [запись «Проба» с «зачем» равным "" и «команда» равным "flang io programs/environment.fscript" и «ждём» равным 0 и «слово» равным ""] - ожидается да - пример «имени нет ни в одной команде» - дано имя равно "arguments.fscript" - дано пробы равно [запись «Проба» с «зачем» равным "" и «команда» равным "flang io programs/environment.fscript" и «ждём» равным 0 и «слово» равным ""] - ожидается нет - свёртка пробы начиная с нет как есть и проба → (есть или ((проба.«команда») содержит имя)) - -тотальная функция «Незаявленные» - принимает имена: список строки, пробы: список «Проба» - возвращает список строки - обеспечивает «незаявленных не больше, чем имён» (длина результат) не больше (длина имена) - пример «лишняя программа названа поимённо» - дано имена равно ["environment.fscript", "лишняя.fscript"] - дано пробы равно [запись «Проба» с «зачем» равным "" и «команда» равным "flang io programs/environment.fscript" и «ждём» равным 0 и «слово» равным ""] - ожидается ["лишняя.fscript"] - отфильтровать имена где имя → не («Названа ли программа» от имя и пробы) +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "orders" и «код расхождения» равным "FLANG_PROBE_ORDERS" и «код слепоты» равным "FLANG_PROBE_ORDERS_CANNOT_LOOK" + запись «Набор» с «имя» равным "orders" и «код расхождения» равным "FLANG_PROBE_ORDERS" и «код слепоты» равным "FLANG_PROBE_ORDERS_CANNOT_LOOK" -тотальная функция «Про беду» - принимает проба: «Проба», код: число, вывод: строка +тотальная функция «Доводы» + принимает ячейка: строка возвращает строка - обеспечивает «беда начинается с того, зачем ставилась проба» результат начинается с (проба.«зачем») - пример «беда называет пробу, ожидание и ответ» - дано проба равно запись «Проба» с «зачем» равным "пустое имя" и «команда» равным "flang io empty-name.fscript" и «ждём» равным 1 и «слово» равным "FLANG_IO_ENV" - дано код равно 0 - дано вывод равно "тихо" - ожидается "пустое имя: ждали код 1 и «FLANG_IO_ENV», вышло код 0 — flang io empty-name.fscript" - соединить [(проба.«зачем»), ": ждали код ", (к строке (проба.«ждём»)), " и «", (проба.«слово»), "», вышло код ", (к строке код), " — ", (проба.«команда»)] по "" - -тотальная функция «Сошлась ли» - принимает проба: «Проба», код: число, вывод: строка - возвращает признак - обеспечивает «сошлась только при обоих совпадениях» результат равен ((код равен (проба.«ждём»)) и притом (вывод содержит (проба.«слово»))) - пример «код и слово сошлись» - дано проба равно запись «Проба» с «зачем» равным "" и «команда» равным "" и «ждём» равным 0 и «слово» равным "доводов 3" - дано код равно 0 - дано вывод равно "{\"result\":\"доводов 3: раз\"}" - ожидается да - пример «код сошёлся, слово нет» - дано проба равно запись «Проба» с «зачем» равным "" и «команда» равным "" и «ждём» равным 0 и «слово» равным "доводов 3" - дано код равно 0 - дано вывод равно "{\"result\":\"доводов 0: \"}" - ожидается нет - (код равен (проба.«ждём»)) и притом (вывод содержит (проба.«слово»)) + пример «прочерк значит, что границы доводов в вызове нет» + дано ячейка равно "-" + ожидается "" + пример «доводы плана идут после границы» + дано ячейка равно "раз два" + ожидается " -- раз два" + если ячейка равен "-" + то "" + иначе соединить [" -- ", ячейка] по "" + +тотальная функция «Команда» + принимает части: список строки + возвращает строка + «От корня» от («С меткой» от (соединить ["env ", («Ключи» от («Поле» от части и 2)), " $flang io 'flang/proof/probes/orders/programs/", («Поле» от части и 1), "' ", («Ключи» от («Поле» от части и 3)), («Доводы» от («Поле» от части и 4))] по "")) -тотальная функция «Итог» - принимает беды: список строки, сделано: число - возвращает «Продолжение» - пример «все пробы сошлись — план доходит до конца» - дано беды равно пустой список - дано сделано равно 8 - ожидается вариант «Конец работы» с значение равным "два поручения: проб 8, разошлось 0" - разбор беды - случай пусто - то вариант «Конец работы» с значение равным (соединить ["два поручения: проб ", (к строке сделано), ", разошлось 0"] по "") - случай голова и хвост - то вариант «Провал» с код равным "FLANG_DVA_PORUCHENIYA" и сообщение равным (соединить (приписать (соединить ["два поручения РАЗОШЛИСЬ, расхождений ", (к строке (длина беды)), " из ", (к строке сделано), ":"] по "") к беды) по "\n · ") +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["arguments.fscript", "-", "--на-веру", "раз два", "0", "доводов 2"] + ожидается запись «Проба» с «программа» равным "arguments.fscript" и «приметы» равным "arguments.fscript [--на-веру раз два]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { env $flang io 'flang/proof/probes/orders/programs/arguments.fscript' --на-веру -- раз два; } 2>&1; echo \"[code=$?]\"" и «код» равным "0" и «слово» равным "доводов 2" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2), («Поле» от части и 3), («Поле» от части и 4)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 5) и «слово» равным («Поле» от части и 6) -тип «Ход» - вариант «Ждём каталог» - вариант «Ждём пробу» содержит проба: «Проба», осталось: список «Проба», беды: список строки, сделано: число +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) тотальная функция «Начать» возвращает «Ход» - пример «первым делом читается каталог программ» - ожидается вариант «Ждём каталог» - вариант «Ждём каталог» - -тотальная функция «Пойти по пробам» - принимает очередь: список «Проба», беды: список строки, сделано: число - возвращает «Продолжение» - разбор очередь - случай пусто - то «Итог» от беды и сделано - случай голова и хвост - то вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", (соединить ["cd ", («Корень»), " && exec ", (голова.«команда»)] по "")]) и потом равным (вариант «Ждём пробу» с проба равным голова и осталось равным хвост и беды равным беды и сделано равным сделано) - -тотальная функция «Нечем смотреть» - принимает почему: строка - возвращает «Продолжение» - пример «невозможность смотреть — не приговор поручению» - дано почему равно "двоичного нет на месте" - ожидается вариант «Не проверено» с код равным "FLANG_DVA_PORUCHENIYA_NECHEM_SMOTRET" и сообщение равным "двоичного нет на месте" - вариант «Не проверено» с код равным "FLANG_DVA_PORUCHENIYA_NECHEM_SMOTRET" и сообщение равным почему - -тотальная функция «После каталога» - принимает отклик: «Отклик» - возвращает «Продолжение» - пример «каталог не прочитан — это невозможность смотреть, а не приговор поручению» - дано отклик равно вариант «Сбой» с код равным "FLANG_IO_LIST" и сообщение равным "каталог не открыт" - ожидается вариант «Не проверено» с код равным "FLANG_DVA_PORUCHENIYA_NECHEM_SMOTRET" и сообщение равным "каталог проб не прочитан (FLANG_IO_LIST): каталог не открыт" - разбор отклик - случай вариант «Перечислено» с имена как имена - то разбор («Незаявленные» от имена и («Пробы»)) - случай пусто - то «Пойти по пробам» от («Пробы») и пустой список и 0 - случай голова и хвост - то вариант «Провал» с код равным "FLANG_DVA_PORUCHENIYA" и сообщение равным (соединить (приписать "НЕЗАЯВЛЕННЫЕ ПРОГРАММЫ: лежат в каталоге, а пробы на них нет:" к («Незаявленные» от имена и («Пробы»))) по "\n · ") - случай вариант «Сбой» с код как код и сообщение как сообщение - то «Нечем смотреть» от (соединить ["каталог проб не прочитан (", код, "): ", сообщение] по "") - случай любое - то «Нечем смотреть» от "ждали перечня каталога программ" - -тотальная функция «После пробы» - принимает проба: «Проба», осталось: список «Проба», беды: список строки, сделано: число, отклик: «Отклик» - возвращает «Продолжение» - разбор отклик - случай вариант «Процесс завершён» с код как код и вывод как вывод и ошибки как ошибки - то если код равен 127 - то «Нечем смотреть» от (соединить ["оболочка ответила 127 «команда не найдена» на пробе «", (проба.«зачем»), "»: двоичного нет на месте, соберите его — make -C bootstrap"] по "") - иначе «Пойти по пробам» от осталось и (если («Сошлась ли» от проба и код и (соединить [вывод, ошибки] по "")) то беды иначе (добавить («Про беду» от проба и код и (соединить [вывод, ошибки] по "")) к беды)) и (сделано плюс 1) - случай вариант «Процесс убит» с сигнал как сигнал и вывод как вывод и ошибки как ошибки - то «Нечем смотреть» от (соединить ["проба «", (проба.«зачем»), "» убита сигналом ", сигнал] по "") - случай вариант «Сбой» с код как код и сообщение как сообщение - то «Нечем смотреть» от (соединить ["sh не запустился (", код, "): ", сообщение] по "") - случай любое - то «Нечем смотреть» от (соединить ["ждали ответа процесса на пробе «", (проба.«зачем»), "»"] по "") + пример «план начинается с начала» + ожидается вариант «Начало» + вариант «Начало» тотальная функция «Дальше» принимает ход: «Ход», отклик: «Отклик» возвращает «Продолжение» разбор ход - случай вариант «Ждём каталог» - то разбор отклик - случай вариант «Пока ничего» - то вариант «Сделать» с поручение равным (вариант «Перечислить каталог» с путь равным "programs") и потом равным (вариант «Ждём каталог») - случай любое - то «После каталога» от отклик - случай вариант «Ждём пробу» с проба как проба и осталось как осталось и беды как беды и сделано как сделано - то «После пробы» от проба и осталось и беды и сделано и отклик + случай вариант «Ждём таблицу» + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик -план «Два поручения» +план «Binary» состояние «Ход» начинает с «Начать» обрабатывает «Дальше» diff --git a/flang/proof/probes/run/expected.tsv b/flang/proof/probes/run/expected.tsv index 5557fad44..18e6af591 100644 --- a/flang/proof/probes/run/expected.tsv +++ b/flang/proof/probes/run/expected.tsv @@ -1,20 +1,14 @@ -# Пробы вердикта при запуске (ADR-0045). Поля: программа, путь (run|io), ключ -# (0 — без --на-веру, 1 — с ним), ожидаемый код возврата, слово, которое обязано -# стоять в выводе. У проб с ключом слово — «доказанность не считалась»: это -# кусок строки «на веру», и печатают её ОБА пути (зонд — полем «вердикт», -# двоичный — в поток ошибок). Одна таблица на два пути: разъедься они, разошлись -# бы молча. Что вычисление состоялось, говорит код 0 рядом: отказ несёт 3. -программа путь ключ код слово -grid.flang run 0 3 не доказано -on-trust.flang run 0 3 не доказано -lie.flang run 0 3 не доказано -identity.flang run 0 0 доказано: утверждений 1 -by-type.flang run 0 0 доказано: утверждений 1 -induction.flang run 0 0 доказано: утверждений 1 -without-statements.flang run 0 0 доказано: утверждений 0 -grid.flang run 1 0 доказанность не считалась -on-trust.flang run 1 0 доказанность не считалась -lie.flang run 1 0 доказанность не считалась -plan-proved.flang io 0 0 доказано: утверждений 1 -plan-on-trust.flang io 0 3 не доказано -plan-on-trust.flang io 1 0 доказанность не считалась +program command keys code word +grid.flang run - 3 не доказано +on-trust.flang run - 3 не доказано +lie.flang run - 3 не доказано +identity.flang run - 0 доказано: утверждений 1 +by-type.flang run - 0 доказано: утверждений 1 +induction.flang run - 0 доказано: утверждений 1 +without-statements.flang run - 0 доказано: утверждений 0 +grid.flang run --на-веру 0 доказанность не считалась +on-trust.flang run --на-веру 0 доказанность не считалась +lie.flang run --на-веру 0 доказанность не считалась +plan-proved.flang io - 0 доказано: утверждений 1 +plan-on-trust.flang io - 3 не доказано +plan-on-trust.flang io --на-веру 0 доказанность не считалась diff --git a/flang/proof/probes/run/run.fscript b/flang/proof/probes/run/run.fscript new file mode 100644 index 000000000..5bb5ae3b0 --- /dev/null +++ b/flang/proof/probes/run/run.fscript @@ -0,0 +1,54 @@ +модуль «Пробы вердикта при запуске» + +использует «Таблица проб» из "../table.fscript" + +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "run" и «код расхождения» равным "FLANG_PROBE_RUN" и «код слепоты» равным "FLANG_PROBE_RUN_CANNOT_LOOK" + запись «Набор» с «имя» равным "run" и «код расхождения» равным "FLANG_PROBE_RUN" и «код слепоты» равным "FLANG_PROBE_RUN_CANNOT_LOOK" + +тотальная функция «Действие» + принимает части: список строки + возвращает строка + если («Поле» от части и 2) равен "io" + то "io %s --max-steps 1000000" + иначе "run %s --function «Ответ»" + +тотальная функция «Команда» + принимает части: список строки + возвращает строка + «От корня» от («С меткой» от (соединить ["$flang ", (соединить (разделить («Действие» от части) по "%s") по (соединить ["'flang/proof/probes/run/programs/", («Поле» от части и 1), "'"] по "")), " ", («Ключи» от («Поле» от части и 3))] по "")) + +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["grid.flang", "run", "-", "3", "не доказано"] + ожидается запись «Проба» с «программа» равным "grid.flang" и «приметы» равным "grid.flang [run]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { $flang run 'flang/proof/probes/run/programs/grid.flang' --function «Ответ» ; } 2>&1; echo \"[code=$?]\"" и «код» равным "3" и «слово» равным "не доказано" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2), («Поле» от части и 3)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 4) и «слово» равным («Поле» от части и 5) + +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) + +тотальная функция «Начать» + возвращает «Ход» + пример «план начинается с начала» + ожидается вариант «Начало» + вариант «Начало» + +тотальная функция «Дальше» + принимает ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём таблицу» + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик + +план «Binary» + состояние «Ход» + начинает с «Начать» + обрабатывает «Дальше» diff --git a/flang/proof/probes/run/run.sh b/flang/proof/probes/run/run.sh deleted file mode 100755 index 5c6744e82..000000000 --- a/flang/proof/probes/run/run.sh +++ /dev/null @@ -1,115 +0,0 @@ -#!/bin/sh -# SPDX-FileCopyrightText: 2026 Digitable (Marat Zimnurov) -# SPDX-License-Identifier: BSD-2-Clause -# -# ПРОБЫ ВЕРДИКТА ПРИ ЗАПУСКЕ (ADR-0045, задача 8222). -# -# sh flang/proof/probes/run/run.sh двоичным: flang run / flang io -# sh flang/proof/probes/run/run.sh --зондом толкованием исходников compiler.flang -# RABOTA=<каталог> sh flang/proof/probes/run/run.sh --по-записям -# сверить уже снятые записи зонда заново, не считая их второй раз: зонд -# стоит десять минут и 12 ГиБ на программу, а сверка — секунды. -# -# Что сверяется — expected.tsv: для каждой programs код возврата и слово в -# выводе. Код 0 — сошлось всё; код 1 — хоть одна проба разошлась, и она названа -# строкой. Слово «не доказано» и код 3 у недоказанной programs без ключа — -# это и есть фальсификатор задачи: код 0 там — ячейка провалена. -# -# ── Два пути, и почему их два ─────────────────────────────────────────────── -# Правки flang/self доезжают до двоичного только перепечаткой семени. До неё -# двоичный (0.7.19) на первом пути даёт прежнее поведение — недоказанное -# запускается кодом 0, — и прогон КРАСЕН по построению: это замер «до». Второй -# путь толкует исходники compiler.flang зондом `flang/self/bootstrap/zond-8222.flang` -# тем же двоичным: около десяти минут и 12 ГиБ на программу (образец — zond-k7, -# задача 9616), и это замер «после» без перепечатки. Зондов идёт не больше трёх -# разом (PARALLEL=N меняет), и запись каждого лежит в каталоге $RABOTA. -# -# Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах -# (dash отвечает «Bad substitution» уже на ${ПАРАЛЛЕЛЬ:-3}; снято 17 сентября 2026). -set -u - -KOREN=$(CDPATH= cd -- "$(dirname -- "$0")/../../../.." && pwd) -FLANG=${FLANG:-$KOREN/bootstrap/flang} -PROBY=$KOREN/flang/proof/probes/run -ZOND=$KOREN/flang/self/bootstrap/zond-8222.flang -PARALLEL=${PARALLEL:-3} -RABOTA=${RABOTA:-$(mktemp -d -p "${FLANG_TMP:-/srv/tmp}" proby-zapuska.XXXXXX)} -export LC_ALL=C.UTF-8 - -ZONDOM=0 -PO_ZAPISYAM=0 -[ "${1:-}" = "--зондом" ] && ZONDOM=1 -[ "${1:-}" = "--по-записям" ] && { ZONDOM=1; PO_ZAPISYAM=1; } -[ -x "$FLANG" ] || { echo "нет двоичного: $FLANG" >&2; exit 2; } - -# Одна проба двоичным: код и слово читаются с потока ошибок и вывода вместе. -proba_binary() { # программа путь ключ → печатает «кодвывод-в-одну-строку» - f=$PROBY/programs/$1; kl="" - [ "$3" = "1" ] && kl=--на-веру - if [ "$2" = run ]; then - out=$("$FLANG" run "$f" --function «Ответ» $kl 2>&1); k=$? - else - out=$("$FLANG" io "$f" --max-steps 1000000 $kl 2>&1); k=$? - fi - printf '%s\t%s\n' "$k" "$(printf '%s' "$out" | tr '\n' ' ')" -} - -# Одна проба зондом: доводы зонду — JSON с текстом programs; ответ зонда — -# ОДНА строка-значение, внутри которой «\n» стоят буквами: «вердикт: …\nкод N\n -# запущено да/нет\nисход». Поэтому читается она через замену «\n» на перевод -# строки, а не построчно: `grep '^код '` по сырому файлу не находил ничего и все -# тринадцать проб выходили «код ?» (снято 18 сентября 2026). -proba_zond() { # программа путь ключ → файл записи - f=$PROBY/programs/$1; zap=$RABOTA/$1.$2.$3.txt - fn='«Проба запуска»'; [ "$2" = io ] && fn='«Проба плана»' - args=$(python3 -c ' -import json,sys -p,f,k=sys.argv[1],sys.argv[2],sys.argv[3] -print(json.dumps({"путь": p, "текст": open(f, encoding="utf-8").read(), "имя": "Ответ" if p.find("план")<0 else "", "на веру": k=="1"}, ensure_ascii=False))' "$1" "$f" "$3") - { /usr/bin/time -f 'зонд: %es, пик %M КБ, код %x' "$FLANG" run "$ZOND" --function "$fn" --max-steps 2000000000 --args "$args"; } > "$zap" 2>&1 - echo "$zap" -} - -BAD=0; N=0; JOBS=0 -awk -F'\t' '!/^#/ && $1 != "программа" && NF >= 5' "$PROBY/expected.tsv" > "$RABOTA/ожидание.tsv" - -if [ "$ZONDOM" -eq 1 ]; then - # Сначала все зонды (не больше PARALLEL разом), потом сверка записей. - while IFS="$(printf '\t')" read -r prog put kl kod slovo; do - [ "$PO_ZAPISYAM" -eq 1 ] && [ -s "$RABOTA/$prog.$put.$kl.txt" ] && continue - proba_zond "$prog" "$put" "$kl" >/dev/null & - JOBS=$((JOBS+1)) - if [ "$JOBS" -ge "$PARALLEL" ]; then wait; JOBS=0; fi - done < "$RABOTA/ожидание.tsv" - wait -fi - -while IFS="$(printf '\t')" read -r prog put kl kod slovo; do - N=$((N+1)) - if [ "$ZONDOM" -eq 1 ]; then - zap=$RABOTA/$prog.$put.$kl.txt - # Код и запуск читаются из ответа зонда, а не из кода выхода двоичного: - # двоичный вернул значение зонда кодом 0 — толкование удалось. - k=$(sed 's/\\n/\n/g' "$zap" | grep -a -m1 '^код ' | awk '{print $2}') - out=$(sed 's/\\n/\n/g' "$zap" | tr '\n' ' ') - [ -n "$k" ] || k="?" - else - set -- $(proba_binary "$prog" "$put" "$kl" | { IFS="$(printf '\t')" read -r a b; printf '%s\n' "$a"; printf '%s\n' "$b"; }) - k=$1; shift; out=$* - fi - # lie.flang с ключом запускается и на 0.7.19 честно даёт FLANG_PROPERTY на NaN? Нет: - # «Квадрат» от 7 даёт 49, постусловие верно на этом входе — вычисление удаётся. - if [ "$k" = "$kod" ] && printf '%s' "$out" | grep -q -a -F -- "$slovo"; then - printf '✓ %-22s %-3s ключ=%s код %s, есть «%s»\n' "$prog" "$put" "$kl" "$k" "$slovo" - else - printf '✗ %-22s %-3s ключ=%s ждали код %s и «%s», вышло код %s: %s\n' "$prog" "$put" "$kl" "$kod" "$slovo" "$k" "$(printf '%s' "$out" | cut -c1-200)" - BAD=$((BAD+1)) - fi -done < "$RABOTA/ожидание.tsv" - -if [ "$BAD" -eq 0 ]; then - echo "сошлось всё: проб $N, разошлось 0 (путь: $([ "$ZONDOM" -eq 1 ] && echo зондом || echo двоичным), записи: $RABOTA)" - exit 0 -fi -echo "НЕ СОШЛОСЬ: проб $N, разошлось $BAD (путь: $([ "$ZONDOM" -eq 1 ] && echo зондом || echo двоичным), записи: $RABOTA)" -exit 1 diff --git a/flang/proof/probes/screen-size/expected.tsv b/flang/proof/probes/screen-size/expected.tsv index 875670b4c..32f3fefa0 100644 --- a/flang/proof/probes/screen-size/expected.tsv +++ b/flang/proof/probes/screen-size/expected.tsv @@ -1,33 +1,7 @@ -# Пробы РАЗМЕРА ЭКРАНА двоичного хозяина: поручение «Размер экрана». -# Поля: программа, среда (терминал|труба), ширина и высота псевдотерминала -# (`-` — не задавать), ключ (`-` — без ключей), ожидаемый код возврата, слово, -# которое обязано стоять в выводе. -# -# РАЗМЕР ЗАДАЁТСЯ НАБОРОМ, А НЕ БЕРЁТСЯ КАКОЙ ПРИДЁТСЯ, и это не удобство: -# `script -qec … /dev/null` заводит псевдотерминал размером с родительский, а у -# прогона под CI, под nohup и под этим набором родительского терминала нет — -# размер вышел бы 0×0 на одной машине и 204×52 на другой, и проба сверяла бы -# числа сама с собой. Здесь размер ставит `stty cols … rows …` внутри того же -# псевдотерминала, и ожидаемые числа набраны рядом: сходятся они с тем, что -# отдаст `stty size` в том же сеансе, знак в знак. -# -# ДВЕ СТРОКИ С РАЗНЫМИ ЧИСЛАМИ (80×24 и 132×50) — не повтор: одна проверяет, -# что размер вообще приходит, вторая — что он ЧИТАЕТСЯ у терминала, а не -# набран в хозяине. Оставь хозяин зашитые 80×24, и вторая строка покраснеет. -# -# СТРОКА 0×0 — ФАЛЬСИФИКАТОР ПРАВИЛА «не выдумывать 80×24»: так отвечает -# терминал без рамки (и ровно так — псевдотерминал без родителя). Ответ обязан -# быть отказом FLANG_IO_NO_SCREEN, а не придуманным размером; позеленей она -# кодом 0, и хозяин молча врал бы всякому, кто считает кадр. -# -# СТРОКА «труба» стережёт совместимость: там, где вывод уведён в трубу, в файл, -# в CI или под nohup, экрана нет и ответ прежний — FLANG_IO_NO_SCREEN. -# Строки с `--no-screen` стерегут порядок проверок: полномочие спрашивается -# ДО терминала, поэтому и в трубе, и в терминале ответ один — FLANG_IO_DENIED. -программа среда ширина высота ключ код слово -size.flang терминал 80 24 - 0 экран измерен: ширина 80, высота 24 -size.flang терминал 132 50 - 0 экран измерен: ширина 132, высота 50 -size.flang терминал 0 0 - 1 FLANG_IO_NO_SCREEN -size.flang труба - - - 1 FLANG_IO_NO_SCREEN -size.flang терминал 80 24 --no-screen 1 FLANG_IO_DENIED -size.flang труба - - --no-screen 1 FLANG_IO_DENIED +program environment width height keys code word +size.flang terminal 80 24 - 0 экран измерен: ширина 80, высота 24 +size.flang terminal 132 50 - 0 экран измерен: ширина 132, высота 50 +size.flang terminal 0 0 - 1 FLANG_IO_NO_SCREEN +size.flang pipe - - - 1 FLANG_IO_NO_SCREEN +size.flang terminal 80 24 --no-screen 1 FLANG_IO_DENIED +size.flang pipe - - --no-screen 1 FLANG_IO_DENIED diff --git a/flang/proof/probes/screen-size/run.fscript b/flang/proof/probes/screen-size/run.fscript index 8db45a0ff..a73d3015f 100644 --- a/flang/proof/probes/screen-size/run.fscript +++ b/flang/proof/probes/screen-size/run.fscript @@ -1,235 +1,74 @@ модуль «Пробы размера экрана» -объект «Проба» - «программа»: строка - «среда»: строка - «ширина»: строка - «высота»: строка - «ключ»: строка - «код»: строка - «слово»: строка +использует «Таблица проб» из "../table.fscript" -тотальная функция «Поле» - принимает части: список строки, номер: число - возвращает строка - пример «Третье поле строки ожидания» - дано части равно ["size.flang", "труба", "-"] - дано номер равно 3 - ожидается "-" - пример «Номер за списком даёт пусто, а не отказ» - дано части равно ["size.flang"] - дано номер равно 4 - ожидается "" - если ((номер не меньше 1) и притом (номер не больше (длина части))) - то элемент номер в части - иначе "" - -тотальная функция «Строка годится» - принимает строка: строка - возвращает признак - пример «Строка ожидания годится» - дано строка равно "size.flang\tтруба\t-\t-\t-\t1\tFLANG_IO_NO_SCREEN" - ожидается да - пример «Проза таблицы начинается с решётки» - дано строка равно "# пояснение" - ожидается нет - пример «Заголовок таблицы пробой не считается» - дано строка равно "программа\tсреда\tширина\tвысота\tключ\tкод\tслово" - ожидается нет - пример «Пустая строка пробой не считается» - дано строка равно "" - ожидается нет - (не (строка начинается с "#")) и притом ((длина (разделить строка по "\t")) не меньше 7) и притом (не ((«Поле» от (разделить строка по "\t") и 1) равен "программа")) - -тотальная функция «Проба из строки» - принимает строка: строка - возвращает «Проба» - пример «Семь полей становятся пробой» - дано строка равно "size.flang\tтерминал\t80\t24\t-\t0\tширина 80" - ожидается запись «Проба» с «программа» равным "size.flang" и «среда» равным "терминал" и «ширина» равным "80" и «высота» равным "24" и «ключ» равным "-" и «код» равным "0" и «слово» равным "ширина 80" - пусть части равно (разделить строка по "\t") - запись «Проба» с «программа» равным («Поле» от части и 1) и «среда» равным («Поле» от части и 2) и «ширина» равным («Поле» от части и 3) и «высота» равным («Поле» от части и 4) и «ключ» равным («Поле» от части и 5) и «код» равным («Поле» от части и 6) и «слово» равным («Поле» от части и 7) +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "screen-size" и «код расхождения» равным "FLANG_PROBE_SCREEN_SIZE" и «код слепоты» равным "FLANG_PROBE_SCREEN_SIZE_CANNOT_LOOK" + запись «Набор» с «имя» равным "screen-size" и «код расхождения» равным "FLANG_PROBE_SCREEN_SIZE" и «код слепоты» равным "FLANG_PROBE_SCREEN_SIZE_CANNOT_LOOK" -тотальная функция «Пробы» - принимает текст: строка - возвращает список «Проба» - пример «Из таблицы берутся только строки проб» - дано текст равно "# проза\nпрограмма\tсреда\tширина\tвысота\tключ\tкод\tслово\nsize.flang\tтруба\t-\t-\t-\t1\tFLANG_IO_NO_SCREEN" - ожидается [запись «Проба» с «программа» равным "size.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN"] - отобразить (отфильтровать (разделить текст по "\n") где строка → («Строка годится» от строка)) как строка → («Проба из строки» от строка) - -тотальная функция «Ключи» - принимает проба: «Проба» +тотальная функция «Вызов» + принимает части: список строки возвращает строка - пример «Прочерк значит без ключей» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "" - если (проба.«ключ») равен "-" - то "" - иначе проба.«ключ» + соединить ["$flang io 'flang/proof/probes/screen-size/programs/", («Поле» от части и 1), "' ", («Ключи» от («Поле» от части и 5))] по "" -тотальная функция «Стелить экран» - принимает проба: «Проба» +тотальная функция «Рамка» + принимает ширина: строка, высота: строка возвращает строка - пример «Размер не задан — псевдотерминал остаётся каким пришёл» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "с" + пример «размер не задан — псевдотерминал остаётся каким пришёл» + дано ширина равно "-" + дано высота равно "-" ожидается "" - пример «Размер задан — рамка ставится внутри того же псевдотерминала» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "терминал" и «ширина» равным "80" и «высота» равным "24" и «ключ» равным "-" и «код» равным "0" и «слово» равным "с" + пример «размер задан — рамка ставится внутри того же псевдотерминала» + дано ширина равно "80" + дано высота равно "24" ожидается "stty cols 80 rows 24; " - если (проба.«ширина») равен "-" + если ширина равен "-" то "" - иначе соединить ["stty cols ", (проба.«ширина»), " rows ", (проба.«высота»), "; "] по "" + иначе соединить ["stty cols ", ширина, " rows ", высота, "; "] по "" -тотальная функция «Вызов» - принимает проба: «Проба» +тотальная функция «В терминале» + принимает части: список строки возвращает строка - пример «Путь к плану собирается из имени программы» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "bootstrap/flang io 'flang/proof/probes/screen-size/programs/р.flang' " - соединить ["bootstrap/flang io 'flang/proof/probes/screen-size/programs/", (проба.«программа»), "' ", («Ключи» от проба)] по "" + соединить ["script -qec \"", («Рамка» от («Поле» от части и 3) и («Поле» от части и 4)), («Вызов» от части), "\" /dev/null"] по "" тотальная функция «Команда» - принимает проба: «Проба» - возвращает строка - пример «В трубе код возврата достаётся меткой, потому что после трубы он чужой» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "cd ../../../.. && { bootstrap/flang io 'flang/proof/probes/screen-size/programs/р.flang' 2>&1; echo \"[КОД=$?]\"; } | cat" - пример «В терминале рамка ставится перед вызовом, в том же сеансе» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "терминал" и «ширина» равным "80" и «высота» равным "24" и «ключ» равным "-" и «код» равным "0" и «слово» равным "с" - ожидается "cd ../../../.. && script -qec \"stty cols 80 rows 24; bootstrap/flang io 'flang/proof/probes/screen-size/programs/р.flang' \" /dev/null; echo \"[КОД=$?]\"" - если (проба.«среда») равен "труба" - то соединить ["cd ../../../.. && { ", («Вызов» от проба), " 2>&1; echo \"[КОД=$?]\"; } | cat"] по "" - иначе соединить ["cd ../../../.. && script -qec \"", («Стелить экран» от проба), («Вызов» от проба), "\" /dev/null; echo \"[КОД=$?]\""] по "" - -тотальная функция «Кратко» - принимает текст: строка - возвращает строка - пример «Переводы строк становятся пробелами» - дано текст равно "раз\nдва" - ожидается "раз два" - пусть одной равно (соединить (разделить (соединить (разделить текст по "\n") по " ") по "\r") по "") - если (длина одной) не больше 400 - то одной - иначе подстрока одной с 1 по 400 - -тотальная функция «Метка кода» - принимает проба: «Проба» - возвращает строка - пример «Метка несёт ожидаемый код» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "[КОД=1]" - соединить ["[КОД=", (проба.«код»), "]"] по "" - -тотальная функция «Приметы» - принимает проба: «Проба» + принимает части: список строки возвращает строка - пример «Приметы называют программу, среду, рамку и ключ» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "терминал" и «ширина» равным "80" и «высота» равным "24" и «ключ» равным "--no-screen" и «код» равным "1" и «слово» равным "с" - ожидается "р.flang [терминал 80×24 --no-screen]" - соединить [(проба.«программа»), " [", (проба.«среда»), (если (проба.«ширина») равен "-" то "" иначе (соединить [" ", (проба.«ширина»), "×", (проба.«высота»)] по "")), (если (проба.«ключ») равен "-" то "" иначе (соединить [" ", (проба.«ключ»)] по "")), "]"] по "" + если («Поле» от части и 2) равен "pipe" + то «От корня» от (соединить ["{ ", («С меткой» от («Вызов» от части)), "; } | cat"] по "") + иначе «От корня» от («С меткой» от («В терминале» от части)) -тотальная функция «Жалоба» - принимает проба: «Проба», вывод: строка - возвращает список строки - пример «Сошлось — жалобы нет» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" - дано вывод равно "FLANG_IO_NO_SCREEN [КОД=1]" - ожидается пустой список - пример «Разошлось — жалоба называет ожидание и ответ» - дано проба равно запись «Проба» с «программа» равным "р.flang" и «среда» равным "труба" и «ширина» равным "-" и «высота» равным "-" и «ключ» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" - дано вывод равно "всё хорошо [КОД=0]" - ожидается [" · р.flang [труба] — ждали [КОД=1] и слово «FLANG_IO_NO_SCREEN», вывод: всё хорошо [КОД=0]"] - если (вывод содержит («Метка кода» от проба)) и притом (вывод содержит (проба.«слово»)) - то пустой список - иначе [(соединить [" · ", («Приметы» от проба), " — ждали ", («Метка кода» от проба), " и слово «", (проба.«слово»), "», вывод: ", («Кратко» от вывод)] по "")] - -тотальная функция «Слить» - принимает первые: список строки, вторые: список строки - возвращает список строки - пример «Два списка жалоб становятся одним» - дано первые равно ["раз"] - дано вторые равно ["два"] - ожидается ["раз", "два"] - свёртка вторые начиная с первые как собрано и жалоба → (добавить жалоба к собрано) - -тотальная функция «Итог» - принимает жалобы: список строки, сделано: число - возвращает «Продолжение» - пример «Все пробы сошлись — план доходит до конца» - дано жалобы равно пустой список - дано сделано равно 6 - ожидается вариант «Конец работы» с значение равным "пробы размера экрана: сошлось 6 из 6" - разбор жалобы - случай пусто - то вариант «Конец работы» с значение равным (соединить ["пробы размера экрана: сошлось ", (к строке сделано), " из ", (к строке сделано)] по "") - случай голова и хвост - то вариант «Провал» с код равным "FLANG_PROBY_RAZMERA_EKRANA" и сообщение равным (соединить (приписать (соединить ["пробы размера экрана РАЗОШЛИСЬ: ", (к строке (длина жалобы)), " из ", (к строке сделано)] по "") к жалобы) по "\n") +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["size.flang", "pipe", "-", "-", "-", "1", "FLANG_IO_NO_SCREEN"] + ожидается запись «Проба» с «программа» равным "size.flang" и «приметы» равным "size.flang [pipe]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { { $flang io 'flang/proof/probes/screen-size/programs/size.flang' ; } 2>&1; echo \"[code=$?]\"; } | cat" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2), («Поле» от части и 3), («Поле» от части и 4), («Поле» от части и 5)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 6) и «слово» равным («Поле» от части и 7) -тип «Ход» - вариант «Начало» - вариант «Ждём таблицу» - вариант «Ждём пробу» содержит проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) тотальная функция «Начать» возвращает «Ход» - пример «Первым делом читается таблица ожиданий» + пример «план начинается с начала» ожидается вариант «Начало» вариант «Начало» -тотальная функция «Пойти по пробам» - принимает очередь: список «Проба», жалобы: список строки, сделано: число - возвращает «Продолжение» - разбор очередь - случай пусто - то «Итог» от жалобы и сделано - случай голова и хвост - то вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", («Команда» от голова)]) и потом равным (вариант «Ждём пробу» с проба равным голова и осталось равным хвост и жалобы равным жалобы и сделано равным сделано) - -тотальная функция «Смотреть нечем» - принимает весть: строка - возвращает «Продолжение» - пример «Невозможность смотреть отделена от расхождения своим кодом» - дано весть равно "sh не запустился" - ожидается вариант «Провал» с код равным "FLANG_PROBY_RAZMERA_EKRANA_NECHEM" и сообщение равным "sh не запустился" - вариант «Провал» с код равным "FLANG_PROBY_RAZMERA_EKRANA_NECHEM" и сообщение равным весть - -тотальная функция «После пробы» - принимает проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число, отклик: «Отклик» - возвращает «Продолжение» - разбор отклик - случай вариант «Процесс завершён» с код как «код оболочки» и вывод как вывод и ошибки как ошибки - то «Пойти по пробам» от осталось и («Слить» от жалобы и («Жалоба» от проба и (соединить [вывод, ошибки] по " "))) и (сделано плюс 1) - случай вариант «Процесс убит» с сигнал как сигнал и вывод как вывод и ошибки как ошибки - то «Смотреть нечем» от (соединить ["проба ", («Приметы» от проба), " убита сигналом ", сигнал, " — это не расхождение, а невозможность смотреть"] по "") - случай вариант «Сбой» с код как «код беды» и сообщение как «весть беды» - то «Смотреть нечем» от (соединить ["оболочка не запустилась (", «код беды», "): ", «весть беды»] по "") - случай любое - то «Смотреть нечем» от "ждали ответ пробы" - -тотальная функция «После таблицы» - принимает отклик: «Отклик» - возвращает «Продолжение» - разбор отклик - случай вариант «Прочитано» с содержимое как содержимое - то «Пойти по пробам» от («Пробы» от содержимое) и (пустой список) и 0 - случай вариант «Сбой» с код как «код беды» и сообщение как «весть беды» - то «Смотреть нечем» от (соединить ["таблица ожиданий не прочитана (", «код беды», "): ", «весть беды»] по "") - случай любое - то «Смотреть нечем» от "ждали таблицу ожиданий" - тотальная функция «Дальше» принимает ход: «Ход», отклик: «Отклик» возвращает «Продолжение» разбор ход - случай вариант «Начало» - то вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "expected.tsv") и потом равным (вариант «Ждём таблицу») случай вариант «Ждём таблицу» - то «После таблицы» от отклик - случай вариант «Ждём пробу» с проба как проба и осталось как осталось и жалобы как жалобы и сделано как сделано - то «После пробы» от проба и осталось и жалобы и сделано и отклик + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик -план «Размер экрана двоичный хозяин отдаёт так, как обещано» +план «Binary» состояние «Ход» начинает с «Начать» обрабатывает «Дальше» diff --git a/flang/proof/probes/screen/expected.tsv b/flang/proof/probes/screen/expected.tsv index 2a1cce6c5..edae77355 100644 --- a/flang/proof/probes/screen/expected.tsv +++ b/flang/proof/probes/screen/expected.tsv @@ -1,38 +1,23 @@ -# Пробы ЭКРАНА двоичного хозяина: поручения «Показать» и «Ждать событие». -# Поля: программа, среда (терминал|труба), ключ (- — без ключей), ввод (что -# подать клавишами; `-` — не подавать ничего, \033 и прочее разворачивает -# printf %b), ожидаемый код возврата, слово, которое обязано стоять в выводе. -# -# СРЕДА ЗНАЧАЩАЯ, и в этом весь уговор: экран двоичного — управляющий терминал, -# и там, где вывод уведён в трубу, в файл, в CI или под nohup, ответ обязан -# остаться прежним отказом FLANG_IO_NO_SCREEN. Строка «труба» — не украшение -# набора, а фальсификатор: позеленей она кодом 0, и правка молча поменяла бы -# ответ всем неинтерактивным прогонам дерева. -# -# Терминал даёт `script -qec … /dev/null` — псевдотерминал без записи сеанса. -# Клавиши подаются с задержкой в секунду: до первого «Ждать событие» терминал -# ещё в построчном режиме, и знаки вроде 0x7F съела бы его же построчная -# правка, не доехав до хозяина. -программа среда ключ ввод код слово -frame-and-key.flang терминал - ы 0 пришло от «клавиатура»: «ы» -frame-and-key.flang терминал - a 0 пришло от «клавиатура»: «a» -frame-and-key.flang терминал - \033[A 0 пришло от «клавиатура»: «вверх» -frame-and-key.flang терминал - \033[B 0 пришло от «клавиатура»: «вниз» -frame-and-key.flang терминал - \033[C 0 пришло от «клавиатура»: «вправо» -frame-and-key.flang терминал - \033[D 0 пришло от «клавиатура»: «влево» -frame-and-key.flang терминал - \r 0 пришло от «клавиатура»: «ввод» -frame-and-key.flang терминал - \040 0 пришло от «клавиатура»: «пробел» -frame-and-key.flang терминал - \t 0 пришло от «клавиатура»: «таб» -frame-and-key.flang терминал - \177 0 пришло от «клавиатура»: «возврат» -frame-and-key.flang терминал - \033 0 пришло от «клавиатура»: «выход» -frame-and-key.flang терминал - - 0 срок вышел -frame-and-key.flang терминал - ы 0 [?1049h -frame-and-key.flang терминал - ы 0 [?1049l -frame-and-key.flang труба - - 1 FLANG_IO_NO_SCREEN -frame-and-key.flang терминал --no-screen - 1 FLANG_IO_DENIED -frame-and-key.flang труба --no-screen - 1 FLANG_IO_DENIED -foreign-place.flang терминал - - 1 FLANG_IO_PLACE -foreign-place.flang терминал - - 1 место у терминала одно и зовётся «экран» -foreign-place.flang труба - - 1 FLANG_IO_NO_SCREEN -deadline-passed.flang терминал - - 0 срок вышел -deadline-passed.flang труба - - 1 FLANG_IO_NO_SCREEN +program environment keys input code word +frame-and-key.flang terminal - ы 0 пришло от «клавиатура»: «ы» +frame-and-key.flang terminal - a 0 пришло от «клавиатура»: «a» +frame-and-key.flang terminal - \033[A 0 пришло от «клавиатура»: «вверх» +frame-and-key.flang terminal - \033[B 0 пришло от «клавиатура»: «вниз» +frame-and-key.flang terminal - \033[C 0 пришло от «клавиатура»: «вправо» +frame-and-key.flang terminal - \033[D 0 пришло от «клавиатура»: «влево» +frame-and-key.flang terminal - \r 0 пришло от «клавиатура»: «ввод» +frame-and-key.flang terminal - \040 0 пришло от «клавиатура»: «пробел» +frame-and-key.flang terminal - \t 0 пришло от «клавиатура»: «таб» +frame-and-key.flang terminal - \177 0 пришло от «клавиатура»: «возврат» +frame-and-key.flang terminal - \033 0 пришло от «клавиатура»: «выход» +frame-and-key.flang terminal - - 0 срок вышел +frame-and-key.flang terminal - ы 0 [?1049h +frame-and-key.flang terminal - ы 0 [?1049l +frame-and-key.flang pipe - - 1 FLANG_IO_NO_SCREEN +frame-and-key.flang terminal --no-screen - 1 FLANG_IO_DENIED +frame-and-key.flang pipe --no-screen - 1 FLANG_IO_DENIED +foreign-place.flang terminal - - 1 FLANG_IO_PLACE +foreign-place.flang terminal - - 1 место у терминала одно и зовётся «экран» +foreign-place.flang pipe - - 1 FLANG_IO_NO_SCREEN +deadline-passed.flang terminal - - 0 срок вышел +deadline-passed.flang pipe - - 1 FLANG_IO_NO_SCREEN diff --git a/flang/proof/probes/screen/run.fscript b/flang/proof/probes/screen/run.fscript index 1dade1672..bfe2c4675 100644 --- a/flang/proof/probes/screen/run.fscript +++ b/flang/proof/probes/screen/run.fscript @@ -1,231 +1,72 @@ модуль «Пробы экрана» -объект «Проба» - «программа»: строка - «среда»: строка - «ключ»: строка - «ввод»: строка - «код»: строка - «слово»: строка +использует «Таблица проб» из "../table.fscript" -тотальная функция «Поле» - принимает части: список строки, номер: число - возвращает строка - пример «Третье поле строки ожидания» - дано части равно ["кадр.flang", "труба", "-"] - дано номер равно 3 - ожидается "-" - пример «Номер за списком даёт пусто, а не отказ» - дано части равно ["кадр.flang"] - дано номер равно 4 - ожидается "" - если ((номер не меньше 1) и притом (номер не больше (длина части))) - то элемент номер в части - иначе "" - -тотальная функция «Строка годится» - принимает строка: строка - возвращает признак - пример «Строка ожидания годится» - дано строка равно "кадр.flang\tтруба\t-\t-\t1\tFLANG_IO_NO_SCREEN" - ожидается да - пример «Проза таблицы начинается с решётки» - дано строка равно "# пояснение" - ожидается нет - пример «Заголовок таблицы пробой не считается» - дано строка равно "программа\tсреда\tключ\tввод\tкод\tслово" - ожидается нет - пример «Пустая строка пробой не считается» - дано строка равно "" - ожидается нет - (не (строка начинается с "#")) и притом ((длина (разделить строка по "\t")) не меньше 6) и притом (не ((«Поле» от (разделить строка по "\t") и 1) равен "программа")) - -тотальная функция «Проба из строки» - принимает строка: строка - возвращает «Проба» - пример «Шесть полей становятся пробой» - дано строка равно "кадр.flang\tтруба\t-\t-\t1\tFLANG_IO_NO_SCREEN" - ожидается запись «Проба» с «программа» равным "кадр.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" - пусть части равно (разделить строка по "\t") - запись «Проба» с «программа» равным («Поле» от части и 1) и «среда» равным («Поле» от части и 2) и «ключ» равным («Поле» от части и 3) и «ввод» равным («Поле» от части и 4) и «код» равным («Поле» от части и 5) и «слово» равным («Поле» от части и 6) - -тотальная функция «Пробы» - принимает текст: строка - возвращает список «Проба» - пример «Из таблицы берутся только строки проб» - дано текст равно "# проза\nпрограмма\tсреда\tключ\tввод\tкод\tслово\nкадр.flang\tтруба\t-\t-\t1\tFLANG_IO_NO_SCREEN" - ожидается [запись «Проба» с «программа» равным "кадр.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN"] - отобразить (отфильтровать (разделить текст по "\n") где строка → («Строка годится» от строка)) как строка → («Проба из строки» от строка) - -тотальная функция «Ключи» - принимает проба: «Проба» - возвращает строка - пример «Прочерк значит без ключей» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "" - если (проба.«ключ») равен "-" - то "" - иначе проба.«ключ» +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "screen" и «код расхождения» равным "FLANG_PROBE_SCREEN" и «код слепоты» равным "FLANG_PROBE_SCREEN_CANNOT_LOOK" + запись «Набор» с «имя» равным "screen" и «код расхождения» равным "FLANG_PROBE_SCREEN" и «код слепоты» равным "FLANG_PROBE_SCREEN_CANNOT_LOOK" тотальная функция «Вызов» - принимает проба: «Проба» + принимает части: список строки возвращает строка - пример «Путь к плану собирается из имени programs» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "bootstrap/flang io 'flang/proof/probes/screen/programs/к.flang' " - соединить ["bootstrap/flang io 'flang/proof/probes/screen/programs/", (проба.«программа»), "' ", («Ключи» от проба)] по "" + соединить ["$flang io 'flang/proof/probes/screen/programs/", («Поле» от части и 1), "' ", («Ключи» от («Поле» от части и 3))] по "" тотальная функция «Подача» - принимает проба: «Проба» + принимает ввод: строка возвращает строка - пример «Без нажатий ввод держится открытым дольше самого долгого срока проб» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "терминал" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "0" и «слово» равным "с" + пример «без нажатий ввод держится открытым дольше самого долгого срока проб» + дано ввод равно "-" ожидается "{ sleep 5; }" - пример «Нажатие подаётся через секунду, когда терминал уже посимвольный» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "терминал" и «ключ» равным "-" и «ввод» равным "ы" и «код» равным "0" и «слово» равным "с" + пример «нажатие подаётся через секунду, когда терминал уже посимвольный» + дано ввод равно "ы" ожидается "{ sleep 1; printf '%b' 'ы'; sleep 1; }" - если (проба.«ввод») равен "-" + если ввод равен "-" то "{ sleep 5; }" - иначе соединить ["{ sleep 1; printf '%b' '", (проба.«ввод»), "'; sleep 1; }"] по "" + иначе соединить ["{ sleep 1; printf '%b' '", ввод, "'; sleep 1; }"] по "" -тотальная функция «Команда» - принимает проба: «Проба» - возвращает строка - пример «В трубе код возврата достаётся меткой, потому что после трубы он чужой» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "cd ../../../.. && { bootstrap/flang io 'flang/proof/probes/screen/programs/к.flang' 2>&1; echo \"[КОД=$?]\"; } | cat" - если (проба.«среда») равен "труба" - то соединить ["cd ../../../.. && { ", («Вызов» от проба), " 2>&1; echo \"[КОД=$?]\"; } | cat"] по "" - иначе соединить ["cd ../../../.. && ", («Подача» от проба), " | script -qec \"", («Вызов» от проба), "\" /dev/null; echo \"[КОД=$?]\""] по "" - -тотальная функция «Кратко» - принимает текст: строка +тотальная функция «В терминале» + принимает части: список строки возвращает строка - пример «Переводы строк становятся пробелами» - дано текст равно "раз\nдва" - ожидается "раз два" - пусть одной равно (соединить (разделить (соединить (разделить текст по "\n") по " ") по "\r") по "") - если (длина одной) не больше 400 - то одной - иначе подстрока одной с 1 по 400 + соединить [(«Подача» от («Поле» от части и 4)), " | script -qec \"", («Вызов» от части), "\" /dev/null"] по "" -тотальная функция «Метка кода» - принимает проба: «Проба» - возвращает строка - пример «Метка несёт ожидаемый код» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "с" - ожидается "[КОД=1]" - соединить ["[КОД=", (проба.«код»), "]"] по "" - -тотальная функция «Приметы» - принимает проба: «Проба» +тотальная функция «Команда» + принимает части: список строки возвращает строка - пример «Приметы называют программу, среду, ключ и ввод» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "терминал" и «ключ» равным "--no-screen" и «ввод» равным "ы" и «код» равным "1" и «слово» равным "с" - ожидается "к.flang [терминал --no-screen ввод ы]" - соединить [(проба.«программа»), " [", (проба.«среда»), (если (проба.«ключ») равен "-" то "" иначе (соединить [" ", (проба.«ключ»)] по "")), (если (проба.«ввод») равен "-" то "" иначе (соединить [" ввод ", (проба.«ввод»)] по "")), "]"] по "" - -тотальная функция «Жалоба» - принимает проба: «Проба», вывод: строка - возвращает список строки - пример «Сошлось — жалобы нет» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" - дано вывод равно "FLANG_IO_NO_SCREEN [КОД=1]" - ожидается пустой список - пример «Разошлось — жалоба называет ожидание и ответ» - дано проба равно запись «Проба» с «программа» равным "к.flang" и «среда» равным "труба" и «ключ» равным "-" и «ввод» равным "-" и «код» равным "1" и «слово» равным "FLANG_IO_NO_SCREEN" - дано вывод равно "всё хорошо [КОД=0]" - ожидается [" · к.flang [труба] — ждали [КОД=1] и слово «FLANG_IO_NO_SCREEN», вывод: всё хорошо [КОД=0]"] - если (вывод содержит («Метка кода» от проба)) и притом (вывод содержит (проба.«слово»)) - то пустой список - иначе [(соединить [" · ", («Приметы» от проба), " — ждали ", («Метка кода» от проба), " и слово «", (проба.«слово»), "», вывод: ", («Кратко» от вывод)] по "")] + если («Поле» от части и 2) равен "pipe" + то «От корня» от (соединить ["{ ", («С меткой» от («Вызов» от части)), "; } | cat"] по "") + иначе «От корня» от («С меткой» от («В терминале» от части)) -тотальная функция «Слить» - принимает первые: список строки, вторые: список строки - возвращает список строки - пример «Два списка жалоб становятся одним» - дано первые равно ["раз"] - дано вторые равно ["два"] - ожидается ["раз", "два"] - свёртка вторые начиная с первые как собрано и жалоба → (добавить жалоба к собрано) - -тотальная функция «Итог» - принимает жалобы: список строки, сделано: число - возвращает «Продолжение» - пример «Все пробы сошлись — план доходит до конца» - дано жалобы равно пустой список - дано сделано равно 22 - ожидается вариант «Конец работы» с значение равным "пробы экрана: сошлось 22 из 22" - разбор жалобы - случай пусто - то вариант «Конец работы» с значение равным (соединить ["пробы экрана: сошлось ", (к строке сделано), " из ", (к строке сделано)] по "") - случай голова и хвост - то вариант «Провал» с код равным "FLANG_PROBY_EKRANA" и сообщение равным (соединить (приписать (соединить ["пробы экрана РАЗОШЛИСЬ: ", (к строке (длина жалобы)), " из ", (к строке сделано)] по "") к жалобы) по "\n") +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["frame-and-key.flang", "terminal", "-", "ы", "0", "клавиатура"] + ожидается запись «Проба» с «программа» равным "frame-and-key.flang" и «приметы» равным "frame-and-key.flang [terminal ы]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { { sleep 1; printf '%b' 'ы'; sleep 1; } | script -qec \"$flang io 'flang/proof/probes/screen/programs/frame-and-key.flang' \" /dev/null; } 2>&1; echo \"[code=$?]\"" и «код» равным "0" и «слово» равным "клавиатура" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2), («Поле» от части и 3), («Поле» от части и 4)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 5) и «слово» равным («Поле» от части и 6) -тип «Ход» - вариант «Начало» - вариант «Ждём таблицу» - вариант «Ждём пробу» содержит проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) тотальная функция «Начать» возвращает «Ход» - пример «Первым делом читается таблица ожиданий» + пример «план начинается с начала» ожидается вариант «Начало» вариант «Начало» -тотальная функция «Пойти по пробам» - принимает очередь: список «Проба», жалобы: список строки, сделано: число - возвращает «Продолжение» - разбор очередь - случай пусто - то «Итог» от жалобы и сделано - случай голова и хвост - то вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", («Команда» от голова)]) и потом равным (вариант «Ждём пробу» с проба равным голова и осталось равным хвост и жалобы равным жалобы и сделано равным сделано) - -тотальная функция «Смотреть нечем» - принимает весть: строка - возвращает «Продолжение» - пример «Невозможность смотреть отделена от расхождения своим кодом» - дано весть равно "sh не запустился" - ожидается вариант «Провал» с код равным "FLANG_PROBY_EKRANA_NECHEM" и сообщение равным "sh не запустился" - вариант «Провал» с код равным "FLANG_PROBY_EKRANA_NECHEM" и сообщение равным весть - -тотальная функция «После пробы» - принимает проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число, отклик: «Отклик» - возвращает «Продолжение» - разбор отклик - случай вариант «Процесс завершён» с код как «код оболочки» и вывод как вывод и ошибки как ошибки - то «Пойти по пробам» от осталось и («Слить» от жалобы и («Жалоба» от проба и (соединить [вывод, ошибки] по " "))) и (сделано плюс 1) - случай вариант «Процесс убит» с сигнал как сигнал и вывод как вывод и ошибки как ошибки - то «Смотреть нечем» от (соединить ["проба ", («Приметы» от проба), " убита сигналом ", сигнал, " — это не расхождение, а невозможность смотреть"] по "") - случай вариант «Сбой» с код как «код беды» и сообщение как «весть беды» - то «Смотреть нечем» от (соединить ["оболочка не запустилась (", «код беды», "): ", «весть беды»] по "") - случай любое - то «Смотреть нечем» от "ждали ответ пробы" - -тотальная функция «После таблицы» - принимает отклик: «Отклик» - возвращает «Продолжение» - разбор отклик - случай вариант «Прочитано» с содержимое как содержимое - то «Пойти по пробам» от («Пробы» от содержимое) и (пустой список) и 0 - случай вариант «Сбой» с код как «код беды» и сообщение как «весть беды» - то «Смотреть нечем» от (соединить ["таблица ожиданий не прочитана (", «код беды», "): ", «весть беды»] по "") - случай любое - то «Смотреть нечем» от "ждали таблицу ожиданий" - тотальная функция «Дальше» принимает ход: «Ход», отклик: «Отклик» возвращает «Продолжение» разбор ход - случай вариант «Начало» - то вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "expected.tsv") и потом равным (вариант «Ждём таблицу») случай вариант «Ждём таблицу» - то «После таблицы» от отклик - случай вариант «Ждём пробу» с проба как проба и осталось как осталось и жалобы как жалобы и сделано как сделано - то «После пробы» от проба и осталось и жалобы и сделано и отклик + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик -план «Экран двоичного хозяина отвечает так, как обещано» +план «Binary» состояние «Ход» начинает с «Начать» обрабатывает «Дальше» diff --git a/flang/proof/probes/strict/expected.tsv b/flang/proof/probes/strict/expected.tsv index 1f22cecdb..b3742ef3c 100644 --- a/flang/proof/probes/strict/expected.tsv +++ b/flang/proof/probes/strict/expected.tsv @@ -1,22 +1,4 @@ -# ЧЕТЫРЕ ИСХОДА СТРОГОГО РЕЖИМА (задача 5502, пункт 5 внешнего аудита). -# -# Поля: программа, ключи (через пробел, «—» — без ключей), ожидаемый код -# возврата, слово, которое обязано стоять в выводе. Слово проверяется вместе с -# кодом нарочно: смена причины при том же коде — тоже расхождение, а не тишина -# (тот же довод, что у flang/proof/checker/tests/programs/lie-verdict.sh). -# -# ДВЕ ПОЛОВИНЫ ТАБЛИЦЫ, И ОБЕ ОБЯЗАТЕЛЬНЫ. -# · Строки без «--строго» — УМОЛЧАНИЕ. Оно правкой 5502 не тронуто ни на знак, и -# эти строки стерегут именно это: пять программ, у которых умолчание отвечает -# ровно как до правки. Разъехалось умолчание — сломано всё дерево разом. -# · Строки с «--строго» — сам строгий режим. Ноль в нём допустим ТОЛЬКО у -# «honest.flang»: у неё у каждого утверждения вердикт «доказано». -# -# ФАЛЬСИФИКАТОР задачи стоит первой парой строк: «false-postcondition.flang» лжёт -# постусловием («результат не больше 100» при теле «н плюс н»), и до правки ноль -# ей давали ВСЕ три прибора. Даст строгий режим ноль ей снова — задача не -# сделана. -программа ключи код слово +program keys code word false-postcondition.flang --proof 0 ПРОВЕРЕНО С ОПОРОЙ, И ОПОРА НЕ СУДИЛАСЬ false-postcondition.flang --proof --строго 3 НЕ УДАЛОСЬ ДОКАЗАТЬ — ОПОРА НЕ СУДИЛАСЬ false-postcondition-without-examples.flang --proof 3 НЕ ПРОВЕРЕНО @@ -37,6 +19,6 @@ refuted.flang --proof 1 FLANG_PROPERTY: нарушено свойство refuted.flang --proof --строго 1 FLANG_PROPERTY: нарушено свойство honest.flang --строго 2 осмыслен только рядом с «--proof» honest.flang --быстро 4 часть проверок НЕ ЗАПУСКАЛАСЬ — код возврата 4, а не 0 -honest.flang — 0 проверено — разбор, типы, завершаемость, ядро и примеры -false-postcondition.flang — 0 проверено — разбор, типы, завершаемость, ядро и примеры -no-obligations.flang — 0 проверено — разбор, типы, завершаемость, ядро и примеры +honest.flang - 0 проверено — разбор, типы, завершаемость, ядро и примеры +false-postcondition.flang - 0 проверено — разбор, типы, завершаемость, ядро и примеры +no-obligations.flang - 0 проверено — разбор, типы, завершаемость, ядро и примеры diff --git a/flang/proof/probes/strict/run.fscript b/flang/proof/probes/strict/run.fscript new file mode 100644 index 000000000..10afbef5b --- /dev/null +++ b/flang/proof/probes/strict/run.fscript @@ -0,0 +1,47 @@ +модуль «Пробы строгого режима» + +использует «Таблица проб» из "../table.fscript" + +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "strict" и «код расхождения» равным "FLANG_PROBE_STRICT" и «код слепоты» равным "FLANG_PROBE_STRICT_CANNOT_LOOK" + запись «Набор» с «имя» равным "strict" и «код расхождения» равным "FLANG_PROBE_STRICT" и «код слепоты» равным "FLANG_PROBE_STRICT_CANNOT_LOOK" + +тотальная функция «Команда» + принимает части: список строки + возвращает строка + «От корня» от («С меткой» от (соединить ["$flang check 'flang/proof/probes/strict/programs/", («Поле» от части и 1), "' ", («Ключи» от («Поле» от части и 2))] по "")) + +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["honest.flang", "--proof", "0", "ДОКАЗАНО"] + ожидается запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang [--proof]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { $flang check 'flang/proof/probes/strict/programs/honest.flang' --proof; } 2>&1; echo \"[code=$?]\"" и «код» равным "0" и «слово» равным "ДОКАЗАНО" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 3) и «слово» равным («Поле» от части и 4) + +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) + +тотальная функция «Начать» + возвращает «Ход» + пример «план начинается с начала» + ожидается вариант «Начало» + вариант «Начало» + +тотальная функция «Дальше» + принимает ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём таблицу» + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик + +план «Binary» + состояние «Ход» + начинает с «Начать» + обрабатывает «Дальше» diff --git a/flang/proof/probes/strict/run.sh b/flang/proof/probes/strict/run.sh deleted file mode 100755 index 959492315..000000000 --- a/flang/proof/probes/strict/run.sh +++ /dev/null @@ -1,105 +0,0 @@ -#!/bin/sh -# SPDX-FileCopyrightText: 2026 Digitable (Marat Zimnurov) -# SPDX-License-Identifier: BSD-2-Clause -# -# ПРОБЫ СТРОГОГО РЕЖИМА (задача 5502, пункт 5 внешнего аудита). -# -# sh flang/proof/probes/strict/run.sh -# FLANG_BIN=<путь> sh flang/proof/probes/strict/run.sh -# -# Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; -# 2 — не смог измерить (нет двоичного, нет таблицы). -# -# ── ЧТО ЗДЕСЬ СТЕРЕЖЁТСЯ ──────────────────────────────────────────────────── -# Внешний аудит, пункт 5, требует различать четыре исхода — «доказано», -# «опровергнуто», «не удалось доказать», «не поддерживается» — и запрещает -# успех без независимой проверки всех обязательств. Словами все четыре были -# названы и раньше; кодами возврата они не разъезжались, и два разных исхода -# ехали нулём. Сборочный сценарий читает `$?`, а не слова. -# -# ДЫРА, СНЯТАЯ ПРОГОНОМ 19 сентября 2026 (двоичный из этого дерева). Программа -# `programs/false-postcondition.flang` лжёт постусловием: обещает «результат не -# больше 100» при теле `н плюс н`, и опровергается на н = 100. Ответы приборов -# ДО правки: -# -# flang check код 0 -# flang check --proof код 0 ПРОВЕРЕНО С ОПОРОЙ, И ОПОРА -# НЕ СУДИЛАСЬ (спросить: --строго) -# flang check --proof --строго код 4 ПРОВЕРЕНО С ОПОРОЙ -# сверщик (по записи того же прогона) код 0 ПРОВЕРЕНО ВПУСТУЮ -# flang run --args '{"н": 100}' код 3 не доказано: утверждений 1 -# то же с --на-веру код 1 FLANG_PROPERTY: нарушено свойство -# -# Ноль ПОКУПАЛСЯ примером: тот же файл без строк `пример` -# (`programs/false-postcondition-without-examples.flang`) давал 3 и без всякого ключа. -# Пара этих двух файлов и держит разницу: одинаковая ложь, одинаковый приговор -# под `--строго` — и разный в умолчании. -# -# ── ЧЕГО ЭТОТ НАБОР НЕ ПРОВЕРЯЕТ ─────────────────────────────────────────── -# Он проверяет ОДИН прибор из двух — компилятор. Вторая половина исхода живёт в -# независимом сверщике (`flang/proof/checker/checker.c`): это он переигрывает -# снятия предусловий и он отвечает `ПРОВЕРЕНО ВПУСТУЮ` кодом 0 на записи, где -# доказанным не числится ничего. Ключ `--строго` у сверщика — отдельная работа, -# и пока её нет, строка «сверщик» из таблицы выше остаётся нулём. Говорить об -# этом надо вслух: строгий компилятор при мягком сверщике закрывает цепь не до -# конца. -# -# Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах -# (снято 17 сентября 2026 на соседнем наборе, `probes/run/run.sh`). -set -u - -KOREN=$(CDPATH= cd -- "$(dirname -- "$0")/../../../.." && pwd) -FLANG=${FLANG_BIN:-${FLANG:-$KOREN/bootstrap/flang}} -PROBY=$KOREN/flang/proof/probes/strict -export LC_ALL=C.UTF-8 - -[ -x "$FLANG" ] || { echo "нет двоичного: $FLANG (собрать: make -C bootstrap)" >&2; exit 2; } -[ -f "$PROBY/expected.tsv" ] || { echo "нет таблицы ожиданий: $PROBY/expected.tsv" >&2; exit 2; } - -RAB=$(mktemp -d -p "${FLANG_TMP:-${TMPDIR:-/tmp}}" proby-strogogo.XXXXXX) || exit 2 -trap 'rm -rf "$RAB"' EXIT INT TERM - -BAD=0; N=0 -awk -F'\t' '!/^#/ && $1 != "программа" && NF >= 4' "$PROBY/expected.tsv" > "$RAB/ожидание.tsv" - -while IFS="$(printf '\t')" read -r prog klyuchi kod slovo; do - N=$((N+1)) - f=$PROBY/programs/$prog - if [ ! -f "$f" ]; then - printf '✗ %-34s НЕТ ПРОГРАММЫ: %s\n' "$prog" "$f" - BAD=$((BAD+1)); continue - fi - # «—» в колонке ключей значит «без ключей»: пустое поле съела бы таблица. - [ "$klyuchi" = "—" ] && klyuchi="" - # Ключи разворачиваются намеренно без кавычек: в них нет ни пробелов внутри - # довода, ни образцов оболочки — только «--proof», «--строго», «--быстро». - out=$("$FLANG" check "$f" $klyuchi 2>&1); k=$? - if [ "$k" = "$kod" ] && printf '%s' "$out" | grep -q -a -F -- "$slovo"; then - printf '✓ %-34s %-18s код %s, есть «%s»\n' "$prog" "${klyuchi:-без ключей}" "$k" "$slovo" - else - printf '✗ %-34s %-18s ждали код %s и «%s», вышло код %s: %s\n' \ - "$prog" "${klyuchi:-без ключей}" "$kod" "$slovo" "$k" \ - "$(printf '%s' "$out" | tr '\n' ' ' | cut -c1-200)" - BAD=$((BAD+1)) - fi -done < "$RAB/ожидание.tsv" - -# ── Сверка с каталогом в обе стороны ─────────────────────────────────────── -# Программа, лежащая в каталоге и не названная в таблице, — дыра в надзоре: -# ровно так заводится файл, о котором никто не спросил ни одного кода. -for f in "$PROBY"/programs/*.flang; do - [ -e "$f" ] || continue - imya=$(basename "$f") - if ! cut -f1 "$RAB/ожидание.tsv" | grep -q -a -F -x -- "$imya"; then - printf '✗ НЕЗАЯВЛЕННАЯ ПРОГРАММА: %s лежит в каталоге, а строки о ней в expected.tsv нет\n' "$imya" - BAD=$((BAD+1)) - fi -done - -echo -if [ "$BAD" -eq 0 ]; then - echo "сошлось всё: проб $N, разошлось 0" - exit 0 -fi -echo "НЕ СОШЛОСЬ: проб $N, разошлось $BAD" -exit 1 diff --git a/flang/proof/probes/syllogism/expected.tsv b/flang/proof/probes/syllogism/expected.tsv index f14a663f1..338089d77 100644 --- a/flang/proof/probes/syllogism/expected.tsv +++ b/flang/proof/probes/syllogism/expected.tsv @@ -1,58 +1,4 @@ -# ПРОБЫ СИЛЛОГИЗМА (ADR-0047, задача 5309). -# -# Поля: программа, слово, которое обязано стоять в ответе ДВОИЧНОГО, слово, -# которое обязано стоять в ответе НАПЕЧАТАННОГО КОМПИЛЯТОРА. Слово, а не код: -# напечатанный компилятор отвечает строкой JSON, а не кодом возврата, и сверять -# оба одной меркой честнее, чем двумя разными. -# -# ── ДВА СТОЛБЦА, И ТЕПЕРЬ ОНИ ЖДУТ ОДНОГО И ТОГО ЖЕ ───────────────────────── -# Слово `следует` живёт в `flang/self/lexer.flang` и `flang/self/parser.flang`, -# а починка распаковки `таких что` — в `flang/self/proofterm.flang`; всё это -# печатаемая часть семени, и до перепечатки двоичный слова НЕ ЗНАЛ. Столбец -# «двоичный» тогда ждал от него ровно отказа разбора — это был замер «до». -# -# ПЕРЕПЕЧАТКА ПРОШЛА 25 сентября 2026 (выпуск 0.7.22, заход 23–25 сентября, -# 35 часов 45 минут), и замер «до» кончился вместе с ней: двоичный теперь несёт -# и слово, и починку. Столбец «двоичный» сведён с двоичным прогоном 26 сентября -# 2026 на дереве `gh/dev` `d5e203b89` — сошлись все шесть строк, и в каждой -# двоичный говорит ровно то же, что печатанный в JavaScript компилятор. -# -# ПОЧЕМУ СТОЛБЦЫ НЕ СЛИТЫ В ОДИН. Раз они совпали, таблица стала сверкой ДВУХ -# РЕАЛИЗАЦИЙ на одних программах: двоичный и компилятор, напечатанный в -# JavaScript (`run.sh --печатью`), обязаны отвечать одинаково. Разойдись они — -# красна будет та сторона, которая ушла, и видно это будет по столбцу. Слей их -# в один — и расхождение двух реализаций перестанет быть заметно вовсе. -# -# ── ЧТО СТЕРЕЖЁТ КАЖДАЯ СТРОКА ────────────────────────────────────────────── -# честный — силлогизм сахарной записью доказывается: три утверждения, все -# доказаны, шаг закрыт приложением посылки; -# изъятие — ФАЛЬСИФИКАТОР задачи 5309 в его переписанном виде: та же -# программа без посылки. Заключение обязано перестать доказываться. -# Код 0 здесь — задача не сделана; -# подделка — заключение ВЕРНО («ни один человек не крылат» — правда), но из -# названной посылки не следует. Отвергнуть его может только правило -# приложения, и оно обязано это сделать; -# цепочка — две посылки, вторая с ограничением `таких что`. До правки -# `flang/self/proofterm.flang` (распаковка `expr`, ADR-0047) ядро -# отвечало «ограничение «таких что» после подстановки не выведено»; -# строка стережёт, чтобы оно не вернулось. A/B снято 20 сентября -# 2026 на ОДНОЙ печати: та же сборка с откаченной строкой отвечает -# прежним отказом, с правкой — «доказано 5»; -# изъятие-жёсткое — ДЫРА, а не проверка, и стоит она здесь нарочно. Снесены и -# посылка, и вывод; остаётся заключение и предикат со своим -# постусловием «всякий человек смертен» — и заключение всё равно -# ДОКАЗАНО, код 0. Значит в этой форме оно от посылки не зависит: -# посылка и постусловие предиката говорят одно и то же дважды, а -# ядро берёт постусловие. Строка ходит храповиком: пока она ждёт -# «доказано», дыра открыта и названа; закроется — ожидание меняется -# вместе с задачей 5309; -# условный — цена закрытия той дыры. У предиката снято постусловие, и тогда -# заключение выводится ТОЛЬКО через посылку (изъятие посылки роняет -# его), но сама посылка становится «объявлено, не доказано», и весь -# файл уходит кодом 3 со словами «доказано ПРИ УСЛОВИИ». Выбор между -# этими двумя строками — не про слово поверхности, и ни один сахар -# его не снимает. -программа слово двоичного слово компилятора в JavaScript +program binary javascript honest.flang доказано 3 доказано 3 removal.flang ни одного шага ни одного шага forgery.flang не получается из цели утверждения подстановкой не получается из цели утверждения подстановкой diff --git a/flang/proof/probes/syllogism/run.fscript b/flang/proof/probes/syllogism/run.fscript new file mode 100644 index 000000000..bb7c43285 --- /dev/null +++ b/flang/proof/probes/syllogism/run.fscript @@ -0,0 +1,176 @@ +модуль «Пробы силлогизма» + +использует «Таблица проб» из "../table.fscript" + +тип «Ход печати» + вариант «Ждём каталог печати» + вариант «Ждём таблицу печати» содержит каталог: строка + вариант «Ждём исходник» содержит каталог: строка, строки: список список строки, готово: список «Проба» + вариант «Ждём запрос» содержит каталог: строка, строки: список список строки, готово: список «Проба» + вариант «Идут пробы» содержит ход: «Ход» + +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "syllogism" и «код расхождения» равным "FLANG_PROBE_SYLLOGISM" и «код слепоты» равным "FLANG_PROBE_SYLLOGISM_CANNOT_LOOK" + запись «Набор» с «имя» равным "syllogism" и «код расхождения» равным "FLANG_PROBE_SYLLOGISM" и «код слепоты» равным "FLANG_PROBE_SYLLOGISM_CANNOT_LOOK" + +тотальная функция «Проба двоичным» + принимает части: список строки + возвращает «Проба» + пример «двоичный спрашивается о доказательствах, и сверяется слово второго столбца» + дано части равно ["honest.flang", "доказано 3", "доказано 3"] + ожидается запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang [binary]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && { $flang check 'flang/proof/probes/syllogism/programs/honest.flang' --proof; } 2>&1; echo \"[code=$?]\"" и «код» равным "-" и «слово» равным "доказано 3" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и ["binary"]) и «команда» равным («От корня» от («С меткой» от (соединить ["$flang check 'flang/proof/probes/syllogism/programs/", («Поле» от части и 1), "' --proof"] по ""))) и «код» равным "-" и «слово» равным («Поле» от части и 2) + +тотальная функция «Путь запроса» + принимает каталог: строка, программа: строка + возвращает строка + пример «запрос лежит рядом с напечатанным компилятором» + дано каталог равно "/tmp/printed" + дано программа равно "honest.flang" + ожидается "/tmp/printed/request-honest.flang.json" + соединить [каталог, "/request-", программа, ".json"] по "" + +тотальная функция «Проба печатью» + принимает каталог: строка, части: список строки + возвращает «Проба» + пример «напечатанный компилятор читает запрос со входа, и сверяется слово третьего столбца» + дано каталог равно "/tmp/printed" + дано части равно ["honest.flang", "доказано 3", "доказано 3"] + ожидается запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang [javascript]" и «команда» равным "{ node '/tmp/printed/flang_cli.js' '/tmp/printed/compiler_flang.js' < '/tmp/printed/request-honest.flang.json'; } 2>&1; echo \"[code=$?]\"" и «код» равным "-" и «слово» равным "доказано 3" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и ["javascript"]) и «команда» равным («С меткой» от (соединить ["node '", каталог, "/flang_cli.js' '", каталог, "/compiler_flang.js' < '", («Путь запроса» от каталог и («Поле» от части и 1)), "'"] по "")) и «код» равным "-" и «слово» равным («Поле» от части и 3) + +тотальная функция «Заменить» + принимает текст: строка, что: строка, чем: строка + возвращает строка + пример «каждое вхождение заменено» + дано текст равно "а-б-в" + дано что равно "-" + дано чем равно "+" + ожидается "а+б+в" + соединить (разделить текст по что) по чем + +тотальная функция «Строкой JSON» + принимает текст: строка + возвращает строка + пример «кавычка, обратная черта и перевод строки заслонены» + дано текст равно "а\"б\\в\nг" + ожидается "\"а\\\"б\\\\в\\nг\"" + соединить ["\"", («Заменить» от («Заменить» от («Заменить» от («Заменить» от («Заменить» от текст и "\\" и "\\\\") и "\"" и "\\\"") и "\n" и "\\n") и "\r" и "\\r") и "\t" и "\\t"), "\""] по "" + +тотальная функция «Запрос» + принимает программа: строка, текст: строка + возвращает строка + пример «запрос зовёт отчёт о доказанном по одному исходнику» + дано программа равно "p.flang" + дано текст равно "модуль «П»" + ожидается "{\"fn\":\"Ведомость исходников\",\"args\":[{\"l\":[{\"r\":[[\"путь\",{\"s\":\"p.flang\"}],[\"текст\",{\"s\":\"модуль «П»\"}]]}]},{\"s\":\"p.flang\"}],\"depth\":\"100000\",\"steps\":\"2000000000\"}\n" + соединить ["{\"fn\":\"Ведомость исходников\",\"args\":[{\"l\":[{\"r\":[[\"путь\",{\"s\":", («Строкой JSON» от программа), "}],[\"текст\",{\"s\":", («Строкой JSON» от текст), "}]]}]},{\"s\":", («Строкой JSON» от программа), "}],\"depth\":\"100000\",\"steps\":\"2000000000\"}\n"] по "" + +тотальная функция «Под общим ходом» + принимает продолжение: «Продолжение» + возвращает «Продолжение» + пример «конец работы остаётся концом работы» + дано продолжение равно вариант «Конец работы» с значение равным "syllogism: проб 6, разошлось 0" + ожидается вариант «Конец работы» с значение равным "syllogism: проб 6, разошлось 0" + разбор продолжение + случай вариант «Сделать» с поручение как поручение и потом как следующий + то вариант «Сделать» с поручение равным поручение и потом равным (вариант «Идут пробы» с ход равным следующий) + случай любое + то продолжение + +тотальная функция «Готовить запросы» + принимает каталог: строка, строки: список список строки, готово: список «Проба» + возвращает «Продолжение» + разбор строки + случай пусто + то «Под общим ходом» от («После таблицы» от («Этот набор») и готово) + случай голова и хвост + то вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным (соединить ["programs/", («Поле» от голова и 1)] по "")) и потом равным (вариант «Ждём исходник» с каталог равным каталог и строки равным строки и готово равным готово) + +тотальная функция «Записать запрос» + принимает каталог: строка, строки: список список строки, готово: список «Проба», отклик: «Отклик» + возвращает «Продолжение» + разбор строки + случай пусто + то «Нечем смотреть» от («Этот набор») и "исходник прочитан, а строки таблицы о нём нет" + случай голова и хвост + то разбор отклик + случай вариант «Прочитано» с содержимое как текст + то вариант «Сделать» с поручение равным (вариант «Записать файл» с путь равным («Путь запроса» от каталог и («Поле» от голова и 1)) и содержимое равным («Запрос» от («Поле» от голова и 1) и текст)) и потом равным (вариант «Ждём запрос» с каталог равным каталог и строки равным строки и готово равным готово) + случай любое + то «Нечем смотреть» от («Этот набор») и (соединить ["программа не прочитана: ", («Поле» от голова и 1)] по "") + +тотальная функция «После запроса» + принимает каталог: строка, строки: список список строки, готово: список «Проба», отклик: «Отклик» + возвращает «Продолжение» + разбор строки + случай пусто + то «Нечем смотреть» от («Этот набор») и "запрос записан, а строки таблицы о нём нет" + случай голова и хвост + то разбор отклик + случай вариант «Записано» с сколько как сколько + то «Готовить запросы» от каталог и хвост и (добавить («Проба печатью» от каталог и голова) к готово) + случай любое + то «Нечем смотреть» от («Этот набор») и (соединить ["запрос не записан в каталог напечатанного компилятора: ", каталог] по "") + +тотальная функция «После каталога печати» + принимает отклик: «Отклик» + возвращает «Продолжение» + пример «без каталога напечатанного компилятора смотреть нечем» + дано отклик равно вариант «Переменной среды нет» + ожидается вариант «Не проверено» с код равным "FLANG_PROBE_SYLLOGISM_CANNOT_LOOK" и сообщение равным "syllogism: переменная PRINTED_COMPILER не называет каталог с compiler_flang.js и flang_cli.js" + разбор отклик + случай вариант «Пока ничего» + то вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "PRINTED_COMPILER") и потом равным (вариант «Ждём каталог печати») + случай вариант «Значение среды» с значение как каталог + то вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "expected.tsv") и потом равным (вариант «Ждём таблицу печати» с каталог равным каталог) + случай любое + то «Нечем смотреть» от («Этот набор») и "переменная PRINTED_COMPILER не называет каталог с compiler_flang.js и flang_cli.js" + +тотальная функция «Начать» + возвращает «Ход» + пример «план начинается с начала» + ожидается вариант «Начало» + вариант «Начало» + +тотальная функция «Дальше» + принимает ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём таблицу» + то «После таблицы» от («Этот набор») и (отобразить («Строки данных» от («Содержимое» от отклик)) как части → («Проба двоичным» от части)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик + +тотальная функция «Начать печатью» + возвращает «Ход печати» + пример «первым делом спрашивается каталог напечатанного компилятора» + ожидается вариант «Ждём каталог печати» + вариант «Ждём каталог печати» + +тотальная функция «Дальше печатью» + принимает ход: «Ход печати», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём каталог печати» + то «После каталога печати» от отклик + случай вариант «Ждём таблицу печати» с каталог как каталог + то «Готовить запросы» от каталог и («Строки данных» от («Содержимое» от отклик)) и (пустой список) + случай вариант «Ждём исходник» с каталог как каталог и строки как строки и готово как готово + то «Записать запрос» от каталог и строки и готово и отклик + случай вариант «Ждём запрос» с каталог как каталог и строки как строки и готово как готово + то «После запроса» от каталог и строки и готово и отклик + случай вариант «Идут пробы» с ход как общий + то «Под общим ходом» от («Шаг» от («Этот набор») и общий и отклик) + +план «Binary» + состояние «Ход» + начинает с «Начать» + обрабатывает «Дальше» + +план «JavaScript» + состояние «Ход печати» + начинает с «Начать печатью» + обрабатывает «Дальше печатью» diff --git a/flang/proof/probes/syllogism/run.sh b/flang/proof/probes/syllogism/run.sh deleted file mode 100755 index f2a6f6858..000000000 --- a/flang/proof/probes/syllogism/run.sh +++ /dev/null @@ -1,137 +0,0 @@ -#!/bin/sh -# SPDX-FileCopyrightText: 2026 Digitable (Marat Zimnurov) -# SPDX-License-Identifier: BSD-2-Clause -# -# ПРОБЫ СИЛЛОГИЗМА (ADR-0047, задача 5309). -# -# sh flang/proof/probes/syllogism/run.sh двоичным: замер «до» -# sh flang/proof/probes/syllogism/run.sh --печатью компилятором, напечатанным -# в JavaScript: замер «после» -# PECHAT=<каталог> sh … --печатью взять уже напечатанный компилятор оттуда, -# а не печатать заново (печать — 13 минут) -# -# Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; -# 2 — не смог измерить (нет двоичного, нет таблицы, нет node). -# -# ── ДВА ПУТИ, И ПОЧЕМУ ИХ ДВА ─────────────────────────────────────────────── -# Слово поверхности `следует` живёт в печатаемой части семени -# (`flang/self/lexer.flang`, `flang/self/parser.flang`), и там же живёт починка -# распаковки `таких что` (`flang/self/proofterm.flang`). Правка там доезжает до -# `bootstrap/flang` только полной перепечаткой. ПЕРЕПЕЧАТКА ПРОШЛА 25 сентября -# 2026 (выпуск 0.7.22): двоичный теперь знает и слово, и починку, и первый путь -# спрашивает у него ВЕРДИКТ, а не отказ разбора. Замер «до» кончился вместе с -# перепечаткой; чем он был и что показывал — в шапке expected.tsv. -# -# Второй путь ПЕЧАТАЕТ КОМПИЛЯТОР В JAVASCRIPT и спрашивает уже его. Теперь это -# не «замер после», а ВТОРОЙ СУДЬЯ: две реализации на одних программах обязаны -# отвечать одинаково, и таблица ждёт от них одних слов. Цена снята 20 сентября -# 2026 на машине `dev`: печать — 12 мин 50 с и 12,9 ГиБ один раз, 14,8 МБ JS; -# дальше каждая проба — СЕКУНДЫ. Способ и обе его ямы описаны заметкой -# docs/zettel/a-compiler-printed-to-javascript-runs-a-new-target-in-seconds.md. -# -# ── ПОЧЕМУ НЕ ЗОНДОМ, КАК У `пробы-запуска` ──────────────────────────────── -# Пробовали, и это замер, а не мнение. Зонд ведомости -# (`flang/self/bootstrap/zond-k7.flang`, «Ведомость исходников», толкование -# исходников нынешним двоичным) на этих же программах НЕ ДОСЧИТАЛСЯ ЗА -# ОДИННАДЦАТЬ ЧАСОВ и был снят сигналом 15, пик 24,7 ГиБ — три программы разом, -# 19–20 сентября 2026. То есть путь дороже самой перепечатки, ради обхода -# которой он заведён. Дешёвая его половина жива: разбор без доказательств -# (`zond-5309.flang`, «Печать разбора исходника») — две минуты и 1 ГиБ, и -# именно ею снято сличение деревьев в ADR-0047. -# -# Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах. -set -u - -KOREN=$(CDPATH= cd -- "$(dirname -- "$0")/../../../.." && pwd) -FLANG=${FLANG:-$KOREN/bootstrap/flang} -PROBY=$KOREN/flang/proof/probes/syllogism -TABLICA=$PROBY/expected.tsv -export LC_ALL=C.UTF-8 - -PECHATYU=0 -[ "${1:-}" = "--печатью" ] && PECHATYU=1 -[ -x "$FLANG" ] || { echo "нет двоичного: $FLANG" >&2; exit 2; } -[ -f "$TABLICA" ] || { echo "нет таблицы: $TABLICA" >&2; exit 2; } - -# Одна проба двоичным: код и вывод читаются вместе, вывод — в одну строку. -proba_binary() { # программа → печатает вывод одной строкой - out=$("$FLANG" check "$PROBY/programs/$1" --proof 2>&1) - printf '%s' "$out" | tr '\n' ' ' -} - -# Одна проба напечатанным компилятором. `следует` он знает, поэтому программа -# едет как есть; ответ — JSON, из него берутся слова ведомости либо первая беда. -proba_pechatyu() { # программа → печатает ответ одной строкой - f=$PROBY/programs/$1 - python3 -c ' -import json,sys -p,f=sys.argv[1],sys.argv[2] -ish={"r":[["путь",{"s":p}],["текст",{"s":open(f,encoding="utf-8").read()}]]} -print(json.dumps({"fn":"Ведомость исходников","args":[{"l":[ish]},{"s":p}], - "depth":"100000","steps":"2000000000"},ensure_ascii=False))' "$1" "$f" \ - | node "$PECHAT/flang_cli.js" "$PECHAT/compiler_flang.js" 2>&1 \ - | python3 -c ' -import json,sys -syr=sys.stdin.read() -try: d=json.loads(syr) -except Exception: print(syr.replace("\n"," ")[:400]); raise SystemExit -if not d.get("ok"): - print("ОТКАЗ ПРОГОНЩИКА "+str(d.get("code"))+": "+str(d.get("message"))[:300]); raise SystemExit -polya=dict(d["value"]["r"]) -if polya["годно"]: - print(polya["словами"]["s"].replace("\n"," ")) -else: - bedy=polya.get("диагностики",{}).get("l",[]) - kuski=[] - for b in bedy: - q=dict(b["r"]); kuski.append(q["код"]["s"]+": "+q["сообщение"]["s"]) - print(" | ".join(kuski) if kuski else "не годно, препятствие")' -} - -BAD=0 -VSEGO=0 -say() { printf '%s\n' "$*"; } - -if [ "$PECHATYU" = "1" ]; then - command -v node > /dev/null 2>&1 || { echo "нет node — путь «--печатью» без него не считается" >&2; exit 2; } - command -v python3 > /dev/null 2>&1 || { echo "нет python3" >&2; exit 2; } - if [ -z "${PECHAT:-}" ]; then - PECHAT=$(mktemp -d -p "${FLANG_TMP:-/srv/tmp}" pechat-sillogizma.XXXXXX) - say "печатаю компилятор в JavaScript (около 13 минут, 13 ГиБ): $PECHAT" - "$FLANG" emit "$KOREN/flang/self/bootstrap/compiler.flang" --target js --no-check \ - --max-steps 200000000 --out "$PECHAT" > "$PECHAT/печать.log" 2>&1 \ - || { echo "печать не удалась, см. $PECHAT/печать.log" >&2; exit 2; } - fi - export PECHAT - [ -f "$PECHAT/compiler_flang.js" ] || { echo "в $PECHAT нет compiler_flang.js" >&2; exit 2; } -fi - -say "таблица: $TABLICA" -say "путь: $([ "$PECHATYU" = "1" ] && echo "печатью ($PECHAT)" || echo 'двоичным (замер «до»)')" -say "" - -while IFS=" " read -r prog slovo_bin slovo_posle; do - case "$prog" in \#*|programma|программа|"") continue ;; esac - VSEGO=$((VSEGO + 1)) - if [ "$PECHATYU" = "1" ]; then - zhdyom=$slovo_posle - vyvod=$(proba_pechatyu "$prog") - else - zhdyom=$slovo_bin - vyvod=$(proba_binary "$prog") - fi - case "$vyvod" in - *"$zhdyom"*) say "СОШЛОСЬ $prog — «$zhdyom»" ;; - *) say "ПРОВАЛ $prog — ждали «$zhdyom»" - say " получили: $(printf '%s' "$vyvod" | cut -c1-260)" - BAD=$((BAD + 1)) ;; - esac -done < "$TABLICA" - -say "" -if [ "$BAD" -eq 0 ]; then - say "сошлось всё: проб $VSEGO" - exit 0 -fi -say "разошлось $BAD из $VSEGO" -exit 1 diff --git a/flang/proof/probes/table.fscript b/flang/proof/probes/table.fscript new file mode 100644 index 000000000..06ec0403e --- /dev/null +++ b/flang/proof/probes/table.fscript @@ -0,0 +1,292 @@ +модуль «Таблица проб» + +объект «Набор» + «имя»: строка + «код расхождения»: строка + «код слепоты»: строка + +объект «Проба» + «программа»: строка + «приметы»: строка + «команда»: строка + «код»: строка + «слово»: строка + +тип «Ход» + вариант «Начало» + вариант «Ждём таблицу» + вариант «Ждём каталог» содержит набор: «Набор», пробы: список «Проба» + вариант «Ждём пробу» содержит набор: «Набор», проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число + +тотальная функция «Поле» + принимает части: список строки, номер: число + возвращает строка + пример «третье поле строки» + дано части равно ["honest.flang", "--proof", "0"] + дано номер равно 3 + ожидается "0" + пример «номер за списком даёт пусто, а не отказ» + дано части равно ["honest.flang"] + дано номер равно 4 + ожидается "" + если ((номер не меньше 1) и притом (номер не больше (длина части))) + то элемент номер в части + иначе "" + +тотальная функция «Без заголовка» + принимает строки: список строки + возвращает список строки + пример «первая строка таблицы — имена столбцов» + дано строки равно ["program\tcode", "honest.flang\t0"] + ожидается ["honest.flang\t0"] + пример «пустая таблица остаётся пустой» + дано строки равно пустой список + ожидается пустой список + разбор строки + случай пусто + то пустой список + случай голова и хвост + то хвост + +тотальная функция «Строки данных» + принимает текст: строка + возвращает список список строки + пример «строка данных режется на поля по табуляции» + дано текст равно "program\tcode\nhonest.flang\t0\n" + ожидается [["honest.flang", "0"]] + отобразить (отфильтровать («Без заголовка» от (разделить текст по "\n")) где строка → не (строка равен "")) как строка → (разделить строка по "\t") + +тотальная функция «Содержимое» + принимает отклик: «Отклик» + возвращает строка + пример «прочитанный файл отдаёт текст» + дано отклик равно вариант «Прочитано» с содержимое равным "program\tcode" + ожидается "program\tcode" + пример «всякий другой отклик — пустой текст» + дано отклик равно вариант «Пока ничего» + ожидается "" + разбор отклик + случай вариант «Прочитано» с содержимое как содержимое + то содержимое + случай любое + то "" + +тотальная функция «Ключи» + принимает ячейка: строка + возвращает строка + пример «прочерк значит пусто» + дано ячейка равно "-" + ожидается "" + пример «ключи едут как написаны» + дано ячейка равно "--proof --строго" + ожидается "--proof --строго" + если ячейка равен "-" + то "" + иначе ячейка + +тотальная функция «Приметы» + принимает программа: строка, отличия: список строки + возвращает строка + пример «приметы — программа и то, чем проба отличается от соседних» + дано программа равно "honest.flang" + дано отличия равно ["--proof", "-"] + ожидается "honest.flang [--proof]" + соединить [программа, " [", (соединить (отфильтровать отличия где ячейка → не (ячейка равен "-")) по " "), "]"] по "" + +тотальная функция «От корня» + принимает вызов: строка + возвращает строка + пример «команда идёт из корня дерева, двоичный берётся из среды или из сборки» + дано вызов равно "$flang check x" + ожидается "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && $flang check x" + соединить ["cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && ", вызов] по "" + +тотальная функция «С меткой» + принимает вызов: строка + возвращает строка + пример «код возврата печатается меткой следом за выводом» + дано вызов равно "$flang check x" + ожидается "{ $flang check x; } 2>&1; echo \"[code=$?]\"" + соединить ["{ ", вызов, "; } 2>&1; echo \"[code=$?]\""] по "" + +тотальная функция «Метка» + принимает код: строка + возвращает строка + пример «метка несёт ожидаемый код» + дано код равно "3" + ожидается "[code=3]" + пример «прочерк значит, что код не сверяется» + дано код равно "-" + ожидается "" + если код равен "-" + то "" + иначе соединить ["[code=", код, "]"] по "" + +тотальная функция «Кратко» + принимает текст: строка + возвращает строка + пример «переводы строк становятся пробелами» + дано текст равно "раз\nдва" + ожидается "раз два" + пусть одной равно (соединить (разделить (соединить (разделить текст по "\n") по " ") по "\r") по "") + если (длина одной) не больше 400 + то одной + иначе подстрока одной с 1 по 400 + +тотальная функция «Сошлась» + принимает проба: «Проба», вывод: строка + возвращает признак + пример «код и слово сошлись» + дано проба равно запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang []" и «команда» равным "" и «код» равным "0" и «слово» равным "ДОКАЗАНО" + дано вывод равно "ДОКАЗАНО [code=0]" + ожидается да + пример «слово сошлось, код нет» + дано проба равно запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang []" и «команда» равным "" и «код» равным "0" и «слово» равным "ДОКАЗАНО" + дано вывод равно "ДОКАЗАНО [code=3]" + ожидается нет + (вывод содержит («Метка» от (проба.«код»))) и притом (вывод содержит (проба.«слово»)) + +тотальная функция «Ожидание» + принимает проба: «Проба» + возвращает строка + пример «код и слово» + дано проба равно запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "" и «команда» равным "" и «код» равным "0" и «слово» равным "ДОКАЗАНО" + ожидается "код 0 и слово «ДОКАЗАНО»" + пример «код не сверяется — назван только слово» + дано проба равно запись «Проба» с «программа» равным "chain.flang" и «приметы» равным "" и «команда» равным "" и «код» равным "-" и «слово» равным "доказано 5" + ожидается "слово «доказано 5»" + если (проба.«код») равен "-" + то соединить ["слово «", (проба.«слово»), "»"] по "" + иначе соединить ["код ", (проба.«код»), " и слово «", (проба.«слово»), "»"] по "" + +тотальная функция «Жалоба» + принимает проба: «Проба», вывод: строка + возвращает строка + пример «жалоба называет пробу, ожидание и ответ» + дано проба равно запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "honest.flang [--proof]" и «команда» равным "" и «код» равным "0" и «слово» равным "ДОКАЗАНО" + дано вывод равно "НЕ ПРОВЕРЕНО\n[code=3]" + ожидается "honest.flang [--proof] — ждали код 0 и слово «ДОКАЗАНО», вывод: НЕ ПРОВЕРЕНО [code=3]" + соединить [(проба.«приметы»), " — ждали ", («Ожидание» от проба), ", вывод: ", («Кратко» от вывод)] по "" + +тотальная функция «Незаявленные» + принимает имена: список строки, пробы: список «Проба» + возвращает список строки + пример «программа без строки в таблице названа поимённо» + дано имена равно ["honest.flang", "stray.flang"] + дано пробы равно [запись «Проба» с «программа» равным "honest.flang" и «приметы» равным "" и «команда» равным "" и «код» равным "0" и «слово» равным ""] + ожидается ["stray.flang"] + отфильтровать имена где имя → не (свёртка пробы начиная с нет как названа и проба → (названа или ((проба.«программа») равен имя))) + +тотальная функция «Нечем смотреть» + принимает набор: «Набор», весть: строка + возвращает «Продолжение» + пример «невозможность смотреть — не расхождение» + дано набор равно запись «Набор» с «имя» равным "strict" и «код расхождения» равным "FLANG_PROBE_STRICT" и «код слепоты» равным "FLANG_PROBE_STRICT_CANNOT_LOOK" + дано весть равно "sh не запустился" + ожидается вариант «Не проверено» с код равным "FLANG_PROBE_STRICT_CANNOT_LOOK" и сообщение равным "strict: sh не запустился" + вариант «Не проверено» с код равным (набор.«код слепоты») и сообщение равным (соединить [(набор.«имя»), ": ", весть] по "") + +тотальная функция «Расхождение» + принимает набор: «Набор», заголовок: строка, жалобы: список строки + возвращает «Продолжение» + пример «расхождение несёт код набора и жалобы по одной на строку» + дано набор равно запись «Набор» с «имя» равным "strict" и «код расхождения» равным "FLANG_PROBE_STRICT" и «код слепоты» равным "FLANG_PROBE_STRICT_CANNOT_LOOK" + дано заголовок равно "проб 20, разошлось 1" + дано жалобы равно ["honest.flang [] — не то"] + ожидается вариант «Провал» с код равным "FLANG_PROBE_STRICT" и сообщение равным "strict: проб 20, разошлось 1\n · honest.flang [] — не то" + вариант «Провал» с код равным (набор.«код расхождения») и сообщение равным (соединить (приписать (соединить [(набор.«имя»), ": ", заголовок] по "") к жалобы) по "\n · ") + +тотальная функция «Счёт» + принимает сделано: число, разошлось: число + возвращает строка + пример «счёт называет пробы и расхождения» + дано сделано равно 20 + дано разошлось равно 0 + ожидается "проб 20, разошлось 0" + соединить ["проб ", (к строке сделано), ", разошлось ", (к строке разошлось)] по "" + +тотальная функция «Итог» + принимает набор: «Набор», жалобы: список строки, сделано: число + возвращает «Продолжение» + пример «все пробы сошлись — план доходит до конца» + дано набор равно запись «Набор» с «имя» равным "strict" и «код расхождения» равным "FLANG_PROBE_STRICT" и «код слепоты» равным "FLANG_PROBE_STRICT_CANNOT_LOOK" + дано жалобы равно пустой список + дано сделано равно 20 + ожидается вариант «Конец работы» с значение равным "strict: проб 20, разошлось 0" + разбор жалобы + случай пусто + то вариант «Конец работы» с значение равным (соединить [(набор.«имя»), ": ", («Счёт» от сделано и 0)] по "") + случай голова и хвост + то «Расхождение» от набор и («Счёт» от сделано и (длина жалобы)) и жалобы + +тотальная функция «Пойти по пробам» + принимает набор: «Набор», очередь: список «Проба», жалобы: список строки, сделано: число + возвращает «Продолжение» + разбор очередь + случай пусто + то «Итог» от набор и жалобы и сделано + случай голова и хвост + то вариант «Сделать» с поручение равным (вариант «Запустить процесс» с программа равным "sh" и аргументы равным ["-c", (голова.«команда»)]) и потом равным (вариант «Ждём пробу» с набор равным набор и проба равным голова и осталось равным хвост и жалобы равным жалобы и сделано равным сделано) + +тотальная функция «Прочитать таблицу» + возвращает «Продолжение» + пример «первым делом читается таблица ожиданий» + ожидается вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "expected.tsv") и потом равным (вариант «Ждём таблицу») + вариант «Сделать» с поручение равным (вариант «Прочитать файл» с путь равным "expected.tsv") и потом равным (вариант «Ждём таблицу») + +тотальная функция «После таблицы» + принимает набор: «Набор», пробы: список «Проба» + возвращает «Продолжение» + разбор пробы + случай пусто + то «Нечем смотреть» от набор и "в expected.tsv нет ни одной строки данных" + случай голова и хвост + то вариант «Сделать» с поручение равным (вариант «Перечислить каталог» с путь равным "programs") и потом равным (вариант «Ждём каталог» с набор равным набор и пробы равным пробы) + +тотальная функция «После каталога» + принимает набор: «Набор», пробы: список «Проба», отклик: «Отклик» + возвращает «Продолжение» + разбор отклик + случай вариант «Перечислено» с имена как имена + то разбор («Незаявленные» от имена и пробы) + случай пусто + то «Пойти по пробам» от набор и пробы и (пустой список) и 0 + случай голова и хвост + то «Расхождение» от набор и "программы лежат в каталоге, а строки о них в expected.tsv нет" и («Незаявленные» от имена и пробы) + случай вариант «Сбой» с код как код и сообщение как сообщение + то «Нечем смотреть» от набор и (соединить ["каталог программ не прочитан (", код, "): ", сообщение] по "") + случай любое + то «Нечем смотреть» от набор и "ждали перечня каталога программ" + +тотальная функция «Принять вывод» + принимает набор: «Набор», проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число, вывод: строка + возвращает «Продолжение» + если вывод содержит "[code=127]" + то «Нечем смотреть» от набор и (соединить ["команда не найдена на пробе ", (проба.«приметы»), ": соберите двоичный — make -C bootstrap"] по "") + иначе «Пойти по пробам» от набор и осталось и (если («Сошлась» от проба и вывод) то жалобы иначе (добавить («Жалоба» от проба и вывод) к жалобы)) и (сделано плюс 1) + +тотальная функция «После пробы» + принимает набор: «Набор», проба: «Проба», осталось: список «Проба», жалобы: список строки, сделано: число, отклик: «Отклик» + возвращает «Продолжение» + разбор отклик + случай вариант «Процесс завершён» с код как код и вывод как вывод и ошибки как ошибки + то «Принять вывод» от набор и проба и осталось и жалобы и сделано и (соединить [вывод, ошибки] по " ") + случай вариант «Процесс убит» с сигнал как сигнал и вывод как вывод и ошибки как ошибки + то «Нечем смотреть» от набор и (соединить ["проба ", (проба.«приметы»), " убита сигналом ", сигнал] по "") + случай вариант «Сбой» с код как код и сообщение как сообщение + то «Нечем смотреть» от набор и (соединить ["sh не запустился (", код, "): ", сообщение] по "") + случай любое + то «Нечем смотреть» от набор и (соединить ["ждали ответа процесса на пробе ", (проба.«приметы»)] по "") + +тотальная функция «Шаг» + принимает набор: «Набор», ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Начало» + то «Прочитать таблицу» + случай вариант «Ждём таблицу» + то «Нечем смотреть» от набор и "таблицу ожиданий разбирает сам набор" + случай вариант «Ждём каталог» с набор как свой и пробы как пробы + то «После каталога» от свой и пробы и отклик + случай вариант «Ждём пробу» с набор как свой и проба как проба и осталось как осталось и жалобы как жалобы и сделано как сделано + то «После пробы» от свой и проба и осталось и жалобы и сделано и отклик diff --git a/flang/proof/probes/unproven/expected.tsv b/flang/proof/probes/unproven/expected.tsv index b89c8509b..0fa62511a 100644 --- a/flang/proof/probes/unproven/expected.tsv +++ b/flang/proof/probes/unproven/expected.tsv @@ -1,33 +1,33 @@ -программа путь файл среда ключи код слово -unproven.flang run — — — 3 — запуск только по явному согласию: --на-веру -unproven.flang run — — --trust 0 на веру: доказанность не считалась — запуск по ключу --trust -unproven.flang run — — --на-веру 0 на веру: доказанность не считалась — запуск по ключу --на-веру -unproven.flang run unproven = allow — — 0 запуск по настройке «unproven = allow» -unproven.flang run unproven = allow — --unproven refuse 3 — запуск только по явному согласию: --trust -unproven.flang run unproven = allow — --недоказанное отказ 3 — запуск только по явному согласию: --на-веру -unproven.flang run unproven = warn — — 0 запуск по настройке «unproven = warn» -unproven.flang run unproven = refuse — — 3 — запуск только по явному согласию: --trust -unproven.flang run unproven = allowed — — 2 такого значения у «unproven» нет -unproven.flang run — allow — 0 запуск по переменной среды FLANG_UNPROVEN=allow -unproven.flang run unproven = allow refuse — 3 — запуск только по явному согласию: --trust -unproven.flang run — да — 2 такого значения у «unproven» нет -unproven.flang run чепуха = что угодно — — 3 — запуск только по явному согласию: --на-веру -unproven.flang run недоказанное = разрешение — — 0 запуск по настройке «недоказанное = разрешение» -unproven.flang run недоказанное = разрешение — — 0 замените её на «unproven = allow» -unproven.flang run недоказанное = предупреждение — — 0 замените её на «unproven = warn» -unproven.flang run недоказанное = отказ — — 3 замените её на «unproven = refuse» -unproven.flang run недоказанное = allow — — 0 замените её на «unproven = allow» -unproven.flang run unproven = разрешение — — 0 замените её на «unproven = allow» -unproven.flang run недоказанное = разрешено — — 2 такого значения у «недоказанное» нет -unproven.flang run недоказанное = разрешение — --unproven refuse 3 — запуск только по явному согласию: --trust -unproven.flang run недоказанное = разрешение refuse — 3 — запуск только по явному согласию: --trust -proved.flang run — — — 0 доказано: утверждений 1 -proved.flang run unproven = warn — — 0 доказано: утверждений 1 -proved.flang run unproven = allow — — 0 на веру: доказанность не считалась -proved.flang run недоказанное = предупреждение — — 0 доказано: утверждений 1 -plan-unproven.flang io — — — 3 — запуск только по явному согласию: --на-веру -plan-unproven.flang io — — --trust 0 на веру: доказанность не считалась — запуск по ключу --trust -plan-unproven.flang io unproven = allow — — 0 запуск по настройке «unproven = allow» -plan-unproven.flang io unproven = warn — — 0 запуск по настройке «unproven = warn» -plan-unproven.flang io unproven = allowed — — 2 такого значения у «unproven» нет -plan-unproven.flang io недоказанное = разрешение — — 0 замените её на «unproven = allow» +program command settings environment keys code word +unproven.flang run - - - 3 — запуск только по явному согласию: --на-веру +unproven.flang run - - --trust 0 на веру: доказанность не считалась — запуск по ключу --trust +unproven.flang run - - --на-веру 0 на веру: доказанность не считалась — запуск по ключу --на-веру +unproven.flang run unproven = allow - - 0 запуск по настройке «unproven = allow» +unproven.flang run unproven = allow - --unproven refuse 3 — запуск только по явному согласию: --trust +unproven.flang run unproven = allow - --недоказанное отказ 3 — запуск только по явному согласию: --на-веру +unproven.flang run unproven = warn - - 0 запуск по настройке «unproven = warn» +unproven.flang run unproven = refuse - - 3 — запуск только по явному согласию: --trust +unproven.flang run unproven = allowed - - 2 такого значения у «unproven» нет +unproven.flang run - allow - 0 запуск по переменной среды FLANG_UNPROVEN=allow +unproven.flang run unproven = allow refuse - 3 — запуск только по явному согласию: --trust +unproven.flang run - да - 2 такого значения у «unproven» нет +unproven.flang run чепуха = что угодно - - 3 — запуск только по явному согласию: --на-веру +unproven.flang run недоказанное = разрешение - - 0 запуск по настройке «недоказанное = разрешение» +unproven.flang run недоказанное = разрешение - - 0 замените её на «unproven = allow» +unproven.flang run недоказанное = предупреждение - - 0 замените её на «unproven = warn» +unproven.flang run недоказанное = отказ - - 3 замените её на «unproven = refuse» +unproven.flang run недоказанное = allow - - 0 замените её на «unproven = allow» +unproven.flang run unproven = разрешение - - 0 замените её на «unproven = allow» +unproven.flang run недоказанное = разрешено - - 2 такого значения у «недоказанное» нет +unproven.flang run недоказанное = разрешение - --unproven refuse 3 — запуск только по явному согласию: --trust +unproven.flang run недоказанное = разрешение refuse - 3 — запуск только по явному согласию: --trust +proved.flang run - - - 0 доказано: утверждений 1 +proved.flang run unproven = warn - - 0 доказано: утверждений 1 +proved.flang run unproven = allow - - 0 на веру: доказанность не считалась +proved.flang run недоказанное = предупреждение - - 0 доказано: утверждений 1 +plan-unproven.flang io - - - 3 — запуск только по явному согласию: --на-веру +plan-unproven.flang io - - --trust 0 на веру: доказанность не считалась — запуск по ключу --trust +plan-unproven.flang io unproven = allow - - 0 запуск по настройке «unproven = allow» +plan-unproven.flang io unproven = warn - - 0 запуск по настройке «unproven = warn» +plan-unproven.flang io unproven = allowed - - 2 такого значения у «unproven» нет +plan-unproven.flang io недоказанное = разрешение - - 0 замените её на «unproven = allow» diff --git a/flang/proof/probes/unproven/run.fscript b/flang/proof/probes/unproven/run.fscript new file mode 100644 index 000000000..fcf2a69a4 --- /dev/null +++ b/flang/proof/probes/unproven/run.fscript @@ -0,0 +1,67 @@ +модуль «Пробы ворот недоказанного» + +использует «Таблица проб» из "../table.fscript" + +тотальная функция «Этот набор» + возвращает «Набор» + пример «набор назван, и у расхождения и слепоты разные коды» + ожидается запись «Набор» с «имя» равным "unproven" и «код расхождения» равным "FLANG_PROBE_UNPROVEN" и «код слепоты» равным "FLANG_PROBE_UNPROVEN_CANNOT_LOOK" + запись «Набор» с «имя» равным "unproven" и «код расхождения» равным "FLANG_PROBE_UNPROVEN" и «код слепоты» равным "FLANG_PROBE_UNPROVEN_CANNOT_LOOK" + +тотальная функция «Настройка» + принимает ячейка: строка + возвращает строка + пример «прочерк значит, что файла настроек в песочнице нет» + дано ячейка равно "-" + ожидается "true" + пример «строка настройки ложится в файл настроек песочницы» + дано ячейка равно "недоказанное = allow" + ожидается "printf '%s\\n' 'недоказанное = allow' > \"$box/.flangrc\"" + если ячейка равен "-" + то "true" + иначе соединить ["printf '%s\\n' '", ячейка, "' > \"$box/.flangrc\""] по "" + +тотальная функция «Действие» + принимает части: список строки + возвращает строка + если («Поле» от части и 2) равен "io" + то соединить ["io '", («Поле» от части и 1), "' --max-steps 1000000"] по "" + иначе соединить ["run '", («Поле» от части и 1), "' --function «Ответ»"] по "" + +тотальная функция «Команда» + принимает части: список строки + возвращает строка + «От корня» от (соединить ["box=$(mktemp -d -p \"${FLANG_TMP:-${TMPDIR:-/tmp}}\" probe-unproven.XXXXXX) && cp 'flang/proof/probes/unproven/programs/", («Поле» от части и 1), "' \"$box/\" && : > \"$box/.git\" && mkdir \"$box/home\" && ", («Настройка» от («Поле» от части и 3)), " && cd \"$box\" && ", («С меткой» от (соединить ["HOME=\"$box/home\" FLANG_UNPROVEN='", («Ключи» от («Поле» от части и 4)), "' $flang ", («Действие» от части), " ", («Ключи» от («Поле» от части и 5))] по "")), "; rm -rf \"$box\""] по "") + +тотальная функция «Проба из строки» + принимает части: список строки + возвращает «Проба» + пример «строка таблицы становится пробой» + дано части равно ["proved.flang", "run", "-", "-", "-", "0", "доказано"] + ожидается запись «Проба» с «программа» равным "proved.flang" и «приметы» равным "proved.flang [run]" и «команда» равным "cd ../../../.. && root=$PWD && flang=${FLANG_BIN:-$root/bootstrap/flang} && box=$(mktemp -d -p \"${FLANG_TMP:-${TMPDIR:-/tmp}}\" probe-unproven.XXXXXX) && cp 'flang/proof/probes/unproven/programs/proved.flang' \"$box/\" && : > \"$box/.git\" && mkdir \"$box/home\" && true && cd \"$box\" && { HOME=\"$box/home\" FLANG_UNPROVEN='' $flang run 'proved.flang' --function «Ответ» ; } 2>&1; echo \"[code=$?]\"; rm -rf \"$box\"" и «код» равным "0" и «слово» равным "доказано" + запись «Проба» с «программа» равным («Поле» от части и 1) и «приметы» равным («Приметы» от («Поле» от части и 1) и [(«Поле» от части и 2), («Поле» от части и 3), («Поле» от части и 4), («Поле» от части и 5)]) и «команда» равным («Команда» от части) и «код» равным («Поле» от части и 6) и «слово» равным («Поле» от части и 7) + +тотальная функция «Пробы» + принимает текст: строка + возвращает список «Проба» + отобразить («Строки данных» от текст) как части → («Проба из строки» от части) + +тотальная функция «Начать» + возвращает «Ход» + пример «план начинается с начала» + ожидается вариант «Начало» + вариант «Начало» + +тотальная функция «Дальше» + принимает ход: «Ход», отклик: «Отклик» + возвращает «Продолжение» + разбор ход + случай вариант «Ждём таблицу» + то «После таблицы» от («Этот набор») и («Пробы» от («Содержимое» от отклик)) + случай любое + то «Шаг» от («Этот набор») и ход и отклик + +план «Binary» + состояние «Ход» + начинает с «Начать» + обрабатывает «Дальше» diff --git a/flang/proof/probes/unproven/run.sh b/flang/proof/probes/unproven/run.sh deleted file mode 100644 index e62964b2a..000000000 --- a/flang/proof/probes/unproven/run.sh +++ /dev/null @@ -1,109 +0,0 @@ -#!/bin/sh -# SPDX-FileCopyrightText: 2026 Digitable (Marat Zimnurov) -# SPDX-License-Identifier: BSD-2-Clause -# -# ПРОБЫ ВОРОТ НЕДОКАЗАННОГО (ADR-0045; docs/guide/settings.ru.md). -# -# sh flang/proof/probes/unproven/run.sh -# FLANG_BIN=<путь> sh flang/proof/probes/unproven/run.sh -# -# Код 0 — сошлось всё; 1 — хоть одна проба разошлась, и она названа строкой; -# 2 — не смог измерить (нет двоичного, нет таблицы). -# -# ── ЧТО ЗДЕСЬ СТЕРЕЖЁТСЯ ──────────────────────────────────────────────────── -# С 0.7.21 недоказанная программа не считается вовсе (`flang/proof/probes/run` -# держит это), а пропустить проверку можно ключом. Этот набор — про ДРУГОЕ: про -# то, КАК человек управляет воротами и ЧТО ему на это отвечают. -# -# · три исхода вместо двух: отказ, предупреждение, разрешение; -# · старшинство: ключ команды → FLANG_UNPROVEN → .flangrc проекта → -# .flangrc дома → умолчание «отказ»; -# · письмо ответа = письмо вопроса: набравший «--trust» получает в строке -# «--trust», а не «--на-веру». -# -# ── ПОЧЕМУ КАЖДАЯ ПРОБА ИДЁТ В СВОЁМ КАТАЛОГЕ, И ЗАЧЕМ В НЁМ ПУСТОЙ `.git` ── -# Настройки ищутся ОТ РАБОЧЕГО КАТАЛОГА ВВЕРХ, и подъём обрывает корневая -# примета. Без своей приметы проба взяла бы чужой `.flangrc` — хоть этого -# дерева, хоть `/tmp/.git`, который на машине разработчика существует (замер -# 8 сентября 2026, шапка scripts/flangrc.sh). Пустой файл `.git` рядом с -# программой обрывает подъём на первом же шаге, и проба судит РОВНО то, что -# ей положено. HOME отводится в пустой каталог по той же причине: `~/.flangrc` -# человека в пробу попадать не должен. -# -# Имена переменных латиницей: ни dash, ни bash не принимают кириллицу в именах. -set -u - -KOREN=$(CDPATH= cd -- "$(dirname -- "$0")/../../../.." && pwd) -FLANG=${FLANG_BIN:-${FLANG:-$KOREN/bootstrap/flang}} -PROBY=$KOREN/flang/proof/probes/unproven -export LC_ALL=C.UTF-8 - -[ -x "$FLANG" ] || { echo "нет двоичного: $FLANG (собрать: make -C bootstrap)" >&2; exit 2; } -[ -f "$PROBY/expected.tsv" ] || { echo "нет таблицы ожиданий: $PROBY/expected.tsv" >&2; exit 2; } - -RAB=$(mktemp -d -p "${FLANG_TMP:-${TMPDIR:-/tmp}}" proby-nedokazannogo.XXXXXX) || exit 2 -trap 'rm -rf "$RAB"' EXIT INT TERM -mkdir -p "$RAB/dom" - -BAD=0; N=0 -awk -F'\t' '!/^#/ && $1 != "программа" && NF >= 7' "$PROBY/expected.tsv" > "$RAB/ожидание.tsv" - -while IFS="$(printf '\t')" read -r prog put fajl sreda klyuchi kod slovo; do - N=$((N+1)) - ISHODNIK=$PROBY/programs/$prog - if [ ! -f "$ISHODNIK" ]; then - printf '✗ %-22s НЕТ ПРОГРАММЫ: %s\n' "$prog" "$ISHODNIK" - BAD=$((BAD+1)); continue - fi - - MESTO=$RAB/proba.$N - mkdir -p "$MESTO" - cp "$ISHODNIK" "$MESTO/" - : > "$MESTO/.git" - [ "$fajl" = "—" ] || printf '%s\n' "$fajl" > "$MESTO/.flangrc" - [ "$klyuchi" = "—" ] && klyuchi="" - - # Ключи разворачиваются без кавычек намеренно: пробелов внутри одного довода - # в этой таблице нет, а «--unproven refuse» — это два довода, и разделить их - # обязана именно оболочка. - # Пустая FLANG_UNPROVEN и незаданная — для двоичного одно и то же (проверка - # `env[0] != 0` в flang_repl.c), поэтому «—» кладётся пустой строкой. - SREDA=$sreda; [ "$SREDA" = "—" ] && SREDA="" - if [ "$put" = run ]; then - out=$(cd "$MESTO" && HOME=$RAB/dom FLANG_UNPROVEN=$SREDA \ - "$FLANG" run "$prog" --function «Ответ» $klyuchi 2>&1); k=$? - else - out=$(cd "$MESTO" && HOME=$RAB/dom FLANG_UNPROVEN=$SREDA \ - "$FLANG" io "$prog" --max-steps 1000000 $klyuchi 2>&1); k=$? - fi - - if [ "$k" = "$kod" ] && printf '%s' "$out" | grep -q -a -F -- "$slovo"; then - printf '✓ %-22s %-4s файл «%s» среда «%s» ключи «%s» → код %s\n' \ - "$prog" "$put" "$fajl" "$sreda" "${klyuchi:-—}" "$k" - else - printf '✗ %-22s %-4s файл «%s» среда «%s» ключи «%s»: ждали код %s и «%s», вышло код %s: %s\n' \ - "$prog" "$put" "$fajl" "$sreda" "${klyuchi:-—}" "$kod" "$slovo" "$k" \ - "$(printf '%s' "$out" | tr '\n' ' ' | cut -c1-200)" - BAD=$((BAD+1)) - fi -done < "$RAB/ожидание.tsv" - -# ── Сверка с каталогом в обе стороны ─────────────────────────────────────── -# Программа, лежащая в каталоге и не названная в таблице, — дыра в надзоре: -# ровно так заводится файл, о котором никто не спросил ни одного кода. -for f in "$PROBY"/programs/*.flang; do - [ -e "$f" ] || continue - imya=$(basename "$f") - if ! cut -f1 "$RAB/ожидание.tsv" | grep -q -a -F -x -- "$imya"; then - printf '✗ НЕЗАЯВЛЕННАЯ ПРОГРАММА: %s лежит в каталоге, а строки о ней в expected.tsv нет\n' "$imya" - BAD=$((BAD+1)) - fi -done - -echo -if [ "$BAD" -eq 0 ]; then - echo "сошлось всё: проб $N, разошлось 0" - exit 0 -fi -echo "НЕ СОШЛОСЬ: проб $N, разошлось $BAD" -exit 1 diff --git a/flang/scripts/run-verdict-targets-not-named.tsv b/flang/scripts/run-verdict-targets-not-named.tsv index bdf609711..14961591c 100644 --- a/flang/scripts/run-verdict-targets-not-named.tsv +++ b/flang/scripts/run-verdict-targets-not-named.tsv @@ -1,7 +1,5 @@ файл ключ довод flang/test/обход.sh да обходчик гоняет проверки дерева на flang; вердикта они не проходят (замер 18.09: «доказано 224, сетка 42, на веру 83»), без ключа не прогналась бы ни одна -flang/proof/probes/run/run.sh нет это проба САМОГО ключа: ключ подставляется из таблицы ожидания ($kl), и прибитый здесь «--на-веру» уничтожил бы половину проб -flang/proof/probes/unproven/run.sh нет то же: проба ВОРОТ недоказанного, ключ приходит столбцом $klyuchi из expected.tsv (в таблице есть строки и с «--на-веру», и с «--trust», и без ключа). Прибитый в скрипте ключ отменил бы предмет набора — старшинство «ключ команды → FLANG_UNPROVEN → .flangrc» flang/proof/check.sh нет зовёт напечатанную во временный каталог программу сверки; она вердикт проходит — прогон 18.09 код 0 flang/proof/rules-match.sh нет то же: напечатанная программа сверки правил, вердикт проходит (сосед «--только-первая» отвечает код 0) flang/proof/reduce.sh нет то же: малый сводитель, напечатанный во временный каталог diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index d3257a94f..591bbb1c9 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1626,7 +1626,6 @@ aa65f3785b0c62edf336a36297e30b38|1|1|0|0|0|flang/proof/probes/unproven/programs/ 86e0e447b270b761bff6ae33fe3ffd12|1|1|0|1|0|flang/proof/checker/tests/programs/audit-2844/unfold2-itself.flang eb5b390d34c90eb95ad3b4382c2a3a1f|1|0|0|0|1|flang/proof/checker/tests/programs/audit-2844/unfold3-control-honest.flang b1b137536d045c4fdd205ece597d4acf|1|0|1|0|0|flang/proof/probes/orders/programs/arguments.fscript -99f0a0d7135e7b2b5eb7f88096d487bb|4|3|1|0|0|flang/proof/probes/orders/run.fscript a9553eaffc7cba5c190df9e076ef0b9c|2|2|0|0|0|flang/proof/probes/io-timeout/run.fscript 1f4a2a844b39793dc79f661223b3dc08|1|0|1|0|0|docs/examples/io/progress-bar-on-screen.flang 227913e61eb3388807d0420cd8ec4fd3|5|5|0|0|0|flang/proof/probes/syllogism/programs/chain.flang From e87f1fe7bfdf8850c8c9d3bc9c111b7b3f924e1a Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Mon, 28 Sep 2026 01:11:54 +0000 Subject: [PATCH 2/4] fix(ci): call the probe plans from the workflow steps The rebase of the probe runner change kept the old binary.yml, so the guards-selftest job still ran sh flang/proof/probes/strict/run.sh, a file the same change deletes, and failed at once. The probe steps now call the run.fscript plans again, as in the original change. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/binary.yml | 62 ++++++------------------------------ 1 file changed, 9 insertions(+), 53 deletions(-) diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index f8e461d1e..de06c7ee1 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -1762,64 +1762,20 @@ jobs: env: FLANG_BIN: ${{ github.workspace }}/bootstrap/flang - # ── ЧЕТЫРЕ ИСХОДА СТРОГОГО РЕЖИМА (задача 5502, пункт 5 аудита) ─────── - # - # Аудит требует, чтобы успех был невозможен без независимой проверки всех - # обязательств. Прогоном 19 сентября 2026 показано обратное: программа с - # ЛОЖНЫМ постусловием («результат не больше 100» при теле «н плюс н») и - # парой строк `пример` получала код 0 и от `flang check`, и от - # `flang check --proof`, и от независимого сверщика разом — при том что - # `flang run --на-веру` на н = 100 печатал FLANG_PROPERTY и код 1. Ноль - # ПОКУПАЛСЯ примером: тот же файл без `пример` давал 3. - # - # Набор держит ОБЕ половины одной таблицей: строки без «--строго» стерегут - # умолчание (оно правкой не тронуто ни на знак — разъедься оно, сломалось - # бы всё дерево разом), строки с ключом — сами четыре исхода. Слово - # проверяется вместе с кодом: смена причины при том же коде — тоже - # расхождение. - # - # Место здесь, а не в работе `chekker`: та собирает C-сверщик БЕЗ - # компилятора нарочно, а этот набор спрашивает мнение компилятора о нём - # самом. Двоичный уже собран этой работой; лишней сборки нет. Замер: 20 - # проб, около 2 секунд на всё. - name: Check strict mode - run: sh flang/proof/probes/strict/run.sh - env: - FLANG_BIN: ${{ github.workspace }}/bootstrap/flang - FLANG_TMP: ${{ runner.temp }} - - # Ворота недоказанного настраиваются тремя способами — ключом команды, - # переменной среды и .flangrc, — и старшинство между ними названо. Проба - # гоняет все три и каждую пару, иначе «ключ бьёт файл» осталось бы словами. + run: bootstrap/flang io flang/proof/probes/strict/run.fscript --plan Binary - name: Check unproven gate - run: sh flang/proof/probes/unproven/run.sh - - # ПРОБЫ СИЛЛОГИЗМА. Набор лежал с 20 сентября 2026 и НЕ ЗВАЛСЯ НИОТКУДА: - # ни один workflow его не трогал, и 25 сентября, после перепечатки семени, - # все шесть проб разошлись с таблицей молча — таблица ждала от двоичного - # отказа разбора слова `следует`, а он его уже знал. Проверка, которую - # никто не зовёт, ничего не проверяет; поэтому шаг здесь. Замер 26 сентября - # 2026: шесть проб, около двух секунд на всё — той же ценой, что соседи. - - name: Check syllogism probes - run: sh flang/proof/probes/syllogism/run.sh + run: bootstrap/flang io flang/proof/probes/unproven/run.fscript --plan Binary env: - FLANG_BIN: ${{ github.workspace }}/bootstrap/flang FLANG_TMP: ${{ runner.temp }} - - # ПЕРЕПЕЧАТКИ ЖДАЛ И ДОЖДАЛСЯ. Слово «Размер экрана» заведено в словарь - # 22 сентября 2026, и прежний двоичный его не знал — шаг был КРАСЕН по - # названному долгу. Печать прошла 25 сентября 2026 (выпуск 0.7.22); замер - # 26 сентября на дереве `gh/dev` `d5e203b89`: сошлось 6 проб из 6, код 0. + - name: Check syllogism probes + run: bootstrap/flang io flang/proof/probes/syllogism/run.fscript --plan Binary + - name: Check run verdict + run: bootstrap/flang io flang/proof/probes/run/run.fscript --plan Binary + - name: Check environment and argument orders + run: bootstrap/flang io flang/proof/probes/orders/run.fscript --plan Binary - name: Check screen size - run: cd flang/proof/probes/screen-size && ../../../../bootstrap/flang io run.fscript - env: - FLANG_BIN: ${{ github.workspace }}/bootstrap/flang - FLANG_TMP: ${{ runner.temp }} - - name: Check memory limit - run: cd flang/proof/probes/memory-limit && ../../../../bootstrap/flang io run.fscript - env: - FLANG_BIN: ${{ github.workspace }}/bootstrap/flang - FLANG_TMP: ${{ runner.temp }} + run: bootstrap/flang io flang/proof/probes/screen-size/run.fscript --plan Binary - name: Check io timeout answers run: cd flang/proof/probes/io-timeout && ../../../../bootstrap/flang io run.fscript From 89ad6beac86f74d21c674a58c6e5fa5cc97f1c83 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 12:42:12 +0000 Subject: [PATCH 3/4] chore(numbers): sync measured counts after rebase onto dev dcfd766d4 Restore the memory limit probe step dropped while replacing the probe steps, and take the shell counts again on the rebased tree. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ --- .github/workflows/binary.yml | 11 ++++++++--- .github/workflows/ci.yml | 4 ++-- docs/javascript-inventory.md | 4 ++-- docs/tree-inventory.md | 4 ++-- 4 files changed, 14 insertions(+), 9 deletions(-) diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index de06c7ee1..876c57e5d 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -393,9 +393,9 @@ jobs: # # Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md, # docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН - # язык: JavaScript. Оболочка (93 файлов, 23372 строк), HTML, CSS, пробы на - # СНЯТО 2026-09-17 файлов *.sh = 93 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17) - # СНЯТО 2026-09-17 строк-в *.sh = 23372 (задача 1400: девять проб на подлог и две честные под правила Н6 и О9 прибавили 42 строки в flang/proof/checker/tests/run.sh) (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 23372, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 23980, снято 2026-09-22) (ADR-0046: довод в шапках двух сторожей имён — сперва почему flang/proof не судится, потом почему вошёл в область — прибавил 9 строк; до него 23971, снято 2026-09-17) + # язык: JavaScript. Оболочка (89 файлов, 22906 строк), HTML, CSS, пробы на + # СНЯТО 2026-09-17 файлов *.sh = 89 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17) + # СНЯТО 2026-09-17 строк-в *.sh = 22906 (задача 1400: девять проб на подлог и две честные под правила Н6 и О9 прибавили 42 строки в flang/proof/checker/tests/run.sh) (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 23372, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 23980, снято 2026-09-22) (ADR-0046: довод в шапках двух сторожей имён — сперва почему flang/proof не судится, потом почему вошёл в область — прибавил 9 строк; до него 23971, снято 2026-09-17) # C, Python, awk и Erlang не считались нигде и ни в одной проверке. Долг, # которого никто не считает, не убывает: его не видно ни в отчёте, ни в # ленте, и растёт он молча. @@ -1776,6 +1776,11 @@ jobs: run: bootstrap/flang io flang/proof/probes/orders/run.fscript --plan Binary - name: Check screen size run: bootstrap/flang io flang/proof/probes/screen-size/run.fscript --plan Binary + - name: Check memory limit + run: cd flang/proof/probes/memory-limit && ../../../../bootstrap/flang io run.fscript + env: + FLANG_BIN: ${{ github.workspace }}/bootstrap/flang + FLANG_TMP: ${{ runner.temp }} - name: Check io timeout answers run: cd flang/proof/probes/io-timeout && ../../../../bootstrap/flang io run.fscript diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1d57197b5..acdf211c8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -206,8 +206,8 @@ jobs: # 31 августа 2026 в дереве нашлось 31 место в 14 файлах, где записанное рукой # число разошлось с тем, что лежит рядом: `docs/tree-inventory.md` считала # `seed-parses-sources-guard.sh` в 83 строки при 195, оболочку — в 66 файлов - # при 71 тогдашних — сегодня их 93; - # СНЯТО 2026-09-17 файлов *.sh = 93 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22; + # при 71 тогдашних — сегодня их 89; + # СНЯТО 2026-09-17 файлов *.sh = 89 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22; # `flang/PLAN.md` — пять вариантов «Поручение» при 22. Каждое из этих чисел # было ВЕРНО В ДЕНЬ ЗАПИСИ и солгало назавтра, и сторожа не было ни на одном. # diff --git a/docs/javascript-inventory.md b/docs/javascript-inventory.md index 8b0c9638d..8a90909e7 100644 --- a/docs/javascript-inventory.md +++ b/docs/javascript-inventory.md @@ -67,8 +67,8 @@ JavaScript стало 55, строк 29 733; в трёх каталогах о Эта опись считает ОДИН язык. Остальные шестнадцать — оболочка, C, C++, Python, HTML, CSS, awk, Erlang, Java, C#, Elixir, Go, Rust, Lua, vimscript, Ruby — -считает [`tree-inventory.md`](tree-inventory.md) (26 сентября 2026: 246 файлов вне flang, - +считает [`tree-inventory.md`](tree-inventory.md) (26 сентября 2026: 242 файлов вне flang, + долг вне JavaScript — **97 файлов, 18 427 строк при потолке 63**: храповик красен, разбор — задачи 4838 и 7405). Там же названы 569 строк JavaScript, лежащих ВНУТРИ файлов `.html`: счёт по именам файлов их не видит, и diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index af0d275c7..960c50586 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -1,5 +1,5 @@ -# Опись дерева по языкам: 246 файлов вне flang, долг вне JavaScript — 98 при потолке 63 - +# Опись дерева по языкам: 242 файлов вне flang, долг вне JavaScript — 93 при потолке 63 + ⚠ **ХРАПОВИК ДОЛГА КРАСЕН, и заголовок это теперь говорит.** Прогон `./ярлык опись:языки` **5 сентября 2026** отвечает кодом 1: «ДОЛГ ВНЕ From feff3b7501281bb88583fdf0ac07cd9d0675461b Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Tue, 29 Sep 2026 13:30:54 +0000 Subject: [PATCH 4/4] chore(numbers): sync measured counts after rebase Co-Authored-By: Claude Opus 5.5 --- docs/tree-inventory.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 960c50586..72ee6729d 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -78,7 +78,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| -| оболочка | 99 | 23 883 | 87 | 15 149 | +| оболочка | 95 | 23 417 | 83 | 14 683 | | C | 36 | 868 191 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 16 | 6 031 | 10 | 2 880 |