diff --git a/.flangrc b/.flangrc index 5f8476fef..c09a34f97 100644 --- a/.flangrc +++ b/.flangrc @@ -59,7 +59,7 @@ script.record-source:check = bootstrap/flang io scripts/guards/record-follows-it script.record-source:forgery = bootstrap/flang io scripts/guards/record-follows-its-source.fscript --plan Подлог script.checker:check = bootstrap/flang io flang/proof/checker/tests/run.fscript --max-steps 4000000000 --timeout 600000 script.plan-rules:probe = bootstrap/flang io flang/proof/probes/plan-rules-asked/run.fscript --plan Binary -script.translation:check = sh flang/translation/run.sh +script.translation:check = bootstrap/flang io flang/translation/run.fscript --plan Проверка script.proved-share:check = bootstrap/flang io flang/proof/share-measure.fscript --max-steps 4000000000 --timeout 900000 -- --set corpus script.proved-share:forgery = bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000 script.kernel-verdict:check = bootstrap/flang io flang/proof/kernel-verdict.fscript --max-steps 4000000000 --timeout 900000 diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index f6e01abfa..7ad1f576e 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -394,9 +394,9 @@ jobs: # # Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md, # docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН - # язык: JavaScript. Оболочка (50 файлов, 9558 строк), HTML, CSS, пробы на - # СНЯТО 2026-10-04 файлов *.sh = 50 (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 52, снято 2026-10-04) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17) - # СНЯТО 2026-10-04 строк-в *.sh = 9558 (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 9756, снято 2026-10-04) (задачи 1426 и 8567: поиск коммита отпечатка по содержимому прибавил 135 строк в scripts/bootstrap-reprint.sh, а отменённая хронология предела шагов убрала 141; до них 9762, снято 2026-09-17) (задача 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. Оболочка (49 файлов, 9344 строк), HTML, CSS, пробы на + # СНЯТО 2026-10-04 файлов *.sh = 49 (перенос flang/translation/run.sh на план flang/translation/run.fscript снял один файл оболочки; до него 50, снято 2026-10-04) (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 52, снято 2026-10-04) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17) + # СНЯТО 2026-10-04 строк-в *.sh = 9344 (перенос flang/translation/run.sh на план flang/translation/run.fscript снял 214 строк оболочки; до него 9558, снято 2026-10-04) (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 9756, снято 2026-10-04) (задачи 1426 и 8567: поиск коммита отпечатка по содержимому прибавил 135 строк в scripts/bootstrap-reprint.sh, а отменённая хронология предела шагов убрала 141; до них 9762, снято 2026-09-17) (задача 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 не считались нигде и ни в одной проверке. Долг, # которого никто не считает, не убывает: его не видно ни в отчёте, ни в # ленте, и растёт он молча. @@ -407,9 +407,9 @@ jobs: # оболочке или на Python останавливает работу в тот же день. # # Замер на этом дереве: 17,7 с и 471 МБ, двоичному хватает `git` и `wc`. - # Предел шагов поднят с умолчания (10 млн): опись обходит 193 файлов и + # Предел шагов поднят с умолчания (10 млн): опись обходит 192 файлов и # семнадцать языков, и в умолчание не укладывается. - # СНЯТО 2026-10-04 файлов *.sh,*.c,*.h,*.py,*.html,*.css,*.awk,*.erl,*.js,*.mjs,*.java,*.cs,*.ex,*.exs,*.go,*.rs,*.lua,*.vim,*.rb,*.cpp,*.cc,*.hpp,*.hh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 193 (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 196, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 194, снято 2026-09-17) (задача 5821: семь проверок scripts/** стали планами; до них 251, снято 2026-09-27) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-17) + # СНЯТО 2026-10-04 файлов *.sh,*.c,*.h,*.py,*.html,*.css,*.awk,*.erl,*.js,*.mjs,*.java,*.cs,*.ex,*.exs,*.go,*.rs,*.lua,*.vim,*.rb,*.cpp,*.cc,*.hpp,*.hh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 192 (перенос flang/translation/run.sh на план flang/translation/run.fscript снял один файл вне flang; до него 193, снято 2026-10-04) (задачи 0049 и 5821: сняты flang/scripts/word-occupancy.mjs, scripts/seed/seed-freshness.sh и scripts/guards/version-derivations-guard.sh — у каждого двойник на flang доказан прогоном; до них 196, снято 2026-10-04) (две честные пары сличителя перевода: отбор по признаку и объявленная мера; до них 194, снято 2026-09-17) (задача 5821: семь проверок scripts/** стали планами; до них 251, снято 2026-09-27) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-17) # # СКОЛЬКО ИЗ ЭТИХ ПЯТИДЕСЯТИ МИЛЛИОНОВ УХОДИТ, замер 29 августа 2026. # Меряно перебором самого предела: при 10 500 000 опись умирает @@ -1480,11 +1480,16 @@ jobs: # 6ebd5e18e, но ни один workflow его не звал, и два сторожа — «кто зовёт # сторожей» и сторож проб порчи — держали на нём хук перед пушем красным. # + # С 4 октября 2026 набор гоняет ПЛАН `flang/translation/run.fscript` (прежняя + # оболочка `run.sh` снята): приговор доказан ядром, ожидания 32 опытов стоят + # таблицей. Жалоба идёт строкой « · <имя опыта> — ждали код N …», и проба + # порчи ниже ищет в выводе ИМЕННО эту строку. + # # Работа соседняя чекеру и отдельная по той же причине: компилятор не - # собирается и не зовётся, нужны только `cc` и `sh`. Сличитель, который - # спрашивает ответ у того же двоичного, о котором судит, не стоит ничего. - # Замер 14 сентября 2026 на рабочей машине: весь прогон — сборка сличителя - # и шестнадцать опытов — 1,2 с. + # собирается, нужны только `cc` и `sh`. Но план зовётся собранным двоичным, + # поэтому шаг сборки семени здесь ЕСТЬ, а сличитель по-прежнему не спрашивает + # ответ у того двоичного, о котором судит. Замер 4 октября 2026 на рабочей + # машине: весь прогон — сборка сличителя и тридцать два опыта — 4,3 с. # # Порча внешняя, одна строка напечатанного C «Светофора»: штраф красного # 500 → 501 при прежнем протоколе. Прогон обязан покраснеть ИМЕННО на этой @@ -1494,11 +1499,37 @@ jobs: perevod: name: translation-matcher runs-on: ubuntu-latest - timeout-minutes: 10 + # Было 10, пока набор гоняла оболочка: `cc` и шестнадцать опытов. План + # зовётся двоичным, и при промахе кеша работа сперва СОБИРАЕТ семя; на + # раннере это минуты, а не 4,3 с здешнего прогона. 20 — запас к соседней + # работе `guards-selftest`, которая собирает то же и просит столько же. + timeout-minutes: 20 steps: - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0 - name: Check verdict cache uses: ./.github/actions/release-without-cache + # Двоичный берётся готовым по тем же правилам, что у соседних работ: + # ключ кеша — хеш всех входов сборки плюс флаги; негодный кеш собирается + # заново, а не принимается молча. + - name: Restore binary cache + id: kesh-dvoichnogo + uses: actions/cache@v4 + with: + path: | + bootstrap/flang + bootstrap/libcompiler_flang.a + key: flang-bootstrap-${{ runner.os }}-${{ hashFiles('bootstrap/*.c', 'bootstrap/*.h', 'bootstrap/Makefile') }}-${{ env.FLANG_CFLAGS }} + - name: Build bootstrap + if: steps.kesh-dvoichnogo.outputs.cache-hit != 'true' + run: make -C bootstrap -j"$(nproc)" CFLAGS="$FLANG_CFLAGS" + - name: Verify cached binary + if: steps.kesh-dvoichnogo.outputs.cache-hit == 'true' + run: | + set -u + if ! ./bootstrap/flang --version >/dev/null 2>&1; then + echo "::warning::двоичный из кеша не запускается — собираю заново" + make -C bootstrap -j"$(nproc)" CFLAGS="$FLANG_CFLAGS" + fi - name: Probe translation matcher run: | set -u @@ -1510,7 +1541,7 @@ jobs: echo "ПОДЛОГ НЕ СОБРАЛСЯ: строки «fl_t1 = fl_number(500.0);» в $podlog уже нет — поправить подлог, сличитель ни при чём" >&2 exit 1 fi - if sh flang/translation/run.sh > "$RUNNER_TEMP/perevod.out" 2>&1; then + if bootstrap/flang run-script translation:check > "$RUNNER_TEMP/perevod.out" 2>&1; then git checkout -- "$podlog" cat "$RUNNER_TEMP/perevod.out" echo "сличитель промолчал на подлоге — проверять им нечего" >&2 @@ -1518,12 +1549,12 @@ jobs: fi git checkout -- "$podlog" cat "$RUNNER_TEMP/perevod.out" - if ! grep -qF 'КРАСЕН честная пара с разбором' "$RUNNER_TEMP/perevod.out"; then + if ! grep -qF '· честная пара с разбором' "$RUNNER_TEMP/perevod.out"; then echo "прогон покраснел, но не на испорченной паре — краснота не по делу" >&2 exit 1 fi - name: Check C translation - run: sh flang/translation/run.sh + run: bootstrap/flang run-script translation:check storozha: name: guards-selftest diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 28b0ba9f5..7a717984d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -212,8 +212,8 @@ jobs: # 31 августа 2026 в дереве нашлось 31 место в 14 файлах, где записанное рукой # число разошлось с тем, что лежит рядом: `docs/tree-inventory.md` считала # `seed-parses-sources-guard.sh` в 83 строки при 195, оболочку — в 66 файлов - # при 71 тогдашних — сегодня их 50; - # СНЯТО 2026-10-04 файлов *.sh = 50 (задача 5821: scripts/guards/version-derivations-guard.sh снят — сверка производных версии стала планом scripts/guards/version-derivations-guard.fscript, приговор доказан ядром (13 из 13), хук зовёт план; до него 51, снято 2026-10-04) (задача 0049: scripts/seed/seed-freshness.sh снят — проверка давно живёт планом scripts/seed/seed-freshness.fscript, а переходник ещё и терял довод (exec без "$@"); до него 52, снято 2026-10-04) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22; + # при 71 тогдашних — сегодня их 49; + # СНЯТО 2026-10-04 файлов *.sh = 49 (перенос flang/translation/run.sh на план flang/translation/run.fscript снял один файл оболочки; до него 50, снято 2026-10-04) (задача 5821: scripts/guards/version-derivations-guard.sh снят — сверка производных версии стала планом scripts/guards/version-derivations-guard.fscript, приговор доказан ядром (13 из 13), хук зовёт план; до него 51, снято 2026-10-04) (задача 0049: scripts/seed/seed-freshness.sh снят — проверка давно живёт планом scripts/seed/seed-freshness.fscript, а переходник ещё и терял довод (exec без "$@"); до него 52, снято 2026-10-04) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22; # `flang/PLAN.md` — пять вариантов «Поручение» при 22. Каждое из этих чисел # было ВЕРНО В ДЕНЬ ЗАПИСИ и солгало назавтра, и сторожа не было ни на одном. # diff --git a/docs/four-coverages.md b/docs/four-coverages.md index f06b34448..b136b1428 100644 --- a/docs/four-coverages.md +++ b/docs/four-coverages.md @@ -104,7 +104,7 @@ Lean: это счёт текста, а не доказательство. (ADR-0030). Генератор кода ведёт протокол перевода, а отдельная программа на C (`flang/translation/matcher.c`) переигрывает протокол против исходника и напечатанного кода. Меряется двумя числами: сколько опытов в -[`flang/translation/run.sh`](../flang/translation/run.sh) (честные пары обязаны сойтись, +[`flang/translation/run.fscript`](../flang/translation/run.fscript) (честные пары обязаны сойтись, подделки — не приняться) и сколько правил печати из закрытого списка [`flang/translation/PRINT-RULES.tsv`](../flang/translation/PRINT-RULES.tsv) сверяются с ТЕКСТОМ ИСХОДНИКА, а не только с протоколом. diff --git a/docs/javascript-inventory.md b/docs/javascript-inventory.md index 85c4567c1..c605cb21c 100644 --- a/docs/javascript-inventory.md +++ b/docs/javascript-inventory.md @@ -68,8 +68,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) (4 октября 2026: 193 файлов вне flang, - +считает [`tree-inventory.md`](tree-inventory.md) (4 октября 2026: 192 файлов вне flang, + долг вне JavaScript — **97 файлов, 18 427 строк при потолке 63**: храповик красен, разбор — задачи 4838 и 7405). Там же названы 569 строк JavaScript, лежащих ВНУТРИ файлов `.html`: счёт по именам файлов их не видит, и diff --git a/docs/tree-inventory.md b/docs/tree-inventory.md index 78057c001..720b0986f 100644 --- a/docs/tree-inventory.md +++ b/docs/tree-inventory.md @@ -1,5 +1,5 @@ -# Опись дерева по языкам: 193 файлов вне flang, долг вне JavaScript — 93 при потолке 63 - +# Опись дерева по языкам: 192 файлов вне flang, долг вне JavaScript — 93 при потолке 63 + ⚠ **ХРАПОВИК ДОЛГА КРАСЕН, и заголовок это теперь говорит.** Прогон `bootstrap/flang run-script inventory:languages` **5 сентября 2026** отвечает кодом 1: «ДОЛГ ВНЕ @@ -76,7 +76,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000 | язык | файлов | строк | долг файлов | долг строк | |---|---:|---:|---:|---:| -| оболочка | 56 | 9 875 | 50 | 5 431 | +| оболочка | 55 | 9661 | 50 | 5 431 | | C | 39 | 882 835 | 0 | 0 | | C++ | 1 | 404 | 0 | 0 | | Python | 5 | 2 906 | 0 | 0 | diff --git a/flang/translation/run.fscript b/flang/translation/run.fscript new file mode 100644 index 000000000..35ca056b7 --- /dev/null +++ b/flang/translation/run.fscript @@ -0,0 +1,818 @@ +модуль «Сличитель перевода» + использует «Inquiry» из "../../scripts/inquiry.fscript" + использует «Lists» только «Соединить списки» + +примечание "СЛИЧИТЕЛЬ ПЕРЕВОДА: ЧЕСТНЫЕ ПАРЫ СХОДЯТСЯ, ПОДДЕЛКИ НЕ ПРИНИМАЮТСЯ." +примечание "ADR-0030 «Печатник доказывает КАЖДЫЙ СВОЙ ЗАПУСК», задачи 1401, 7098." +примечание "Зовут одним ярлыком:" +примечание " bootstrap/flang run-script translation:check код 1, если опыт разошёлся с ожиданием" + +примечание "ЧТО ЗДЕСЬ ПРОИСХОДИТ. Печатник C ведёт протокол перевода. Отдельная программа на C" +примечание "(flang/translation/matcher.c) переигрывает протокол против исходника и напечатанного" +примечание "кода. Честные пары лежат в fixtures/ — напечатанный C и протокол примеров" +примечание "flang/proof/examples/, снятые печатником flang/self/emit-c.flang. Подделки строятся" +примечание "здесь же из честных пар, каждая одной правкой, названной словами." + +примечание "КОДЫ СЛИЧИТЕЛЯ: 0 — СОШЛОСЬ; 3 — НЕ ПРОВЕРЕНО (правило не переигрывается); 1 — НЕ" +примечание "СОШЛОСЬ. Опыт ждёт один из трёх и одно слово в ответе; разошлось — план сдаётся" +примечание "кодом 1 и называет каждый разошедшийся опыт поимённо." + +примечание "ЧЕМ ЭТОТ ФАЙЛ ОТЛИЧАЕТСЯ ОТ ПРЕЖНЕГО НА ОБОЛОЧКЕ. До 4 октября 2026 то же гонял" +примечание "flang/translation/run.sh, 214 строк. Перенос дал две вещи, которых у оболочки быть" +примечание "не могло. ПЕРВОЕ: приговор здесь ДОКАЗАН ядром — 16 обязательств, план идёт БЕЗ" +примечание "ключа --на-веру, — а разбор ответа, сверка закрытого списка и сборка опыта из частей" +примечание "проверяются ПРИМЕРАМИ на месте. ВТОРОЕ: ожидания опытов стоят таблицей — «что»," +примечание "«код», «слово», «дело», — и число опытов в каждой стопке закреплено обязательством." +примечание "Оболочка осталась ровно там, где она прибор, а не судья: сборка сличителя, правка" +примечание "честной пары в подделку и запуск сличителя." + +примечание "ЧТО СЛИЧЕНО С ПРЕЖНЕЙ ОБОЛОЧКОЙ, И ЧЕМ. Тройки «что, код, слово» сняты прибором у" +примечание "обоих — у run.sh разбором вызовов opyt, здесь прогоном функции «Опыты» — и совпали" +примечание "все 32 знак в знак. Прогон обоих на одном дереве 4 октября: опытов 32, ни одного" +примечание "расхождения, код 0 у обоих. Отрицательный контроль, три подлога: число в напечатанном" +примечание "C «Светофора» (500 → 501), правило «свёртка» вынуто из PRINT-RULES.tsv, число в" +примечание "напечатанном C объявленной меры (1.0 → 2.0). На каждом оба краснеют кодом 1 и называют" +примечание "ОДНО И ТО ЖЕ место." + +примечание "ДВА ОТЛИЧИЯ, НАЗВАННЫЕ НАРОЧНО. ПЕРВОЕ: разошедшийся закрытый список у оболочки" +примечание "обрывал прогон до первого опыта, здесь он становится бедой номер один, а опыты всё" +примечание "равно прогоняются — сведений больше, код тот же 1. ВТОРОЕ: несобравшаяся подделка" +примечание "(«ПОДДЕЛКА НЕ ПОСТРОЕНА», код 9 от оболочки) у run.sh обрывала весь прогон, здесь она" +примечание "краснит СВОЙ опыт и названа поимённо, а остальные опыты досчитываются." + +примечание "ДЕВЯТЬ ОПЫТОВ ДОБАВЛЕНЫ ЭТИМ ПЕРЕНОСОМ — пять на правило «отфильтровать» и четыре на" +примечание "поблажку сторожу меры (PR 298). Они написаны и прогнаны автором сличителя, но в его" +примечание "ветку не вписаны: run.sh был не его. На прежнем сличителе 5 из 9 краснели." + +примечание "ЧЕГО ЗДЕСЬ НЕТ. Печатник не доказан: сличитель переигрывает ПРОТОКОЛ КАЖДОГО ЗАПУСКА," +примечание "а не печатника (ADR-0030 §1). Девять правил из 33 и 8 блоков протокола сличаются" +примечание "только текстом — какие именно, называет сам сличитель кодом 3." + +объект «Опыт» + «что»: строка + «код»: число + «слово»: строка + «дело»: строка + +тотальная функция «Сложить опыт» + принимает что: строка, код: число, слово: строка, дело: строка + возвращает «Опыт» + пример «опыт несёт имя, ожидаемый код, обязательное слово и дело оболочки» + дано что равно "пара" + дано код равно 0 + дано слово равно "СОШЛОСЬ" + дано дело равно "look" + ожидается запись «Опыт» с «что» равным "пара" и «код» равным 0 и «слово» равным "СОШЛОСЬ" и «дело» равным "look" + запись «Опыт» с «что» равным что и «код» равным код и «слово» равным слово и «дело» равным дело +тотальная функция «Пути» + возвращает список строки + обеспечивает «путей двадцать три» (длина результат) равен 23 + [ + "set -u", + "M=$W/matcher", + "T=flang/translation", + "E=flang/proof/examples", + "F=$T/fixtures/forgery-if-without-descent", + "SRC=$E/forgery-if-without-descent.flang", + "CEE=$F/poddelka_usloviya_bez_spuska.c", + "PRO=$F/poddelka_usloviya_bez_spuska.protocol", + "NAMED=$F/podmena_imeni_vremennoy", + "SWAP=$F/perestavlennye_operandy", + "LSRC=$E/traffic-light.flang", + "LCEE=$T/fixtures/traffic-light/svetofor.c", + "LPRO=$T/fixtures/traffic-light/svetofor.protocol", + "VSRC=$T/fixtures/all-elements/all-elements.flang", + "VCEE=$T/fixtures/all-elements/all_elements_at_the_boundary.c", + "VPRO=$T/fixtures/all-elements/all_elements_at_the_boundary.protocol", + "FSRC=$T/fixtures/filter/filter.flang", + "FCEE=$T/fixtures/filter/filter_at_the_boundary.c", + "FPRO=$T/fixtures/filter/filter_at_the_boundary.protocol", + "MBASE=$T/fixtures/declared-measure/declared_measure_at_the_boundary", + "MSRC=$T/fixtures/declared-measure/declared-measure.flang", + "MCEE=$MBASE.c", + "MPRO=$MBASE.protocol" + ] + +тотальная функция «Правки» + возвращает список строки + обеспечивает «правок восемь» (длина результат) равен 8 + [ + "fail() { echo \"ПОДДЕЛКА НЕ ПОСТРОЕНА: $*\" >&2; exit 9; }", + "rotten() { echo \"ПОДДЕЛКА ПРОГНИЛА: $*\" >&2; exit 9; }", + "line_is() { sed -n \"$2p\" \"$1\" | grep -qF -- \"$3\" || fail \"в $(basename \"$1\") строка $2 не «$3»\"; }", + "cut_lines() { line_is \"$1\" \"$2\" \"$4\"; sed \"$2,$3d\" \"$1\"; }", + "same_as() { cmp -s \"$1\" \"$2\" || rotten \"$(basename \"$2\") в дереве не равна построенной здесь\"; }", + "look() { \"$M\" \"$1\" \"$2\" \"$3\"; }", + соединить [ + "once() { n=$(grep -cF -- \"$2\" \"$1\"); [ \"$n\" = 1 ] || fail \"«$2» в $(basename \"$1\") встречается $n р", + "аз\"; }" + ] по "", + соединить [ + "swap() { once \"$1\" \"$2\"; awk -v old=\"$2\" -v new=\"$3\" '{ i = index($0, old); if (i) $0 = substr($0, 1", + ", i - 1) new substr($0, i + length(old)); print }' \"$1\"; }" + ] по "" + ] + +тотальная функция «Образцы» + возвращает список строки + обеспечивает «образцов сорок шесть» (длина результат) равен 46 + [ + "CALL='poddelka_usloviya_bez_spuska_stoit_na_meste(ctx, n, &fl_t3'", + "OTHER='poddelka_usloviya_bez_spuska_cherez_odno(ctx, n, &fl_t3'", + "WAS='fl_t2 = fl_t3;'", + "NOW='fl_t2 = fl_t1;'", + "ARG9='узел var строка 9 столбец 31'", + "BRANCH='часть иначе строк 1'", + "BRACE='} else {'", + "PAIR='kruzhit_po_pare(ctx, m, n, &fl_t8'", + "BACK='kruzhit_po_pare(ctx, n, m, &fl_t8'", + "ALONE='kruzhit_po_pare(ctx, n, &fl_t8'", + "RULE='столбец 11 правило «вызов» имя «Стоит на месте»'", + "GUESS='столбец 11 правило «вызов-наугад» имя «Стоит на месте»'", + "SHIFT='столбец 12 правило «вызов» имя «Стоит на месте»'", + "DEEP='функция «Дно зовёт себя»'", + "BODY='/* Тело «Дно зовёт себя»'", + "STRAY='/* строка, которой не печатал ни один узел */'", + "ARG17='узел var строка 17 столбец 31'", + "ENTRY='граница входа'", + "LEAVE='граница выхода'", + "RENAME='s/fl_t3\\([^0-9A-Za-z_]\\)/fl_t2\\1/g; s/fl_t3$/fl_t2/'", + "BARE='узел var строка 7 столбец 8 правило «число-распакованное»'", + "LIT='узел literal строка 7 столбец 20 правило «число-литерал»'", + "DIRECT='fl_flag(n.as.number <= 0.0)'", + "TURNED='fl_flag(0.0 <= n.as.number)'", + "STOP='fl_t3 && fl_t4 < fl_t2'", + "NOSTOP='fl_t4 < fl_t2'", + "YES='bool fl_t3 = true; /* для всех «п» */'", + "NO='bool fl_t3 = false; /* для всех «п» */'", + "QUANT='значение fl_flag(fl_t3)'", + "PLAIN='значение fl_flag(true)'", + "POST='fl_post(ctx, fl_flag(fl_t3),'", + "POSTYES='fl_post(ctx, fl_flag(true),'", + "EVERY='правило «все-элементы» элемент «п»'", + "FOLD='правило «свёртка» элемент «п»'", + "PUT='fl_t2[fl_t3] = el;'", + "MISPUT='fl_t2[fl_t4] = el;'", + "LOOP='for (size_t fl_t4 = 0; fl_t4 < fl_t1.as.list.count; fl_t4 += 1) {'", + "FIRST='for (size_t fl_t4 = 0; fl_t3 < 1 && fl_t4 < fl_t1.as.list.count; fl_t4 += 1) {'", + "LEN='значение fl_list(fl_t2, fl_t3)'", + "WHOLE='значение fl_list(fl_t2, fl_t1.as.list.count)'", + "KEEP='правило «отфильтровать» элемент «эл»'", + "MAP='правило «отобразить» элемент «эл»'", + "MUTE='s/объявленная мера убывает/объявленная мера молчит/g'", + "WATCH='узел call строка 17 столбец 11 правило «вызов» имя «объявленная мера убывает»'", + "MOVED='узел call строка 17 столбец 20 правило «вызов» имя «объявленная мера убывает»'", + соединить [ + "ADD='/^диспетчер$/ && !extra { print \"функция «мера убывает» идентификатор declared_measure_at_the_boundary", + "_mera_ubyvaet оболочка простая\"; print \"конец узла\"; extra = 1 } { print }'" + ] по "" + ] + +тотальная функция «Строки сборки» + возвращает список строки + обеспечивает «строк сборки четыре» (длина результат) равен 4 + [ + "set -u", + "R=$(mktemp -d \"${TMPDIR:-/tmp}/translation.XXXXXX\") || exit 1", + соединить [ + "cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -o \"$R/matcher\" flang/translation/matcher.c || { rm -rf \"", + "$R\"; exit 1; }" + ] по "", + "echo \"$R\"" + ] + +тотальная функция «Команда правил описи» + возвращает строка + обеспечивает «список берётся из PRINT-RULES.tsv» результат содержит "PRINT-RULES.tsv" + "awk -F'\\t' '!/^#/ && $1 != \"имя\" && NF { print $1 }' flang/translation/PRINT-RULES.tsv" + +тотальная функция «Команда правил сличителя» + возвращает строка + обеспечивает «список берётся из RULES[] в matcher.c» результат содержит "RULES" + соединить [ + "sed -n '/^static const char \\*const RULES\\[\\] = {$/,/^};$/p' flang/translation/matcher.c | sed -n 's/^ ", + "\"\\(.*\\)\",$/\\1/p'" + ] по "" + +тотальная функция «Опыты условия» + возвращает список список строки + обеспечивает «опытов условия восемнадцать» (длина результат) равен 18 + [ + [ + "честная пара: четыре функции, все правила переиграны", + "0", + "СОШЛОСЬ", + "look \"$SRC\" \"$CEE\" \"$PRO\"" + ], + [ + "честная пара с разбором: сошлось, непереигранное названо", + "3", + "правило «случай» не переиграно", + "look \"$LSRC\" \"$LCEE\" \"$LPRO\"" + ], + [ + "подменённый фрагмент протокола: вызов другой функции", + "1", + "напечатанный C, строка 22", + "swap \"$PRO\" \"$CALL\" \"$OTHER\" > \"$W/1.protocol\" && look \"$SRC\" \"$CEE\" \"$W/1.protocol\"" + ], + [ + "изменённая строка C при прежнем протоколе", + "1", + "напечатанный C, строка", + "swap \"$CEE\" \"$WAS\" \"$NOW\" > \"$W/2.c\" && look \"$SRC\" \"$W/2.c\" \"$PRO\"" + ], + [ + "пропущенный узел: довод вызова выпал из протокола", + "1", + "исходник строка 9 столбец 11", + "cut_lines \"$PRO\" 49 51 \"$ARG9\" > \"$W/3.protocol\" && look \"$SRC\" \"$CEE\" \"$W/3.protocol\"" + ], + [ + "протокол от другого исходника", + "1", + "протокол от другого исходника", + "look \"$LSRC\" \"$CEE\" \"$PRO\"" + ], + [ + "подменённая функция в напечатанном коде (C и протокол заодно)", + "1", + "по правилу ждали", + "swap \"$PRO\" \"$CALL\" \"$OTHER\" > \"$W/6.protocol\" && swap \"$CEE\" \"$CALL\" \"$OTHER\" > \"$W/", + "6.c\" && look \"$SRC\" \"$W/6.c\" \"$W/6.protocol\"" + ], + [ + "потерянная ветвь «иначе» (C и протокол заодно)", + "1", + "не три ветви", + "cut_lines \"$PRO\" 45 59 \"$BRANCH\" > \"$W/7.protocol\" && cut_lines \"$CEE\" 20 23 \"$BRACE\" > \"", + "$W/7.c\" && look \"$SRC\" \"$W/7.c\" \"$W/7.protocol\"" + ], + [ + "переставленные доводы (C и протокол заодно)", + "1", + "исходник строка 17 столбец 11", + "swap \"$PRO\" \"$PAIR\" \"$BACK\" > \"$W/8.protocol\" && swap \"$CEE\" \"$PAIR\" \"$BACK\" > \"$W/8.", + "c\" && look \"$SRC\" \"$W/8.c\" \"$W/8.protocol\"" + ], + [ + "правило не из закрытого списка", + "1", + "не из закрытого списка", + "swap \"$PRO\" \"$RULE\" \"$GUESS\" > \"$W/9.protocol\" && look \"$SRC\" \"$CEE\" \"$W/9.protocol\"" + ], + [ + "место узла сдвинуто на знак", + "1", + "на этом месте исходника", + "swap \"$PRO\" \"$RULE\" \"$SHIFT\" > \"$W/10.protocol\" && look \"$SRC\" \"$CEE\" \"$W/10.protocol\"" + ], + [ + "функция замолчана (C и протокол заодно)", + "1", + "протокол о ней молчит", + "cut_lines \"$PRO\" 360 472 \"$DEEP\" > \"$W/11.protocol\" && cut_lines \"$CEE\" 146 189 \"$BODY\" > ", + "\"$W/11.c\" && look \"$SRC\" \"$W/11.c\" \"$W/11.protocol\"" + ], + [ + "оборванный протокол", + "1", + "оборван", + "sed '$d' \"$PRO\" > \"$W/12.protocol\" && look \"$SRC\" \"$CEE\" \"$W/12.protocol\"" + ], + [ + "лишняя строка в конце C", + "1", + "не напечатал ни один узел", + "{ cat \"$CEE\"; echo \"$STRAY\"; } > \"$W/13.c\" && look \"$SRC\" \"$W/13.c\" \"$PRO\"" + ], + [ + "довод выпал (C и протокол заодно)", + "1", + "доводов у вызова 1, а функция в исходнике принимает 2", + "cut_lines \"$PRO\" 162 164 \"$ARG17\" > \"$W/14a.protocol\" && swap \"$W/14a.protocol\" \"$PAIR\" \"", + "$ALONE\" > \"$W/14.protocol\" && swap \"$CEE\" \"$PAIR\" \"$ALONE\" > \"$W/14.c\" && look \"$SRC\" ", + "\"$W/14.c\" \"$W/14.protocol\"" + ], + [ + "подложный блок протокола", + "1", + "блок не из закрытого списка", + "swap \"$PRO\" \"$ENTRY\" \"$LEAVE\" > \"$W/15.protocol\" && look \"$SRC\" \"$CEE\" \"$W/15.protocol", + "\"" + ], + [ + "переименованная временная: внутренняя накрыла внешнюю (C и протокол заодно)", + "1", + "накрывает живое имя", + "for ext in c protocol; do sed \"$RENAME\" \"$F/poddelka_usloviya_bez_spuska.$ext\" > \"$W/name.$ext", + "\" || exit 9; same_as \"$W/name.$ext\" \"$NAMED.$ext\"; done && look \"$SRC\" \"$NAMED.c\" \"$NAMED.", + "protocol\"" + ], + [ + "переставленные операнды сравнения (дети протокола подогнаны)", + "1", + "не в порядке мест исходника", + "line_is \"$PRO\" 10 \"$BARE\" && line_is \"$PRO\" 16 \"$LIT\" && line_is \"$PRO\" 21 \"значение $DIR", + "ECT\" && line_is \"$PRO\" 25 \"$DIRECT\" && line_is \"$CEE\" 16 \"$DIRECT\" && { sed -n '1,9p' \"$PR", + "O\"; sed -n '16,18p' \"$PRO\"; sed -n '10,15p' \"$PRO\"; sed -n '19,$p' \"$PRO\"; } | sed \"21s/$DIR", + "ECT/$TURNED/; 25s/$DIRECT/$TURNED/\" > \"$W/oper.protocol\" && sed \"16s/$DIRECT/$TURNED/\" \"$CEE\"", + " > \"$W/oper.c\" && same_as \"$W/oper.protocol\" \"$SWAP.protocol\" && same_as \"$W/oper.c\" \"$SWAP", + ".c\" && look \"$SRC\" \"$SWAP.c\" \"$SWAP.protocol\"" + ] + ] + +тотальная функция «Опыты квантора» + возвращает список список строки + обеспечивает «опытов квантора пять» (длина результат) равен 5 + [ + [ + "честная пара с квантором по элементам: все узлы переиграны", + "0", + "СОШЛОСЬ", + "look \"$VSRC\" \"$VCEE\" \"$VPRO\"" + ], + [ + "квантор без остановки на первом «нет» (C и протокол заодно)", + "1", + "по правилу ждали", + "swap \"$VPRO\" \"$STOP\" \"$NOSTOP\" > \"$W/16.protocol\" && swap \"$VCEE\" \"$STOP\" \"$NOSTOP\" > ", + "\"$W/16.c\" && look \"$VSRC\" \"$W/16.c\" \"$W/16.protocol\"" + ], + [ + "квантор начат с «нет»: на пустом списке ложь (C и протокол заодно)", + "1", + "по правилу ждали", + "swap \"$VPRO\" \"$YES\" \"$NO\" > \"$W/17.protocol\" && swap \"$VCEE\" \"$YES\" \"$NO\" > \"$W/17.c", + "\" && look \"$VSRC\" \"$W/17.c\" \"$W/17.protocol\"" + ], + [ + "сторож обещания сверяет «да» вместо квантора (C и протокол заодно)", + "1", + "значение «для всех»", + "swap \"$VPRO\" \"$QUANT\" \"$PLAIN\" > \"$W/18.protocol\" && swap \"$VCEE\" \"$POST\" \"$POSTYES\" >", + " \"$W/18.c\" && look \"$VSRC\" \"$W/18.c\" \"$W/18.protocol\"" + ], + [ + "квантор назван свёрткой: правило без сличения не засчитано", + "3", + "правило «свёртка» не переиграно", + "swap \"$VPRO\" \"$EVERY\" \"$FOLD\" > \"$W/19.protocol\" && look \"$VSRC\" \"$VCEE\" \"$W/19.protoco", + "l\"" + ] + ] + +тотальная функция «Опыты отбора» + возвращает список список строки + обеспечивает «опытов отбора пять» (длина результат) равен 5 + [ + [ + "честная пара с отбором по признаку: все узлы переиграны", + "0", + "СОШЛОСЬ", + "look \"$FSRC\" \"$FCEE\" \"$FPRO\"" + ], + [ + "отбор пишет по счётчику цикла, а не взятых (C и протокол заодно)", + "1", + "по правилу ждали", + "swap \"$FPRO\" \"$PUT\" \"$MISPUT\" > \"$W/20.protocol\" && swap \"$FCEE\" \"$PUT\" \"$MISPUT\" > \"", + "$W/20.c\" && look \"$FSRC\" \"$W/20.c\" \"$W/20.protocol\"" + ], + [ + "отбор встаёт на первом взятом: цикл с остановкой (C и протокол заодно)", + "1", + "по правилу ждали", + "swap \"$FPRO\" \"$LOOP\" \"$FIRST\" > \"$W/21.protocol\" && swap \"$FCEE\" \"$LOOP\" \"$FIRST\" > \"", + "$W/21.c\" && look \"$FSRC\" \"$W/21.c\" \"$W/21.protocol\"" + ], + [ + "длина отбора названа длиной списка (протокол)", + "1", + "значение «отфильтровать»", + "swap \"$FPRO\" \"$LEN\" \"$WHOLE\" > \"$W/22.protocol\" && look \"$FSRC\" \"$FCEE\" \"$W/22.protocol", + "\"" + ], + [ + "отбор назван отображением: правило без сличения не засчитано", + "3", + "правило «отобразить» не переиграно", + "swap \"$FPRO\" \"$KEEP\" \"$MAP\" > \"$W/23.protocol\" && look \"$FSRC\" \"$FCEE\" \"$W/23.protocol", + "\"" + ] + ] + +тотальная функция «Опыты меры» + возвращает список список строки + обеспечивает «опытов меры четыре» (длина результат) равен 4 + [ + [ + "честная пара с объявленной мерой: узлы сторожа названы числом", + "3", + "узлов сторожа меры 10", + "look \"$MSRC\" \"$MCEE\" \"$MPRO\"" + ], + [ + "сторож меры назван не своим именем (C и протокол заодно)", + "1", + "функции нет в исходнике", + "for ext in c protocol; do sed \"$MUTE\" \"$MBASE.$ext\" > \"$W/24.$ext\" || exit 9; done && look \"$", + "MSRC\" \"$W/24.c\" \"$W/24.protocol\"" + ], + [ + "сторож меры, которого никто не зовёт (протокол)", + "1", + "функции нет в исходнике", + "awk \"$ADD\" \"$MPRO\" > \"$W/25.protocol\" && look \"$MSRC\" \"$MCEE\" \"$W/25.protocol\"" + ], + [ + "сторож меры съехал с места вызова: поблажка узлам снята (протокол)", + "1", + "а не слово узла", + "swap \"$MPRO\" \"$WATCH\" \"$MOVED\" > \"$W/26.protocol\" && look \"$MSRC\" \"$MCEE\" \"$W/26.protoc", + "ol\"" + ] + ] + +тотальная функция «Поле» + принимает части: список строки, номер: число + возвращает строка + пример «третье поле строки опыта — обязательное слово» + дано части равно ["пара", "0", "СОШЛОСЬ", "look"] + дано номер равно 3 + ожидается "СОШЛОСЬ" + пример «номер за списком даёт пусто, а не отказ» + дано части равно ["пара"] + дано номер равно 4 + ожидается "" + если ((номер не меньше 1) и притом (номер не больше (длина части))) + то элемент номер в части + иначе "" + +тотальная функция «Без головы» + принимает части: список строки + возвращает список строки + пример «голова снята, хвост остался» + дано части равно ["раз", "два", "три"] + ожидается ["два", "три"] + пример «у пустого списка снимать нечего» + дано части равно пустой список + ожидается пустой список + разбор части + случай пусто + то пустой список + случай голова и хвост + то хвост + +тотальная функция «Код из знака» + принимает знак: строка + возвращает число + пример «сошлось» + дано знак равно "0" + ожидается 0 + пример «не проверено» + дано знак равно "3" + ожидается 3 + пример «всё прочее — не сошлось» + дано знак равно "1" + ожидается 1 + если знак равен "0" + то 0 + иначе если знак равен "3" + то 3 + иначе 1 + +тотальная функция «Опыт из частей» + принимает части: список строки + возвращает «Опыт» + пример «первые три части — имя, код и слово, остальные склеиваются в дело» + дано части равно ["пара", "0", "ОК", "look ", "x"] + ожидается запись «Опыт» с «что» равным "пара" и «код» равным 0 и «слово» равным "ОК" и «дело» равным "look x" + пусть дело равно (соединить («Без головы» от («Без головы» от («Без головы» от части))) по "") + пусть что равно («Поле» от части и 1) + пусть код равно («Код из знака» от («Поле» от части и 2)) + пусть слово равно («Поле» от части и 3) + запись «Опыт» с «что» равным что и «код» равным код и «слово» равным слово и «дело» равным дело + +тотальная функция «Опыты» + возвращает список «Опыт» + обеспечивает «опытов тридцать два» (длина результат) равен 32 + пусть стопки равно [(«Опыты условия»), («Опыты квантора»), («Опыты отбора»), («Опыты меры»)] + пусть все равно (свёртка стопки начиная с (пустой список) как всё и стопка → «Соединить списки» от всё и стопка) + отобразить все как части → («Опыт из частей» от части) + +тотальная функция «Прелюдия» + принимает работа: строка + возвращает строка + пусть начало равно (приписать (соединить ["W=", работа] по "") к («Пути»)) + пусть хвостик равно («Соединить списки» от («Правки») и («Образцы»)) + соединить («Соединить списки» от начало и хвостик) по "\n" + +тотальная функция «Путь прелюдии» + принимает работа: строка + возвращает строка + пример «прелюдия оболочки лежит во временном каталоге рядом со сличителем» + дано работа равно "/tmp/translation.ab12" + ожидается "/tmp/translation.ab12/prelude.sh" + соединить [работа, "/prelude.sh"] по "" + +тотальная функция «Команда опыта» + принимает работа: строка, дело: строка + возвращает строка + пример «опыт берёт прибор из прелюдии и делает ровно своё дело» + дано работа равно "/tmp/t.ab" + дано дело равно "look x y z" + ожидается ". \"/tmp/t.ab/prelude.sh\"\nlook x y z\n" + соединить [". \"", («Путь прелюдии» от работа), "\"\n", дело, "\n"] по "" + +тотальная функция «Команда сборки» + возвращает строка + обеспечивает «сборка идёт тем же вызовом cc, что у прежней оболочки» результат содержит "-Werror -pedantic -O2" + соединить («Строки сборки») по "\n" + +тотальная функция «Вопросы сборки» + возвращает список «Question» + обеспечивает «вопрос сборки один» (длина результат) равен 1 + [(«Run from» от "сборка" и "../.." и "sh" и ["-c", («Команда сборки»)])] + +тотальная функция «Вопросы прибора» + принимает работа: строка + возвращает список «Question» + обеспечивает «вопросов прибора три» (длина результат) равен 3 + [(«Write» от "прелюдия" и («Путь прелюдии» от работа) и («Прелюдия» от работа)), + («Run from» от "правила описи" и "../.." и "sh" и ["-c", («Команда правил описи»)]), + («Run from» от "правила сличителя" и "../.." и "sh" и ["-c", («Команда правил сличителя»)])] + +тотальная функция «Вопрос опыта» + принимает работа: строка, опыт: «Опыт» + возвращает «Question» + пусть дело равно («Команда опыта» от работа и (опыт.«дело»)) + «Run from» от (опыт.«что») и "../.." и "sh" и ["-c", дело] + +тотальная функция «Вопросы опытов» + принимает работа: строка + возвращает список «Question» + обеспечивает «вопросов столько же, сколько опытов» (длина результат) равен (длина («Опыты»)) + отобразить («Опыты») как опыт → («Вопрос опыта» от работа и опыт) + +тотальная функция «Первая строчка» + принимает текст: строка + возвращает строка + пример «первая строка ответа» + дано текст равно "/tmp/translation.ab12\n" + ожидается "/tmp/translation.ab12" + пример «пустой ответ остаётся пустым» + дано текст равно "" + ожидается "" + разбор (разделить текст по "\n") + случай пусто + то "" + случай голова и хвост + то голова + +тотальная функция «Ответ» + принимает имя: строка, ответы: список «Answer» + возвращает строка + соединить [(«Output of» от имя и ответы), («Errors of» от имя и ответы)] по " " + +тотальная функция «Работа» + принимает ответы: список «Answer» + возвращает строка + если («Exit code of» от "сборка" и ответы) равен 0 + то («Первая строчка» от («Output of» от "сборка" и ответы)) + иначе "" + +тотальная функция «Этап после прибора» + принимает сколько: число, работа: строка + возвращает список «Question» + если сколько равен 1 + то («Вопросы опытов» от работа) + иначе [(«Run» от "уборка" и "rm" и ["-rf", работа])] + +тотальная функция «Этап с работой» + принимает сколько: число, работа: строка + возвращает список «Question» + если сколько равен 2 + то («Вопросы прибора» от работа) + иначе («Этап после прибора» от сколько и работа) + +тотальная функция «Этап после сборки» + принимает сколько: число, ответы: список «Answer» + возвращает список «Question» + пусть работа равно («Работа» от ответы) + если работа равен "" + то пустой список + иначе («Этап с работой» от сколько и работа) + +тотальная функция «Этап» + принимает сколько: число, ответы: список «Answer» + возвращает список «Question» + если сколько равен 3 + то («Вопросы сборки») + иначе («Этап после сборки» от сколько и ответы) + +тотальная функция «Строчки» + принимает текст: строка + возвращает список строки + пример «пустые строки не считаются» + дано текст равно "литерал\n\nсписок\n" + ожидается ["литерал", "список"] + пример «пустой текст — пустой список» + дано текст равно "" + ожидается пустой список + отфильтровать (разделить текст по "\n") где строчка → не (строчка равен "") + +тотальная функция «Правила описи» + принимает ответы: список «Answer» + возвращает список строки + «Строчки» от («Output of» от "правила описи" и ответы) + +тотальная функция «Правила сличителя» + принимает ответы: список «Answer» + возвращает список строки + «Строчки» от («Output of» от "правила сличителя" и ответы) + +тотальная функция «Есть среди» + принимает имя: строка, стопка: список строки + возвращает признак + пример «имя из списка» + дано имя равно "случай" + дано стопка равно ["разбор", "случай"] + ожидается да + пример «чужого имени в списке нет» + дано имя равно "свёртка" + дано стопка равно ["разбор", "случай"] + ожидается нет + (длина (отфильтровать стопка где другое → другое равен имя)) больше 0 + +тотальная функция «Только в» + принимает одни: список строки, другие: список строки + возвращает список строки + пример «что есть в первом и чего нет во втором» + дано одни равно ["разбор", "случай"] + дано другие равно ["разбор"] + ожидается ["случай"] + отфильтровать одни где имя → не («Есть среди» от имя и другие) + +тотальная функция «Слово о списке» + принимает тут: список строки, там: список строки + возвращает строка + пример «названо то, что есть лишь в одном из двух» + дано тут равно ["случай"] + дано там равно пустой список + ожидается "закрытый список разошёлся — только в PRINT-RULES.tsv: случай; только в matcher.c: " + соединить ["закрытый список разошёлся — только в PRINT-RULES.tsv: ", (соединить тут по ", "), + "; только в matcher.c: ", (соединить там по ", ")] по "" + +тотальная функция «Беда списка» + принимает опись: список строки, сличитель: список строки + возвращает список строки + пусть тут равно («Только в» от опись и сличитель) + пусть там равно («Только в» от сличитель и опись) + если ((длина тут) плюс (длина там)) равен 0 + то пустой список + иначе [(«Слово о списке» от тут и там)] + +тотальная функция «Кратко» + принимает текст: строка + возвращает строка + пример «переводы строк становятся пробелами» + дано текст равно "раз\nдва" + ожидается "раз два" + пусть одной равно (соединить (разделить (соединить (разделить текст по "\n") по " ") по "\r") по "") + если (длина одной) не больше 400 + то одной + иначе подстрока одной с 1 по 400 + +тотальная функция «Сошёлся» + принимает опыт: «Опыт», ответы: список «Answer» + возвращает признак + пусть ответ равно («Ответ» от (опыт.«что») и ответы) + пусть код равно («Exit code of» от (опыт.«что») и ответы) + (код равен (опыт.«код»)) и притом (ответ содержит (опыт.«слово»)) + +тотальная функция «Жалоба опыта» + принимает опыт: «Опыт», ответы: список «Answer» + возвращает строка + пусть код равно (к строке («Exit code of» от (опыт.«что») и ответы)) + пусть ответ равно («Кратко» от («Ответ» от (опыт.«что») и ответы)) + соединить [(опыт.«что»), " — ждали код ", (к строке (опыт.«код»)), " со словом «", (опыт.«слово»), + "», ответил кодом ", код, ": ", ответ] по "" + +тотальная функция «Жалобы опытов» + принимает ответы: список «Answer» + возвращает список строки + пусть разошлись равно (отфильтровать («Опыты») где опыт → не («Сошёлся» от опыт и ответы)) + отобразить разошлись как опыт → («Жалоба опыта» от опыт и ответы) + +тотальная функция «Жалобы» + принимает ответы: список «Answer» + возвращает список строки + пусть опись равно («Правила описи» от ответы) + пусть закрытый равно («Беда списка» от опись и («Правила сличителя» от ответы)) + «Соединить списки» от закрытый и («Жалобы опытов» от ответы) + +тотальная функция «Слово согласия» + принимает ответы: список «Answer» + возвращает строка + пусть правил равно (к строке (длина («Правила описи» от ответы))) + пусть опытов равно (к строке (длина («Опыты»))) + соединить ["перевод: закрытый список ", правил, " правил, опытов ", опытов, + ", все сошлись с ожиданием"] по "" + +тотальная функция «Слово отказа» + принимает жалобы: список строки + возвращает строка + пример «заголовок называет число опытов и число бед, жалобы идут по одной» + дано жалобы равно ["пара — ждали код 0"] + ожидается "перевод: опытов 32, бед 1\n · пара — ждали код 0" + пусть заголовок равно (соединить ["перевод: опытов ", (к строке (длина («Опыты»))), ", бед ", + (к строке (длина жалобы))] по "") + соединить (приписать заголовок к жалобы) по "\n · " + +тотальная функция «Нечем смотреть» + принимает весть: строка + возвращает «Продолжение» + пример «невозможность смотреть — не расхождение» + дано весть равно "не собран" + ожидается вариант «Не проверено» с код равным "FLANG_PEREVOD_NECHEM" и сообщение равным "перевод: не собран" + пусть слово равно (соединить ["перевод: ", весть] по "") + вариант «Не проверено» с код равным "FLANG_PEREVOD_NECHEM" и сообщение равным слово + +тотальная функция «Беда правил» + принимает ответы: список «Answer» + возвращает строка + пусть опись равно («Exit code of» от "правила описи" и ответы) + пусть код равно («Exit code of» от "правила сличителя" и ответы) + если (опись плюс код) равен 0 + то "" + иначе "закрытый список не прочитан: PRINT-RULES.tsv или matcher.c не отдались" + +тотальная функция «Беда прелюдии» + принимает ответы: список «Answer» + возвращает строка + разбор («Reply to» от "прелюдия" и ответы) + случай вариант «Записано» с сколько как сколько + то "" + случай любое + то "прелюдия оболочки не записана во временный каталог" + +тотальная функция «Беда прибора» + принимает ответы: список «Answer» + возвращает строка + пусть беда равно («Беда прелюдии» от ответы) + если беда равен "" + то («Беда правил» от ответы) + иначе беда + +тотальная функция «Беда подготовки» + принимает ответы: список «Answer» + возвращает строка + если («Exit code of» от "сборка" и ответы) равен 0 + то («Беда прибора» от ответы) + иначе (соединить ["сличитель не собран: ", («Кратко» от («Ответ» от "сборка" и ответы))] по "") + +тотальная функция «Суд» + принимает ответы: список «Answer» + возвращает «Продолжение» + пусть жалобы равно («Жалобы» от ответы) + если (длина жалобы) равен 0 + то вариант «Конец работы» с значение равным («Слово согласия» от ответы) + иначе вариант «Провал» с код равным "FLANG_PEREVOD_RAZOSHLIS" и сообщение равным («Слово отказа» от жалобы) + +тотальная функция «Приговор» + принимает ответы: список «Answer» + возвращает «Продолжение» + пусть беда равно («Беда подготовки» от ответы) + если беда равен "" + то «Суд» от ответы + иначе «Нечем смотреть» от беда + +тотальная функция «Идти» + принимает очередь: список «Question», сколько: число, ответы: список «Answer» + возвращает «Продолжение» + разбор очередь + случай голова и хвост + то «Ask» от (голова) и (хвост) и сколько и ответы + случай пусто + то если сколько не больше 0 + то «Приговор» от ответы + иначе «Идти» от («Этап» от (сколько минус 1) и ответы) и (сколько минус 1) и ответы + +тотальная функция «Начать» + возвращает «Inquiry» + «Begin with» от 4 + +тотальная функция «Дальше» + принимает inquiry: «Inquiry», отклик: «Отклик» + возвращает «Продолжение» + «Идти» от (inquiry.«queue») и (inquiry.«stages») и («Heard» от inquiry и отклик) + +план «Проверка» + состояние «Inquiry» + начинает с «Начать» + обрабатывает «Дальше» + +тотальная функция «Объявление короткой команды translation:check» + возвращает строка + "bootstrap/flang io --plan Проверка — протокол перевода переигрывается на C: честные пары сходятся, подделки — нет" diff --git a/flang/translation/run.sh b/flang/translation/run.sh deleted file mode 100644 index 8615df0e5..000000000 --- a/flang/translation/run.sh +++ /dev/null @@ -1,214 +0,0 @@ -#!/bin/sh -# SPDX-FileCopyrightText: 2026 Digitable (Marat Zimnurov) -# SPDX-License-Identifier: BSD-2-Clause -# -# СЛИЧИТЕЛЬ ПЕРЕВОДА: честные пары сходятся, подделки не принимаются. -# ADR-0030 «Печатник доказывает КАЖДЫЙ СВОЙ ЗАПУСК», задача 1401. -# -# sh flang/translation/run.sh -# -# Код 0 — всё, как ждали; 1 — хоть один опыт разошёлся с ожиданием. -# -# Честные пары лежат в fixtures/: напечатанный C и протокол перевода примеров -# flang/proof/examples/, снятые печатником flang/self/emit-c.flang. Подделки -# строятся здесь же из честных пар — каждая одной правкой, названной словами. -set -u -KOREN=$(cd "$(dirname "$0")/../.." && pwd) -TUT=$KOREN/flang/translation -RAB=$(mktemp -d "${TMPDIR:-/tmp}/translation.XXXXXX") -trap 'rm -rf "$RAB"' EXIT INT TERM - -cc -std=c99 -Wall -Wextra -Werror -pedantic -O2 -o "$RAB/matcher" "$TUT/matcher.c" || exit 1 - -awk -F'\t' '!/^#/ && $1 != "имя" && NF { print $1 }' "$TUT/PRINT-RULES.tsv" > "$RAB/rules.tsv" -sed -n '/^static const char \*const RULES\[\] = {$/,/^};$/p' "$TUT/matcher.c" | - sed -n 's/^ "\(.*\)",$/\1/p' > "$RAB/rules.c" -if ! cmp -s "$RAB/rules.tsv" "$RAB/rules.c"; then - echo "КРАСЕН закрытый список: PRINT-RULES.tsv и RULES[] в matcher.c разошлись" - diff "$RAB/rules.tsv" "$RAB/rules.c" - exit 1 -fi -echo "зелен закрытый список: $(wc -l < "$RAB/rules.tsv") правил, в PRINT-RULES.tsv и в matcher.c одни и те же" - -BEDA=0 -VSEGO=0 -# opyt <что> <ждём: 0|1|3> <исходник> <протокол> [слово, которое обязано быть в ответе] -opyt() { - chto=$1; zhdem=$2; ish=$3; si=$4; prot=$5; slovo=${6:-} - VSEGO=$((VSEGO + 1)) - "$RAB/matcher" "$ish" "$si" "$prot" > "$RAB/otvet" 2>&1 - kod=$? - if [ "$kod" = "$zhdem" ] && { [ -z "$slovo" ] || grep -qF -- "$slovo" "$RAB/otvet"; }; then - printf 'зелен %s (код %s)\n' "$chto" "$kod" - else - printf 'КРАСЕН %s: ждали код %s%s, получили %s\n' "$chto" "$zhdem" "${slovo:+ со словом «$slovo»}" "$kod" - sed 's/^/ /' "$RAB/otvet" | head -n 5 - BEDA=$((BEDA + 1)) - fi -} - -# ── правки для подделок ───────────────────────────────────────────────────── -# vyrezat <файл> <с> <по> <начало строки «с»>: файл без строк с…по; если строка -# «с» начинается не так, подделка не построена — это отказ прогона, а не опыт. -vyrezat() { - if ! sed -n "$2p" "$1" | grep -qF -- "$4"; then - echo "КРАСЕН подделка не построена: в $(basename "$1") строка $2 не «$4»" >&2 - exit 1 - fi - sed "$2,$3d" "$1" -} -# zamenit <файл> <было> <стало>: заменить единственное вхождение строки; было -# оно не одно — подделка не построена. -zamenit() { - n=$(grep -cF -- "$2" "$1") - if [ "$n" != 1 ]; then - echo "КРАСЕН подделка не построена: «$2» в $(basename "$1") встречается $n раз" >&2 - exit 1 - fi - awk -v old="$2" -v new="$3" '{ i = index($0, old); if (i) $0 = substr($0, 1, i - 1) new substr($0, i + length(old)); print }' "$1" -} - -PRIMERY=$KOREN/flang/proof/examples -OSN=$TUT/fixtures/forgery-if-without-descent -ISH=$PRIMERY/forgery-if-without-descent.flang -SI=$OSN/poddelka_usloviya_bez_spuska.c -PR=$OSN/poddelka_usloviya_bez_spuska.protocol -SV=$TUT/fixtures/traffic-light - -opyt "честная пара: четыре функции, все правила переиграны" 0 "$ISH" "$SI" "$PR" "СОШЛОСЬ" -opyt "честная пара с разбором: сошлось, непереигранное названо" 3 "$PRIMERY/traffic-light.flang" \ - "$SV/svetofor.c" "$SV/svetofor.protocol" "правило «случай» не переиграно" - -VYZOV='poddelka_usloviya_bez_spuska_stoit_na_meste(ctx, n, &fl_t3' -DRUGOY='poddelka_usloviya_bez_spuska_cherez_odno(ctx, n, &fl_t3' - -zamenit "$PR" "$VYZOV" "$DRUGOY" > "$RAB/1.protocol" -opyt "подменённый фрагмент протокола: вызов другой функции" 1 "$ISH" "$SI" "$RAB/1.protocol" "напечатанный C, строка 22" - -zamenit "$SI" 'fl_t2 = fl_t3;' 'fl_t2 = fl_t1;' > "$RAB/2.c" -opyt "изменённая строка C при прежнем протоколе" 1 "$ISH" "$RAB/2.c" "$PR" "напечатанный C, строка" - -vyrezat "$PR" 49 51 'узел var строка 9 столбец 31' > "$RAB/3.protocol" -opyt "пропущенный узел: довод вызова выпал из протокола" 1 "$ISH" "$SI" "$RAB/3.protocol" "исходник строка 9 столбец 11" - -opyt "протокол от другого исходника" 1 "$PRIMERY/traffic-light.flang" "$SI" "$PR" "протокол от другого исходника" - -zamenit "$PR" "$VYZOV" "$DRUGOY" > "$RAB/6.protocol" -zamenit "$SI" "$VYZOV" "$DRUGOY" > "$RAB/6.c" -opyt "подменённая функция в напечатанном коде (C и протокол заодно)" 1 "$ISH" "$RAB/6.c" "$RAB/6.protocol" \ - "по правилу ждали" - -vyrezat "$PR" 45 59 'часть иначе строк 1' > "$RAB/7.protocol" -vyrezat "$SI" 20 23 '} else {' > "$RAB/7.c" -opyt "потерянная ветвь «иначе» (C и протокол заодно)" 1 "$ISH" "$RAB/7.c" "$RAB/7.protocol" "не три ветви" - -PARA='kruzhit_po_pare(ctx, m, n, &fl_t8' -NAOBOROT='kruzhit_po_pare(ctx, n, m, &fl_t8' -zamenit "$PR" "$PARA" "$NAOBOROT" > "$RAB/8.protocol" -zamenit "$SI" "$PARA" "$NAOBOROT" > "$RAB/8.c" -opyt "переставленные доводы (C и протокол заодно)" 1 "$ISH" "$RAB/8.c" "$RAB/8.protocol" "исходник строка 17 столбец 11" - -zamenit "$PR" 'столбец 11 правило «вызов» имя «Стоит на месте»' 'столбец 11 правило «вызов-наугад» имя «Стоит на месте»' > "$RAB/9.protocol" -opyt "правило не из закрытого списка" 1 "$ISH" "$SI" "$RAB/9.protocol" "не из закрытого списка" - -zamenit "$PR" 'столбец 11 правило «вызов» имя «Стоит на месте»' 'столбец 12 правило «вызов» имя «Стоит на месте»' > "$RAB/10.protocol" -opyt "место узла сдвинуто на знак" 1 "$ISH" "$SI" "$RAB/10.protocol" "на этом месте исходника" - -vyrezat "$PR" 360 472 'функция «Дно зовёт себя»' > "$RAB/11.protocol" -vyrezat "$SI" 146 189 '/* Тело «Дно зовёт себя»' > "$RAB/11.c" -opyt "функция замолчана (C и протокол заодно)" 1 "$ISH" "$RAB/11.c" "$RAB/11.protocol" "протокол о ней молчит" - -sed '$d' "$PR" > "$RAB/12.protocol" -opyt "оборванный протокол" 1 "$ISH" "$SI" "$RAB/12.protocol" "оборван" - -{ cat "$SI"; echo '/* строка, которой не печатал ни один узел */'; } > "$RAB/13.c" -opyt "лишняя строка в конце C" 1 "$ISH" "$RAB/13.c" "$PR" "не напечатал ни один узел" - -vyrezat "$PR" 162 164 'узел var строка 17 столбец 31' > "$RAB/14a.protocol" -zamenit "$RAB/14a.protocol" "$PARA" 'kruzhit_po_pare(ctx, n, &fl_t8' > "$RAB/14.protocol" -zamenit "$SI" "$PARA" 'kruzhit_po_pare(ctx, n, &fl_t8' > "$RAB/14.c" -opyt "довод выпал (C и протокол заодно)" 1 "$ISH" "$RAB/14.c" "$RAB/14.protocol" "доводов у вызова 1, а функция в исходнике принимает 2" - -zamenit "$PR" 'граница входа' 'граница выхода' > "$RAB/15.protocol" -opyt "подложный блок протокола" 1 "$ISH" "$SI" "$RAB/15.protocol" "блок не из закрытого списка" - -# ── две дыры замера 18 сентября (задача 1401): подделки лежат в fixtures/ ──── -# Обе — из честной пары одной названной правкой, и обе правки проигрываются -# здесь заново: построенное обязано совпасть с файлом дерева байт в байт. -# Разойдись они — фикстура прогнила, и опыт больше не про то, про что написан. -sverit() { # <построенное здесь> <подделка в дереве> - if ! cmp -s "$1" "$2"; then - echo "КРАСЕН подделка прогнила: $(basename "$2") в дереве не равна построенной здесь" >&2 - exit 1 - fi -} -# stroka <файл> <номер> <что обязано стоять в строке>: иначе подделка не построена. -stroka() { - if ! sed -n "$2p" "$1" | grep -qF -- "$3"; then - echo "КРАСЕН подделка не построена: в $(basename "$1") строка $2 не «$3»" >&2 - exit 1 - fi -} - -# Дыра 1. Переименованная временная: fl_t3 → fl_t2 разом в C и в протоколе. -# Внутренняя временная ветви «иначе» схлопывается с внешней временной «если» — -# накрытие во вложенной области. Текст сходится байт в байт, смысл меняется. -IMYA=$OSN/podmena_imeni_vremennoy -for rasshirenie in c protocol; do - sed 's/fl_t3\([^0-9A-Za-z_]\)/fl_t2\1/g; s/fl_t3$/fl_t2/' \ - "$OSN/poddelka_usloviya_bez_spuska.$rasshirenie" > "$RAB/imya.$rasshirenie" - sverit "$RAB/imya.$rasshirenie" "$IMYA.$rasshirenie" -done -opyt "переименованная временная: внутренняя накрыла внешнюю (C и протокол заодно)" 1 \ - "$ISH" "$IMYA.c" "$IMYA.protocol" "накрывает живое имя" - -# Дыра 2. Переставленные операнды сравнения: «н не больше 0» напечатано как -# «0 не больше н», и два блока детей в протоколе переставлены под этот порядок. -# Значение сходится, потому что оно считается по детям в порядке ПРОТОКОЛА. -PRYAMO='fl_flag(n.as.number <= 0.0)' -NAVYVOROT='fl_flag(0.0 <= n.as.number)' -OPER=$OSN/perestavlennye_operandy -stroka "$PR" 10 'узел var строка 7 столбец 8 правило «число-распакованное»' -stroka "$PR" 16 'узел literal строка 7 столбец 20 правило «число-литерал»' -stroka "$PR" 21 "значение $PRYAMO" -stroka "$PR" 25 "$PRYAMO" -stroka "$SI" 16 "$PRYAMO" -{ sed -n '1,9p' "$PR"; sed -n '16,18p' "$PR"; sed -n '10,15p' "$PR"; sed -n '19,$p' "$PR"; } | - sed "21s/$PRYAMO/$NAVYVOROT/; 25s/$PRYAMO/$NAVYVOROT/" > "$RAB/oper.protocol" -sed "16s/$PRYAMO/$NAVYVOROT/" "$SI" > "$RAB/oper.c" -sverit "$RAB/oper.protocol" "$OPER.protocol" -sverit "$RAB/oper.c" "$OPER.c" -opyt "переставленные операнды сравнения (дети протокола подогнаны)" 1 \ - "$ISH" "$OPER.c" "$OPER.protocol" "не в порядке мест исходника" - -# ── квантор по элементам (правило «все-элементы», задача 7098) ────────────── -VSE=$TUT/fixtures/all-elements -VISH=$VSE/all-elements.flang -VSI=$VSE/all_elements_at_the_boundary.c -VPR=$VSE/all_elements_at_the_boundary.protocol - -opyt "честная пара с квантором по элементам: все узлы переиграны" 0 "$VISH" "$VSI" "$VPR" "СОШЛОСЬ" - -zamenit "$VPR" 'fl_t3 && fl_t4 < fl_t2' 'fl_t4 < fl_t2' > "$RAB/16.protocol" -zamenit "$VSI" 'fl_t3 && fl_t4 < fl_t2' 'fl_t4 < fl_t2' > "$RAB/16.c" -opyt "квантор без остановки на первом «нет» (C и протокол заодно)" 1 "$VISH" "$RAB/16.c" "$RAB/16.protocol" "по правилу ждали" - -zamenit "$VPR" 'bool fl_t3 = true; /* для всех «п» */' 'bool fl_t3 = false; /* для всех «п» */' > "$RAB/17.protocol" -zamenit "$VSI" 'bool fl_t3 = true; /* для всех «п» */' 'bool fl_t3 = false; /* для всех «п» */' > "$RAB/17.c" -opyt "квантор начат с «нет»: на пустом списке ложь (C и протокол заодно)" 1 "$VISH" "$RAB/17.c" "$RAB/17.protocol" "по правилу ждали" - -zamenit "$VPR" 'значение fl_flag(fl_t3)' 'значение fl_flag(true)' > "$RAB/18.protocol" -zamenit "$VSI" 'fl_post(ctx, fl_flag(fl_t3),' 'fl_post(ctx, fl_flag(true),' > "$RAB/18.c" -opyt "сторож обещания сверяет «да» вместо квантора (C и протокол заодно)" 1 "$VISH" "$RAB/18.c" "$RAB/18.protocol" "значение «для всех»" - -zamenit "$VPR" 'правило «все-элементы» элемент «п»' 'правило «свёртка» элемент «п»' > "$RAB/19.protocol" -opyt "квантор назван свёрткой: правило без сличения не засчитано" 3 "$VISH" "$VSI" "$RAB/19.protocol" "правило «свёртка» не переиграно" - -echo -if [ "$BEDA" = 0 ]; then - echo "ИТОГ: опытов $VSEGO, все сошлись с ожиданием" - exit 0 -fi -echo "ИТОГ: опытов $VSEGO, разошлись с ожиданием $BEDA" -exit 1 -# короткая команда «translation:check» sh — протокол перевода в C переигрывается сличителем на C: честные пары сходятся, подделки протокола и напечатанного C не принимаются (ADR-0030) diff --git a/scripts/ledgers/proved-share-ledger.txt b/scripts/ledgers/proved-share-ledger.txt index 671685606..bfed5db88 100644 --- a/scripts/ledgers/proved-share-ledger.txt +++ b/scripts/ledgers/proved-share-ledger.txt @@ -1777,3 +1777,8 @@ cf872d516e34dd69bc73a4e95995017f|2|2|0|0|0|flang/proof/checker/tests/families/fm // Три программы каталога `programs/` обязательств не несут и в опись не // входят по общему правилу шапки. 38286ffe6728e1fb395a6be84acf6c23|3|3|0|0|0|flang/proof/probes/runs-not-executed/run.fscript +// ── Сличитель перевода на плане (перенос run.sh), снято 4 октября 2026 ────── +// Приговор снят `flang check --proof` этого же дерева: «утверждений 15: +// доказано 15 (из них без теоремы 15), сетка 0, объявлено, не доказано 0». +// `требует` и `закон` в файле нет, потому «без приговора» ноль. +11d6263322f60bf76452901348c7981d|15|15|0|0|0|flang/translation/run.fscript