From 40475040e595b6006bbac39c0a8f71bd4c338053 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Sun, 4 Oct 2026 16:05:39 +0000 Subject: [PATCH 1/3] refactor(translation): the matcher suite is a proved plan with 32 probes flang/translation/run.sh (214 lines of shell) is gone; the same work is now flang/translation/run.fscript, a plan the kernel proves: 15 obligations, all 15 proved, so the shortcut runs without --trust. Nine probes that lived only in the body of PR 298 are written in: five on the list-filter rule and four on the measure-guard allowance. The expectations are measured, not predicted - every one answered exactly what that block said it would, so the suite grew from 23 probes to 32 and all 32 match. What proves the move is right: the 32 triples (name, expected code, required word) were taken by instrument from both files - from run.sh by parsing its probe calls, from the plan by running its probe-table function - and they are identical. Both run green on one tree: 32 probes, zero divergences, code 0. Negative control, three forgeries: a number in the printed C of the traffic light (500 -> 501), one rule cut out of PRINT-RULES.tsv, and a number in the printed C of the declared measure (1.0 -> 2.0). On each one both go red with code 1 and name the same place. Two differences are deliberate and written in the file. A diverged closed list no longer stops the run before the first probe - it becomes complaint number one and the probes still run. A forgery that fails to build now reddens its own probe by name instead of aborting the whole run. CI calls the plan by its shortcut and takes the binary from the shared cache the way its neighbours do, because a plan needs the binary; the forgery probe greps for the plan's complaint line. The counted marks in this workflow follow the shell file that left. --- .flangrc | 2 +- .github/workflows/binary.yml | 41 +- flang/translation/run.fscript | 818 ++++++++++++++++++++++++++++++++++ flang/translation/run.sh | 214 --------- 4 files changed, 853 insertions(+), 222 deletions(-) create mode 100644 flang/translation/run.fscript delete mode 100644 flang/translation/run.sh 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..16f2dd62c 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -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 при прежнем протоколе. Прогон обязан покраснеть ИМЕННО на этой @@ -1499,6 +1504,28 @@ jobs: - 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 +1537,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 +1545,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/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) From 3f7b28792ae1ab928b7ded9dacf60c05898220b9 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Sun, 4 Oct 2026 16:05:53 +0000 Subject: [PATCH 2/3] chore(ledger): counted numbers follow the shell script that left The translation suite moved from shell to a plan, so the numbers it is counted in move with it: one shell file and 214 shell lines less, one file less outside flang. Taken by instrument (inventory:languages for the table, prose-numbers-guard for the marks), not by hand: docs/tree-inventory.md shell row 56 / 9875 -> 55 / 9661, title 193 -> 192 docs/javascript-inventory.md 193 -> 192 .github/workflows/binary.yml shell 50 / 9558 -> 49 / 9344, total 193 -> 192 .github/workflows/ci.yml shell files 50 -> 49 After it: inventory:check code 0, prose-numbers-guard 209 marks of 209 agree. scripts/ledgers/proved-share-ledger.txt takes a row for the new plan: 15 written, 15 proved, 0 on a grid, 0 declared, 0 without a verdict. The verdict was taken by flang check --proof on this tree, not assumed. docs/four-coverages.md pointed at the removed run.sh; the link now names run.fscript, so links:check stays at 88 broken paths of 7130 - the same count as the base of this branch. Not touched, because they belong to other cells: scripts/four-coverages.fscript still reads and runs flang/translation/run.sh, so section 4 of that report will print "NOT TAKEN" until its owner renames the path; docs/adr/0030 line 273 still names the shell command in prose. --- .github/workflows/binary.yml | 10 +++++----- .github/workflows/ci.yml | 4 ++-- docs/four-coverages.md | 2 +- docs/javascript-inventory.md | 4 ++-- docs/tree-inventory.md | 6 +++--- scripts/ledgers/proved-share-ledger.txt | 5 +++++ 6 files changed, 18 insertions(+), 13 deletions(-) diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index 16f2dd62c..8fb3ccab7 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 опись умирает 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/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 From 321eef5ccc24f506a5957bebf62db0ab46a9cd97 Mon Sep 17 00:00:00 2001 From: Marat Zimnurov Date: Sun, 4 Oct 2026 16:24:14 +0000 Subject: [PATCH 3/3] ci(translation): the matcher job gets twenty minutes for a seed build The suite is a plan now, so the job builds the seed on a cache miss. Ten minutes were the budget of a shell run that needed only cc; its neighbour guards-selftest, which builds the same seed, asks for twenty. --- .github/workflows/binary.yml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index 8fb3ccab7..7ad1f576e 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -1499,7 +1499,11 @@ 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