diff --git a/.flangrc b/.flangrc index b0771936c..719539580 100644 --- a/.flangrc +++ b/.flangrc @@ -59,6 +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.kernel-memo:probe = bootstrap/flang io flang/proof/probes/kernel-memo/run.fscript script.ru-morphology:probe = bootstrap/flang io flang/proof/probes/ru-morphology/run.fscript --plan Binary script.ru-morphology:forgery = bootstrap/flang io flang/proof/probes/ru-morphology/run.fscript --plan Forgery script.ru-morphology:snap = bootstrap/flang io flang/proof/probes/ru-morphology/run.fscript --plan Snap diff --git a/.github/workflows/binary.yml b/.github/workflows/binary.yml index d44c90990..55635c09e 100644 --- a/.github/workflows/binary.yml +++ b/.github/workflows/binary.yml @@ -1859,6 +1859,29 @@ jobs: - name: Check import list order run: cd flang/proof/probes/import-list-order && ../../../../bootstrap/flang io run.fscript --plan Binary + # ПАМЯТЬ ВЫЗОВОВ ЯДРА НЕ СМЕЕТ МЕНЯТЬ ОТВЕТ, и до 4 октября 2026 этого не + # спрашивал никто. Проба лежала в дереве с ветки задачи 5709 и не звалась + # ниоткуда: ни работой, ни ярлыком, ни хуком, — на неё и краснела работа + # `checks-nobody-calls` выключенного `ci.yml` (задача 5310). + # + # Место здесь, а не отдельной работой: двоичный уже собран, а все + # двадцать её сестёр из `flang/proof/probes/**` стоят этими же шагами + # выше. Зовём путём от корня, как сосед `plan-rules-asked`: пути + # поручений проба считает от своего каталога, и `cd` ей не нужен. + # + # ЦЕНА НАЗВАНА, А НЕ СПРЯТАНА. Замер 4 октября 2026 на дереве 5604556ef, + # двоичный 0.7.23, 256 ядер под чужой нагрузкой: 175,5 с, пик 0,36 ГиБ, + # код 0, «kernel memo: runs 6, memo on and audit answer byte for byte as + # memo off». Шесть прогонов `check --proof` на двух модулях stdlib при + # FLANG_MEMO=0, =1 и =1 с пересчётом каждого попадания; ответы сверяются + # кодом и выводом знак в знак. Работа `guards-selftest` на раннере идёт + # 6 мин 47 с — 7 мин 01 с (заходы 37223001273 и 37223864296), и это + # число на раннере не мерено: 175,5 с — пол, снятый на этой машине. + - name: Check kernel memo does not change the answer + run: bootstrap/flang io flang/proof/probes/kernel-memo/run.fscript + env: + FLANG_BIN: ${{ github.workspace }}/bootstrap/flang + # ── БЛОКИ «прогон»: НАЗВАНЫ ЧИСЛОМ ИЛИ ПРОХОДЯТ МОЛЧА (задача 1116) ─────── # # ПОЧЕМУ ОТДЕЛЬНАЯ РАБОТА, А НЕ ШАГ У СОСЕДЕЙ ВЫШЕ. Эта проба собирает ВТОРОЙ diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ffcf10e6d..24f97672d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1382,11 +1382,15 @@ jobs: # Обещание «бэкенд занимает ровно пять имён» — правда; подменяем на # шесть, и сторож обязан назвать функцию и обещание поимённо. cp "$podlog" "$podlog.do" - sed -i '75s/равен 5$/равен 6/' "$podlog" - # Та же защита: подлог прибит к строке 75. + # ПОДЛОГ ПРИБИТ К ОБЕЩАНИЮ, А НЕ К НОМЕРУ СТРОКИ, и это та же грабля, + # что у «Probe blockers table» выше: номер 75 съехал на 20, `sed` + # смолчал, и шаг краснел словами «подлог не собрался» на нетронутом + # файле. Померено задачей 1117 (перемер 4 октября 2026: код 1 за + # 0,0 с). Обещание в файле одно, образец однозначен. + sed -i 's/^\( обеспечивает «бэкенд занимает ровно пять имён» (длина результат) равен \)5$/\16/' "$podlog" if cmp -s "$podlog.do" "$podlog"; then rm -f "$podlog.do"; git checkout -- "$podlog" - echo "ПОДЛОГ НЕ СОБРАЛСЯ: строка 75 $podlog уже не та — поправить подлог, сторож ни при чём" >&2 + echo "ПОДЛОГ НЕ СОБРАЛСЯ: обещания «бэкенд занимает ровно пять имён» со «равен 5» в $podlog нет — поправить подлог, сторож ни при чём" >&2 exit 1 fi rm -f "$podlog.do" diff --git a/docs/course/03-totality.md b/docs/course/03-totality.md index f2e8a48c5..0a447f7e0 100644 --- a/docs/course/03-totality.md +++ b/docs/course/03-totality.md @@ -101,9 +101,9 @@ bootstrap/flang run-script numbers:build и сверяет отдельной проверкой. У файла две половины с разной родословной: «дешёвая» (число файлов) пересчитана 18 сентября 2026 на коммите `d6e88d50` за девять секунд, «дорогая» (функции, тотальность, носители обещания, места -сторожей) — 23 августа 2026 на коммите `252606e8` прогоном двоичного по всему -корпусу в несколько часов. Дорогая половина на 0.7.22 не снята заново: пересчёт -не укладывается в отведённое время.* +проверок) — 23 августа 2026 на коммите `252606e8` прогоном двоичного по всем +программам репозитория в несколько часов. Дорогая половина на 0.7.22 не снята +заново: пересчёт не укладывается в отведённое время.* Разберём таблицу. diff --git a/docs/course/09-eight-targets.md b/docs/course/09-eight-targets.md index b2e083fd2..109eb061e 100644 --- a/docs/course/09-eight-targets.md +++ b/docs/course/09-eight-targets.md @@ -277,8 +277,8 @@ dotnet bin/Debug/net8.0/flang.dll MestoVstavki > согласии: `nadzor-uzla.test.mjs` держит `cpp` в списке `С_НАДЗОРОМ`, > `uzel-osnastka.mjs` описывает его тулчейн (`c++`/`g++`), а > `self-ledger.txt` строкой 13 записывает `flang/self/emit-cpp.flang вне -> присмотра 10` — то есть сам печатник цели из присмотра как раз выпадает, на -> десяти счётах. +> присмотра 10` — то есть сам генератор кода цели из присмотра как раз +> выпадает, на десяти счётах. > > Чего этот замер НЕ говорит: совпадает ли `cpp` с интерпретатором на всех > программах репозитория так же полно, как остальные восемь. Снят только `grep`; diff --git a/docs/course/13-where-next.md b/docs/course/13-where-next.md index 82b502316..4e15dfeb1 100644 --- a/docs/course/13-where-next.md +++ b/docs/course/13-where-next.md @@ -109,7 +109,7 @@ node docs/site/build.mjs --check половины, и родословная у них разная: «дешёвая» (файлы, строки, версия выпуска) пересчитана 18 сентября 2026 на коммите `d6e88d50`, «дорогая» (функции, тотальность, утверждения, словарь) — 23 августа 2026 на коммите `252606e8`, -прогоном двоичного по всему корпусу в несколько часов. +прогоном двоичного по всем программам репозитория в несколько часов. **И честная оговорка, которая пережила все правки.** Проверка чисел не входит в `npm test`, и расхождение между файлом и деревом может стоять неделями. Так и diff --git a/docs/guide/how-to-write-flang.ru.md b/docs/guide/how-to-write-flang.ru.md index 2dce7a3f7..560cda847 100644 --- a/docs/guide/how-to-write-flang.ru.md +++ b/docs/guide/how-to-write-flang.ru.md @@ -41,8 +41,8 @@ нельзя сослаться, и он расходится с кодом молча — код правят, приписка остаётся. Прибавку комментариев не пускает храповик `scripts/guards/no-comments-guard.fscript`: долг -записан пофайлово (`scripts/ledgers/no-comments-debt.tsv`) и может только убывать. Сторож стоит -в `.githooks/pre-push`, считает все пять расширений языка и хвостовые `//` тоже, а `//` внутри +записан пофайлово (`scripts/ledgers/no-comments-debt.tsv`) и может только убывать. +Проверка стоит в `.githooks/pre-push`, считает все пять расширений языка и хвостовые `//` тоже, а `//` внутри строкового литерала за комментарий не принимает. В долге сегодня только входы печати семени (`flang/self/**` и файлы из `scripts/seed-fingerprint`, их комментарии уходят со следующей печатью) и пять проб сверщика, где комментарий и есть подделка diff --git a/docs/jargon.json b/docs/jargon.json index 3489248f4..c8df7338c 100644 --- a/docs/jargon.json +++ b/docs/jargon.json @@ -441,6 +441,18 @@ "внутри": "repl_call(\"Свести корпус\"", "почему": "имя функции на flang (flang/self/bootstrap/corpus.flang:778), а не текст для читателя: переименовать его текстовым запретом нельзя, только перепечаткой" }, + { + "файл": "flang/src/emit/c/flang_repl.c", + "слово": "корпус", + "внутри": "repl_call(\"Каталоги мимо корпуса\"", + "почему": "имя функции на flang (flang/self/bootstrap/corpus.flang:270), а не текст для читателя: та же порода, что у «Свести корпус» выше — переименовать текстовым запретом нельзя, только перепечаткой" + }, + { + "файл": "flang/src/emit/c/flang_repl.c", + "слово": "корпус", + "внутри": "repl_call(\"Отбор корпуса\"", + "почему": "имя функции на flang (flang/self/bootstrap/corpus.flang:334), а не текст для читателя: та же порода, что у «Свести корпус» выше — переименовать текстовым запретом нельзя, только перепечаткой" + }, { "файл": "docs/glossary.md", "слово": "свидетель", diff --git a/docs/site/roadmap.ru.md b/docs/site/roadmap.ru.md index da923dc04..1c1018583 100644 --- a/docs/site/roadmap.ru.md +++ b/docs/site/roadmap.ru.md @@ -80,7 +80,7 @@ (`scripts/guards/traceability-guard.fscript`, задача 1407): постусловий 409, с примером 322, в записи 361, доказано 244; разрывов 62 и 68, храповиком. Перемер 4 октября 2026 тем же прогоном: постусловий 430, с примером 341, в записи 367, доказано 250; -оба числа разрывов стоят, и сторож разбирает их по родам — 58 из 62 приходятся на +оба числа разрывов стоят, и проверка разбирает их по родам — 58 из 62 приходятся на подделки, где недоказанность и есть требуемый итог, 4 честных и 1 не знает ни одна опись (задачи 7523, 7008); из 68 функций без постусловия 27 лежат в подделках, 41 — обычный код (задача 9008). Что внешний проверяющий перепроверит сам, по требованию на diff --git a/docs/tasks/1117-twenty-five-disabled-ci-jobs-run-locally.md b/docs/tasks/1117-twenty-five-disabled-ci-jobs-run-locally.md index c1a113dc8..5dfe880af 100644 --- a/docs/tasks/1117-twenty-five-disabled-ci-jobs-run-locally.md +++ b/docs/tasks/1117-twenty-five-disabled-ci-jobs-run-locally.md @@ -264,6 +264,249 @@ CI, ни короткая команда, ни хук, ни другой скр Задач на красные работы эта правка не заводит: её дело — назвать число и причину, а не починить. +## Перемер 4 октября 2026: пять самых дешёвых красных + +Дерево `dev` на коммите `5604556ef`, двоичный `bootstrap/flang` 0.7.23, машина та +же (256 ядер, часть прогонов шла под чужой нагрузкой — числа ниже это пол). +Мерено той же оснасткой: каждый шаг в своей подоболочке +`bash --noprofile --norc -e -o pipefail <тело шага>`, свои `RUNNER_TEMP`, +`GITHUB_OUTPUT`, `GITHUB_STEP_SUMMARY`, `GITHUB_ENV`, среда +`GITHUB_REF=refs/heads/dev`, `GITHUB_REF_TYPE=branch`, `GITHUB_EVENT_NAME=push`; +шаги идут по порядку и обрываются на первом красном. Сверх прошлого замера +разобрано и составное действие `./.github/actions/release-without-cache`: его +тело вынуто из `action.yml` и прогнано шагом, а не пропущено. Дерево после +каждой работы чисто (`git status --porcelain` пуст). + +Числа прошлого замера ниже не переписаны — они сняты на `85cc976a`, и ствол с +тех пор ушёл. + +| работа | было (2 октября) | перемерено 4 октября | чем стало | +|---|---|---|---| +| `zadachnik` / task-tracker | код 2, 0,3 с | **перемерено 4 октября: код 0, 94,0 с** (шаги 46,6 с + 47,4 с) | зелена без правки с моей стороны: оснастку шага починил `16729f7f9` 2 октября | +| `seed-verdicts` / seed-verdicts | код 1, 40,1 с | **перемерено 4 октября: код 0, 212,2 с** (95,5 + 96,0 + 10,5 + 10,2 с) | зелена: отпечаток семени называет живой коммит | +| `uncalled` / checks-nobody-calls | код 1, 17,1 с | **перемерено 4 октября: код 0, 19,2 с** (10,4 + 8,8 с) | зелена правкой этой ветки: пробе `kernel-memo` заведён зов | +| `neznanye-storozha` / uncalled-guards | код 1, 7,2 с до обрыва | **перемерено 4 октября: код 0, 722,5 с**, все 26 шагов проверки зелены, обрыва нет | зелена правкой этой ветки: словарь и жаргон закрыты, подлог шага 10 перебит на образец | +| `klyuchi` / cli-keys | код 1, 75,7 с | **перемерено 4 октября: код 0, 73,3 с** (36,7 + 36,6 с) | зелена без правки с моей стороны: ведомость долга поправил `f909a981f` 2 октября | + +### `seed-verdicts`: отказ судить кончился, и причина названа прогоном + +Прежняя краснота звалась «КОММИТ СЕМЕНИ НЕ ПРЕДОК HEAD: `b8aecf53`». Сегодня +отпечаток называет другой коммит, и он жив: + +``` +$ sed -n '7p' scripts/seed-fingerprint +коммит 843c429eb7011d717de9eb032279653cb4cf556c +$ git merge-base --is-ancestor 843c429eb7011d717de9eb032279653cb4cf556c HEAD + код 0 +$ git log -1 --format='%h %ad %s' --date=short 843c429eb +843c429eb 2026-10-04 fix(repl): the refusal names imported modules instead of denying a cause +``` + +Оба приговора отвечают кодом 0, а не 3: `proven:check` — 96,0 с, +`kernel-abilities:check` — 10,2 с. Пробы при них зелены, то есть подлог они +по-прежнему ловят и называют подложенное число. + +**ГРАБЛЯ ОСНАСТКИ, А НЕ ДЕРЕВА, и стоила она одного ложного красного.** Первый +мой заход этой работы дал код 1 за 38,5 с и сказал «ПОДЛОГ НЕ ПОКАЗАН». Причина +— в моём разборе YAML: `${{ runner.temp }}` подставлялось только в теле `run:`, +а в блоке `env:` шага оставалось текстом, и сторож отвечал +«mktemp: failed to create directory via template '${{ runner.temp }}/…'», то +есть кодом 3 «проверить не удалось». У всех четырёх шагов этой работы +`FLANG_TMP: ${{ runner.temp }}` стоит именно в `env:`. Кто будет мерить работы +этого файла руками — подставлять выражения обязан и в `env:`. + +### `neznanye-storozha`: три красных шага разобраны, все три зелены + +Шаг 14 «Probe uncalled guards» починен не здесь: перевёрнутое условие выправил +`16729f7f9` 2 октября, и сегодня он отвечает кодом 0 за 17,3 с. + +Шаг 5 «Check glossary» (`dictionary:check`) краснел так: «понятие «follows» есть +в таблице языка и не вписано ни в один раздел словаря» — код 1 за 3,4 с. Строку +понятия в `docs/glossary.md` вписали рукой 25 сентября (`5c640f2c2`), а список +разделов в `scripts/site/emit-dictionary.fscript`, из которого страница +печатается, о понятии не знал. Понятие вписано в раздел «Наследие прежней +поверхности» рядом с `therefore`, обещание длины списка поднято с 64 на 65. +Страницу пересобирать не пришлось: рукописная строка стоит ровно там, куда её +кладёт печать, и сверка сошлась знак в знак. После правки — код 0 за 4,7 с, +«словарь: чисто — docs/glossary.md сходится с таблицей, понятий 156». + +Шаг 9 «Check jargon» (`jargon:check`) краснел шестью бедами, а не пятью: к +четырём страницам курса и руководства добавилась `docs/site/roadmap.ru.md` +(внутренних слов 5 при дозволенных 4). Код 1 за 196,3 с, пик 3,57 ГиБ. Беды +двух родов, и починены они по-разному: + +* **проза для читателя, шесть строк в пяти файлах** — слово заменено на внешнее: + «сторож» → «проверка» (`docs/site/roadmap.ru.md:83`, + `docs/course/03-totality.md:104`, `docs/guide/how-to-write-flang.ru.md:44`), + «корпус» → «программы репозитория» (`docs/course/03-totality.md:105`, + `docs/course/13-where-next.md:112`), «печатник» → «генератор кода» + (`docs/course/09-eight-targets.md:280`). +* **имена функций на flang, две строки в `flang/src/emit/c/flang_repl.c`** — + `repl_call("Каталоги мимо корпуса")` и `repl_call("Отбор корпуса")`, то есть + `flang/self/bootstrap/corpus.flang:270` и `:334`. Это не проза: переименовать + их текстовым запретом нельзя, только перепечаткой. Записаны в раздел + «исключения» файла `docs/jargon.json` — той же породой и тем же доводом, что + уже лежащий там `repl_call("Свести корпус")`. Долг файла остался 42, расти ему + правило не даёт. + +После правки — код 0 за 200,7 с, «внутренних слов 992 (долг по 34 файлам, расти +не имеет права), новых 0». + +**ЧЕТВЁРТЫЙ КРАСНЫЙ ШАГ, КОТОРОГО В ПРОШЛОМ ЗАМЕРЕ НЕ БЫЛО.** Шаг 10 «Probe +length claims» — код 1 за 0,0 с, «ПОДЛОГ НЕ СОБРАЛСЯ: строка 75 +flang/self/emit-rust.flang уже не та». Обещание «бэкенд занимает ровно пять +имён» съехало со строки 75 на строку 20, и `sed`, прибитый к номеру, смолчал. +Это ровно та грабля, о которой предупреждает шаг «Probe blockers table» двумя +шагами выше («номер 40 съехал на 42»). Подлог перебит на образец самой строки, +в файле он однозначен; сообщение о несобравшемся подлоге теперь называет +обещание, а не номер. После правки — код 0 за 96,0 с. + +Шагов работы 29, из них `uses:` два и `make` один. Все 26 шагов проверки зелены, +и работа доходит до конца: код 0 за 722,5 с. Самые дорогие — «Check jargon» +200,7 с, «Probe jargon guard» 195,3 с, «Probe length claims» 96,0 с, «Check +length claims» 80,4 с. + +### `uncalled`: пробе `kernel-memo` заведён зов, и она зелена + +Прежняя жалоба: «НОВАЯ ПРОВЕРКА БЕЗ ЗОВА: +`flang/proof/probes/kernel-memo/run.fscript`». Сама проба **сегодня зелена**, и +запись задачи 5310 от 2 октября («код 1 за 306,7 с, KERNEL MEMO CHANGES THE +ANSWER») больше не действует — обёртки памяти вызовов доехали в семя: + +``` +$ cd flang/proof/probes/kernel-memo && ../../../../bootstrap/flang io run.fscript +kernel memo: runs 6, memo on and audit answer byte for byte as memo off + код 0 за 175,5 с, пик 0,36 ГиБ +``` + +Поэтому выбран зов, а не запись в ведомость: ярлык `script.kernel-memo:probe` в +`.flangrc` рядом с сестринским `plan-rules:probe`, и шаг «Check kernel memo does +not change the answer» в работе `storozha` файла `binary.yml` — там, где стоят +все двадцать её сестёр из `flang/proof/probes/**`. `ci.yml` для зова не годится: +он выключен, и зов в нём не звал бы никого. + +**ЦЕНА НАЗВАНА, И ОДНО ЧИСЛО НЕ МЕРЕНО.** Работа `storozha` на раннере идёт +6 мин 47 с и 7 мин 01 с (заходы 37223001273 и 37223864296). Сколько к ней +прибавят 175,5 с с этой машины — **не мерил: работу на раннере я не запускал**, +а один поток `check --proof` на двухъядерном раннере идёт не с этой скоростью. + +На место `kernel-memo` в списке незваных встала другая проверка — +`flang/proof/probes/text-block/tokens.fscript`, пришедшая с правкой лексера +(ADR-0052) и зова не получившая. Ей зов не заведён, и довод числом: без +`--max-steps` она вердикта не даёт вовсе (код 3 за 78,9 с, «функция «Склеить» +исчерпала лимит шагов»), а с выборкой дорожает не линейно по размеру файла — на +файле 394 байта код 0 за 5,9 с, тогда как ADR-0052 называет 9 мин 29 с на один +файл 106 КБ и 78 мин на выборку из десяти (эти два числа взяты со страницы +решения, здесь не мерены). Зов на одном крошечном файле был бы проверкой, +которая не проверяет, поэтому она вписана в +`scripts/ledgers/checks-nobody-calls.tsv` с этим доводом. Разбор — в задаче +5310. + +После правки работа зелена: код 0 за 19,2 с, «проверок в дереве 104, без зова 8, +все названы в ведомости — сходится». + +### `klyuchi` и `zadachnik`: зелены без правки, и это надо было проверить, а не предположить + +Обе починены стволом 2 октября, и обе я только перемерил. + +`klyuchi` — код 0 за 73,3 с: «эталон flang/self/cli.flang: ключей 39, разбор C +2 файла: ключей 67, двоичный (прогоном): ключей в справке 66 … НАБОРЫ СОШЛИСЬ: +ни одного расхождения сверх записанного долга». Пятерых незнакомцев +(`--memory-limit`, `--step-limit`, `--timeout`, `--предел-памяти`, +`--предел-шагов`) закрыл `f909a981f`: расхождение было **со стороны ведомости**, +а не дерева — ключи у двоичного есть все пять, и ведомость о них либо не знала, +либо утверждала то, что перестало быть правдой. + +Отличать «ключ ждёт перепечатки» от «ключ забыт» сторож **умеет уже сегодня**, и +учить его этому нечем: разряды ведомости — это и есть различение, а довод каждой +записи называет срок. Все пять записей о незнакомцах говорят «долг закроется +перепечаткой семени и правкой `flang/self/cli.flang`», и ни одна не говорит +«забыт». Остаток — не в наборах, а в ЧТЕНИИ стороны C: три ветви +`flang/src/emit/c/flang_cli.c` сравнивают местную копию довода, и сторож их +числовой разряд читает неверно. Это задача 3787, и она уже заведена. + +`zadachnik` — код 0 за 94,0 с: шаг «Probe task tracker» разбирается оболочкой +(`bash -n` код 0), подлог собирается, сторож краснеет на нём и называет и файл, +и подложенное слово; «Check task tracker» отвечает «задачник цел: всего задач +194: свободно 181, в работе 7, сделано 6, отклонено 0». + +### Отрицательные контроли: шесть, и каждый красен + +Правка без отрицательного контроля ничего не доказывает, поэтому к каждой +починке сломано ровно то, что она стережёт: + +| что сломано | чем обязано кончиться | кончилось | +|---|---|---| +| `zadachnik`: у одного `if` в теле шага снят `fi` | шаг не разбирается | код 2, 0,0 с, «syntax error: unexpected end of file from `if` command on line 11» | +| `zadachnik`: `sed` подлога переделан в пустую операцию | «подлог не собрался» | код 1, 0,0 с, имя файла названо | +| словарь: `follows` снят из раздела | `dictionary:check` краснеет | код 1, прежнее сообщение слово в слово | +| `uncalled`: сняты оба зова `kernel-memo` (ярлык и шаг) | «НОВАЯ ПРОВЕРКА БЕЗ ЗОВА» | код 1, имя пробы названо | +| шаг 10: образец подлога заменён на отсутствующий в файле | «подлог не собрался» | код 1, 0,0 с, обещание названо | +| `klyuchi`, `seed-verdicts`, шаги 8 и 14 | пробы этих работ подлог кладут сами | все четыре пробы зелены, то есть сторожа на подлоге краснеют | + +### Что из семи красных осталось красным + +**Две, и ни одна не из этих пяти.** `links` — признанный долг, работа помечена +`continue-on-error: true` и ни тега, ни пуша не держит. `stale-pages` — страницы +`docs/course/**` объявляют 0.7.22 при 0.7.23, и работа идёт только по метке и по +кнопке. Обе перемера здесь не получили: `links` — 250,9 с, `stale-pages` — +1309,6 с по прошлому замеру, и **не мерил: в мою долю они не входили**. + +Из шести работ пуша, что блокировали, осталась **ни одна**: `zadachnik`, +`klyuchi`, `neznanye-storozha`, `seed-verdicts` и `uncalled` зелены, а `links` +не блокирует. Включать CI это решение не принимает — `stale-pages` на метке +по-прежнему красна. + +### Перемер того же дня после переноса на ушедший ствол + +Ствол за время работы ушёл на 16 коммитов, ветка перенесена на `4d76abd53`, и +среди тех 16 стоит пересев семени (`d26780ea8`): двоичный собран заново и стал +**0.7.24**. Все пять работ прогнаны ещё раз на этом дереве — числа ниже сняты +им, а числа выше остаются при дереве `5604556ef` и двоичном 0.7.23. + +| работа | на `5604556ef`, 0.7.23 | на `4d76abd53` + ветка, 0.7.24 | +|---|---|---| +| `zadachnik` | код 0, 94,0 с | код 0, **105,9 с** | +| `seed-verdicts` | код 0, 212,2 с | код 0, **249,6 с** | +| `uncalled` | код 0, 19,2 с | код 0, **19,1 с**, «проверок в дереве 105, без зова 8» | +| `klyuchi` | код 0, 73,3 с | код 0, **73,4 с** | +| `neznanye-storozha` | код 0, 722,5 с, 26 шагов из 26 | **код 1, 397,0 с**, обрыв на шаге 9 | + +**Четыре работы из пяти зелены и на новом дереве.** Пятая снова красна, и +причина пришла со стволом, а не отсюда. + +**ПОПРАВКА К МОЕЙ ЖЕ ЗАПИСИ ВЫШЕ про `seed-verdicts`, и она важнее разницы в +секундах.** Выше я написал, что работа зелена потому, что отпечаток называет +живой коммит и `git merge-base --is-ancestor` отвечает кодом 0. **Это неверный +довод.** На новом дереве отпечаток называет `a1102df50`, и предком `HEAD` он НЕ +является (`git merge-base --is-ancestor` → код 1: пересев печатался в чужом +ряду, который при переносе стал `d5a0a470`), — а работа всё равно зелена, код 0. +Судит сторож не по родству коммитов, а по хешам входов печати, и говорит это +сам: «семя не отстало от исходников: proven:check». Родство коммитов он называет +лишь объяснением, когда хеши разошлись. Проверять надо прогоном сторожа, а не +`merge-base`. + +**Почему `neznanye-storozha` снова красна.** Шаг 9 «Check jargon» — код 1 за +202,9 с, бед четыре, и все четыре новые: `docs/site/registry.md` (внутренних +слов 10 при дозволенных 0), `docs/site/registry.ru.md` (9), +`docs/site/packages.md` (1), `docs/site/packages.ru.md` (1). Страницы пришли +коммитом `ffeca8f82` «feat(site): the registry page is printed from the ledger» +и **печатаются** (`scripts/site/registry-page.fscript`) — руками их не +поправить, правка нужна в печатнике. Ни одна из шести бед, закрытых этой +веткой, не вернулась. Разбор и числа — задача **2325**, туда же и «когда +сделана». + +Остальные 27 шагов проверки зелены, и это снято **по-шагово** (759,9 с +суммарно), а не обрывом: шагов в работе стало 31, прибавилась пара «Probe/Check +guards without forgery probe» (15,4 и 16,2 с, обе зелены). Мои две починки этой +работы держатся и на новом дереве: шаг 5 «Check glossary» — код 0 за 4,7 с, шаг +10 «Probe length claims» — код 0 за 96,5 с. + +Проба `kernel-memo` на двоичном 0.7.24 — код 0 за **177,4 с**, пик 0,36 ГиБ, тот +же ответ знак в знак («kernel memo: runs 6, memo on and audit answer byte for +byte as memo off»). В пометке шага `binary.yml` стоит число с 0.7.23 (175,5 с); +разница в 1,9 с — шум машины под чужой нагрузкой, а не правка. + ## Что должно быть У каждой работы `ci.yml` и `target-twins.yml` известен исход на нынешнем diff --git a/docs/tasks/2325-the-registry-page-is-printed-with-internal-words.md b/docs/tasks/2325-the-registry-page-is-printed-with-internal-words.md new file mode 100644 index 000000000..9828b5eeb --- /dev/null +++ b/docs/tasks/2325-the-registry-page-is-printed-with-internal-words.md @@ -0,0 +1,87 @@ +--- +номер: 2325 +заголовок: Страница реестра печатается с внутренними словами, и работа uncalled-guards от этого красна +статус: свободна +приоритет: P2 +исполнитель: — +ветка: — +команда: вторая +карта: Что мешает больше всего +рядом: 1117, 5310 +нужность: сторож жаргона краснеет на четырёх страницах сайта, и правка нужна в печатнике, а не на страницах — руками их не поправить +--- + +# 2325. Страница реестра печатается с внутренними словами + +## Шаги воспроизведения + +1. Прогнать сторожа жаргона на нынешнем стволе: + +``` +bootstrap/flang run-script jargon:check +``` + +2. Смотреть беды и имена страниц. + +## Что происходит + +``` +$ bootstrap/flang run-script jargon:check +Сторож жаргона ОТКАЗЫВАЕТ. Беды: + · docs/site/packages.md: внутренних слов 1, дозволено 0. Лишние: + строка 5: «ledger» → the proof report + · docs/site/packages.ru.md: внутренних слов 1, дозволено 0. Лишние: + строка 4: «ведомост» → отчёт о доказательствах + · docs/site/registry.md: внутренних слов 10, дозволено 0. Лишние: + строка 3: «ledger» (дважды), 7, 12, 27, 43, 49, 63, 74: «ledger» + строка 29: «byte for byte» → compared byte for byte — say it in words + · docs/site/registry.ru.md: внутренних слов 9, дозволено 0. Лишние: + строки 3 (дважды), 6, 11, 26, 42, 48, 62, 73: «ведомост» + +всего бед: 4 код 1 за 195,1 с +``` + +Версия: flang 0.7.24. Дата прогона: 4 октября 2026, ствол `4d76abd53`. + +Четыре страницы пришли коммитом `ffeca8f82` «feat(site): the registry page is +printed from the ledger». Руками их не поправить: `docs/site/registry.md` и +`registry.ru.md` **печатаются** — печатник `scripts/site/registry-page.fscript`, +и внутренние слова стоят в его тексте. У страниц `packages.md` и +`packages.ru.md` дозволено 0, и прибавка по одному слову в каждой тоже новая. + +Из-за этого работа `neznanye-storozha` / uncalled-guards выключенного `ci.yml` +снова обрывается — теперь на шаге 9 «Check jargon»: код 1 за 195,1 с, и +двадцать шагов после него в CI не видны. До этой прибавки работа доходила до +конца: код 0 за 722,5 с, все 26 шагов проверки зелены (замер 4 октября 2026 на +дереве `5604556ef`, задача 1117). + +## Что должно быть + +`jargon:check` отвечает кодом 0. Слово «ведомость»/«ledger» на странице для +читателя заменено внешним — сторож подсказывает «отчёт о доказательствах» / «the +proof report», — а «byte for byte» сказано словами. Правка идёт в печатник, и +страницы пересобираются им же, а не правятся поверх: правку страницы затрёт +следующая сборка. + +## Обходной путь + +Нет. Долг страницы можно было бы вписать в `docs/jargon.json`, но это не обход, +а глушение: слово стоит в прозе для читателя, а не в имени функции, и запрет +назван именно для такой прозы. + +## Когда задача сделана + +``` +bootstrap/flang run-script jargon:check код 0 +``` + +и работа `neznanye-storozha` доходит до конца — все 26 шагов проверки зелены. +Проба, которая краснеет, если беда вернётся, уже стоит: шаг 8 «Probe jargon +guard» той же работы дописывает внутреннее слово в `CONTRIBUTING.md` и требует +от сторожа красноты (код 0 за 186,8 с на том же дереве). + +## Где живёт правка + +`scripts/site/registry-page.fscript` (печатник), `docs/site/packages.md` и +`docs/site/packages.ru.md`, и пересобранные им `docs/site/registry.md` и +`docs/site/registry.ru.md`. Перепечатка семени не нужна. diff --git a/docs/tasks/5310-a-check-nobody-calls-goes-red.md b/docs/tasks/5310-a-check-nobody-calls-goes-red.md index 03e4ad707..e62da2988 100644 --- a/docs/tasks/5310-a-check-nobody-calls-goes-red.md +++ b/docs/tasks/5310-a-check-nobody-calls-goes-red.md @@ -81,6 +81,65 @@ scripts/guards/seed-parses-sources-guard.fscript Звать каждую из восьми руками; команды записаны в ведомости. +## Перемер 4 октября 2026: `kernel-memo` позвана, на её место пришла другая + +Дерево `dev` на коммите `5604556ef`, двоичный `bootstrap/flang` 0.7.23, машина +256 ядер под чужой нагрузкой. + +Проба `flang/proof/probes/kernel-memo/run.fscript` **сегодня зелена**, и прежняя +запись этой задачи — «код 1 за 306,7 с, KERNEL MEMO CHANGES THE ANSWER» — больше +не действует: обёртки памяти вызовов доехали в семя. Свои прогоны: + +``` +$ cd flang/proof/probes/kernel-memo && ../../../../bootstrap/flang io run.fscript +kernel memo: runs 6, memo on and audit answer byte for byte as memo off + код 0 за 175,5 с, пик 0,36 ГиБ +$ … то же с --на-веру + код 0 за 175,5 с, пик 0,36 ГиБ +``` + +Поэтому она **позвана**, а не вписана в ведомость: ярлык +`script.kernel-memo:probe` в `.flangrc` и шаг «Check kernel memo does not change +the answer» в работе `storozha` файла `binary.yml` — там, где стоят все её +сёстры из `flang/proof/probes/**`. Работа `storozha` на раннере идёт 6 мин 47 с +и 7 мин 01 с (заходы 37223001273 и 37223864296); цена пробы НА РАННЕРЕ не +мерена — 175,5 с снято на этой машине. + +Работа `checks-nobody-calls` выключенного `ci.yml` после этого **зелена**: код 0 +за 19,2 с, «проверок в дереве 104, без зова 8, все названы в ведомости — +сходится». + +### Восьмая незваная теперь другая: `flang/proof/probes/text-block/tokens.fscript` + +Перепись на том же дереве: + +``` +$ bootstrap/flang io scripts/guards/checks-nobody-calls.fscript --plan Перепись --max-steps 4000000000 + проверок в дереве 104 + зовут 96 + НЕ ЗОВУТ 8 код 0 +``` + +Проверок в дереве стало 104 вместо 98, и в списке незваных вместо `kernel-memo` +встала `flang/proof/probes/text-block/tokens.fscript` — она пришла с правкой +лексера (`b5c40394e`, ADR-0052) и зова не получила. Её прогоны 4 октября: + +``` +$ bootstrap/flang io flang/proof/probes/text-block/tokens.fscript --plan Tokens --на-веру +функция «Склеить» исчерпала лимит шагов (10000000) код 3 за 78,9 с, пик 3,01 ГиБ +$ … --max-steps 4000000000 -- docs/examples/guide/exact-money.flang (394 байта) +text-block: файлов 1, поток токенов разошёлся у 0 код 0 за 5,9 с, пик 0,36 ГиБ +``` + +Без `--max-steps` она вердикта не даёт вовсе, а цена растёт по размеру файла не +линейно: ADR-0052 называет 9 мин 29 с на один файл 106 КБ и 78 мин на выборку из +десяти, всё дерево — около 50 часов оценкой (эти три числа здесь НЕ мерены, +взяты со страницы решения). Зов на одном крошечном файле был бы проверкой, +которая не проверяет, поэтому она вписана в ведомость с этим доводом, а не +позвана. Чтобы её позвать, нужна выборка, дающая вердикт за разумное время. + +Итог переписи: незваных по-прежнему восемь, и все восемь названы в ведомости. + ## Когда задача сделана 1. План «Проверка» отвечает кодом 0: `kernel-memo` либо позвана, либо вписана в diff --git a/scripts/ledgers/checks-nobody-calls.tsv b/scripts/ledgers/checks-nobody-calls.tsv index 6308c26ad..de89db0d8 100644 --- a/scripts/ledgers/checks-nobody-calls.tsv +++ b/scripts/ledgers/checks-nobody-calls.tsv @@ -1,5 +1,6 @@ check reason flang/proof/probes/screen/run.fscript ЗЕЛЕНА и не дёшева, тихий долг. Свой прогон 27 сентября 2026 (`cd flang/proof/probes/screen && ../../../../bootstrap/flang io run.fscript --на-веру`): код 0 за 53 с, «пробы экрана: сошлось 22 из 22». В binary.yml шагом стоит ТОЛЬКО сосед screen-size (строка 1785); про «screen» разбор задачи 5309 от 26 сентября говорит, будто он там есть, — это неправда, снято грепом по binary.yml: имя «screen» встречается один раз, и то как «screen-size». +flang/proof/probes/text-block/tokens.fscript ПРИБОР ДЛЯ ПРАВКИ ЛЕКСЕРА, а не ворота, и дорога не линейно по размеру файла. Сверяет поток токенов «исходник flang/self/lexer.flang под интерпретатором» против «лексер, зашитый в семя» (ADR-0052); выборку файлов берёт доводами после «--». Свои прогоны 4 октября 2026 на дереве 5604556ef, двоичный 0.7.23: без доводов (`bootstrap/flang io flang/proof/probes/text-block/tokens.fscript --plan Tokens --на-веру`) — код 3 за 78,9 с, пик 3,01 ГиБ, «функция «Склеить» исчерпала лимит шагов (10000000)»: без `--max-steps` проба вердикта не даёт вовсе; на одном файле 394 байта (`--max-steps 4000000000 -- docs/examples/guide/exact-money.flang`) — код 0 за 5,9 с, пик 0,36 ГиБ, «файлов 1, поток токенов разошёлся у 0». ЦЕНА БОЛЬШОЙ ВЫБОРКИ НЕ МЕРЕНА ЗДЕСЬ: ADR-0052 называет 9 мин 29 с на один файл 106 КБ и 78 мин на выборку из десяти, всё дерево — около 50 часов оценкой. Зов на одном крошечном файле был бы проверкой, которая не проверяет: в CI её ставить нечем, пока сверка не идёт по названной выборке за разумное время. Задача 1310 рядом: всё дерево сверяет перепечатка. flang/scripts/count-guard.fscript КРАСНА по делу и ДОРОГА. Свой прогон 27 сентября 2026 на gh/dev 5190e4708 (`bootstrap/flang io flang/scripts/count-guard.fscript --на-веру --max-steps 2000000000`): код 1 за 562 с, «9 числ(о/а) прозы разошлись с деревом» — FL_MAX_STEPS сказано 1400000000000, измерено 4000000000000 в четырёх файлах; цена шага печати сказано 456857834234, измерено 2412102536357. Тот же ответ дал прогон на прежней базе 1043ff82a за 491 с. Ставить в CI нельзя, пока долг не закрыт. Двойник на JavaScript flang/scripts/count-guard.mjs зовут ярлыком «counts:check», и в соседней ведомости uncalled-guards.json он числится красным и очень дорогим (6884 с). flang/scripts/direct-run-guard.fscript КРАСНА по делу и ДОРОГА. Свой прогон 27 сентября 2026 на gh/dev 5190e4708 (`bootstrap/flang io flang/scripts/direct-run-guard.fscript --на-веру`): код 1 за 422 с; тот же ответ на прежней базе за 437 с. Беда: свои копии «запущен ли я напрямую» вместо ввоза образца — flang/src/emit/js/flang_host_node.js:505 и напечатанные flang_cli.js трёх примеров-каркасов в docs/examples/frameworks/. Ни одного зова в дереве нет вовсе: единственное упоминание — пояснение в .github/workflows/ci.yml, и это строка-комментарий, а не вызов. flang/scripts/name-guard.fscript КРАСНА по делу и ОЧЕНЬ ДОРОГА. Свой прогон 27 сентября 2026 на базе 1043ff82a (`cd flang/scripts && FLANG_NAME_GUARD_JOB=$T FLANG_NAME_GUARD_MODE='проверка' ../../bootstrap/flang io name-guard.fscript --plan 'Выписать имена' --max-steps 2000000000`): план дописал отчёт за 1327 с и вышел кодом 0, а вердикт лежит в файле $T/итог, и там первое слово — «красный»: «Сторож имён: 328 файлов, 4877 мест долга в 210 файлах» (Р1-одна-буква 2739, Р2-короче-трёх 702, Р3-обрубок 1623, Р4-две-письменности 1, Р5-длинное-имя 3, Р6-длинный-пример 3). Код плана 0 здесь НЕ значит «зелена»: план пишет отчёт, а судит план «Имена в порядке», и его не гоняли — 22 минуты на заход. ПЕРЕМЕР на свежей базе 5190e4708 НЕ СНЯТ: прогон убит сигналом 9 на 7,7 ГиБ через 64 с, когда рядом шли два других тяжёлых замера; это цена машины, а не ответ сторожа. Двойник на JavaScript flang/scripts/name-guard.mjs зовут ярлыком «names:check», и по соседней ведомости uncalled-guards.json он красен за 584 с. diff --git a/scripts/site/emit-dictionary.fscript b/scripts/site/emit-dictionary.fscript index d5aa2e0ee..e8a9067ab 100644 --- a/scripts/site/emit-dictionary.fscript +++ b/scripts/site/emit-dictionary.fscript @@ -265,7 +265,7 @@ тотальная функция «Понятия наследия» возвращает список строки - обеспечивает «длина постоянного списка — Понятия наследия» (длина результат) равен 64 + обеспечивает «длина постоянного списка — Понятия наследия» (длина результат) равен 65 пример «Постоянная Понятия наследия списана из тела знак в знак» ожидается [ "utility|объявляет исполняемую утилиту", "rule|объявляет правило утилиты", "property|свойство в правиле", "result|результат правила", "startsWith|начальное значение правила", @@ -284,7 +284,9 @@ "morphismPair|пара морфизмов бифунктора", "proposition|объявляет утверждение о поведении", "has|утверждает наличие поля или свойства", "inData|уточняет, что поиск идёт в данных", "findWhere|поиск по условию", "byMorphism|указывает морфизм, по которому идёт действие", - "therefore|вывод шага доказательства", "law|ссылается на закон в доказательстве", + "therefore|вывод шага доказательства", + "follows|силлогизм: вывод утверждения из посылок, названных выше", + "law|ссылается на закон в доказательстве", "mapsTo|образ объекта под функтором", "mapsToField|образ поля под функтором", "mapsToMorphism|образ морфизма под функтором", "requires|предусловие функции", "ensures|постусловие функции — то, что доказывает ядро", "forall|квантор всеобщности в утверждении", @@ -336,6 +338,7 @@ "findWhere|поиск по условию", "byMorphism|указывает морфизм, по которому идёт действие", "therefore|вывод шага доказательства", + "follows|силлогизм: вывод утверждения из посылок, названных выше", "law|ссылается на закон в доказательстве", "mapsTo|образ объекта под функтором", "mapsToField|образ поля под функтором",