diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index f8e461d1e..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 не считались нигде и ни в одной проверке. Долг, # которого никто не считает, не убывает: его не видно ни в отчёте, ни в # ленте, и растёт он молча. @@ -1762,59 +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 }} + 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: 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/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/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/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/tree-inventory.md b/docs/tree-inventory.md index af0d275c7..72ee6729d 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: «ДОЛГ ВНЕ @@ -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 | 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