Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions .github/workflows/binary.yml
Original file line number Diff line number Diff line change
Expand Up @@ -393,9 +393,9 @@ jobs:
#
# Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md,
# docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН
# язык: JavaScript. Оболочка (94 файлов, 23379 строк), HTML, CSS, пробы на
# язык: JavaScript. Оболочка (94 файлов, 23404 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-23 файлов *.sh = 94 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-24 строк-в *.sh = 23379 (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 23372, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 23980, снято 2026-09-22) (ADR-0046: довод в шапках двух сторожей имён — сперва почему flang/proof не судится, потом почему вошёл в область — прибавил 9 строк; до него 23971, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 23404 (задача 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 не считались нигде и ни в одной проверке. Долг,
# которого никто не считает, не убывает: его не видно ни в отчёте, ни в
# ленте, и растёт он молча.
Expand Down
15 changes: 15 additions & 0 deletions .github/workflows/provability.yml
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,21 @@ jobs:
name: provability
runs-on: ubuntu-latest
timeout-minutes: 45
# FLANG_TMP НА ВСЮ РАБОТУ, а не по шагам. Прогон набора проб чекера
# (flang/proof/checker/tests/run.sh, его зовёт scripts/доказуемость.sh)
# берёт времянку как `mktemp -d -p "${FLANG_TMP:-/srv/tmp}"`. На раннере
# каталога /srv/tmp нет, mktemp падает, и при `set -eu` прогон кончается
# НЕМЕДЛЕННО кодом 1, не напечатав ни одной строки итога. Вердикт читает
# итог разбором строк, не находит их — и печатает «проб на подлог 0» при
# храповике 533, то есть красное, которое выглядит как ослабший набор, а
# на деле значит «ничего не проверялось».
#
# Так и было: работа краснела КАЖДЫЙ ДЕНЬ с 18 по 24 сентября 2026 (семь
# прогонов подряд), и все семь раз по этой причине. Переменную здесь просто
# забыли: ci.yml задаёт её 10 раз, binary.yml 17, reprint.yml 8 — и все по
# шагам, откуда её и можно забыть. Здесь она на работе целиком.
env:
FLANG_TMP: ${{ runner.temp }}
steps:
- uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
- name: Build bootstrap
Expand Down
2 changes: 1 addition & 1 deletion docs/site/cli.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ were, and 3 of the 5 had drifted — two `io` runs now exit `3` instead of `0`
(an unproved plan is refused by default, ADR-0045) and the shortcut count in the
`Целость` output moved from 102 to 147. All three are corrected below, together
with the `io` usage line, its key table and its permission list. The remaining
16 examples are written against a fictional `привет.flang` that this tree does
16 examples are written against a fictional привет.flang that this tree does
not contain: they cannot be re-run at all and still rest on the 11 September
check. Task 7731 is about closing that.

Expand Down
2 changes: 1 addition & 1 deletion docs/site/cli.ru.md
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
`0` (недоказанный план по умолчанию не исполняется, ADR-0045), а число ярлыков в
выводе плана «Целость» выросло со 102 до 147. Все три поправлены ниже — вместе
со строкой вызова `io`, таблицей её ключей и списком полномочий. Остальные 16
примеров написаны на выдуманном `привет.flang`, которого в дереве нет: прогнать
примеров написаны на выдуманном привет.flang, которого в дереве нет: прогнать
их нельзя вовсе, и они по-прежнему стоят на сверке 11 сентября. Об этом — задача
7731.

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@

Двоичный в дереве — 0.7.21, собран из `90249e71f`. Примеров вида `$ flang …` на
странице 21. Из них **5 называют настоящие файлы дерева** и поддаются прогону;
остальные 16 написаны на выдуманном `привет.flang`, которого в дереве нет.
остальные 16 написаны на выдуманном привет.flang, которого в дереве нет.

Прогнаны все пять. Разошлись три:

Expand Down Expand Up @@ -52,8 +52,8 @@
## Что делать

**1. Дать странице настоящий входной файл.** Шестнадцать примеров стоят на
`привет.flang`, которого нет. Положить его (и `плохо.flang`, `план.flang`,
`факты.json`) в `docs/site/examples/` — тогда прогоняемыми станут все 21.
привет.flang, которого нет. Положить его (и плохо.flang, план.flang,
факты.json) в `docs/site/examples/` — тогда прогоняемыми станут все 21.

**2. Снимать примеры прогоном, а не рукой.** Проверка читает из страницы блоки
` ```bash `, берёт строки `$ flang …`, зовёт двоичный, сверяет вывод и код с
Expand Down
2 changes: 1 addition & 1 deletion docs/tree-inventory.md
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ $ bootstrap/flang io scripts/guards/tree-inventory.fscript --max-steps 50000000

| язык | файлов | строк | долг файлов | долг строк |
|---|---:|---:|---:|---:|
| оболочка | 99 | 24 048 | 87 | 15 480 <!-- СНЯТО 2026-09-24 долг файлов/строк оболочки = 87/15480 (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 87/15462, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 94/16157, снято 2026-09-17) (ADR-0046: довод двух сторожей имён прибавил 5 строк; до него 94/16148, снято 2026-09-17) (задача 1430: записанный довод области сторожа транслита прибавил 57 строк в scripts/guards/translit-file-names-guard.sh; до него 93/15982, снято 2026-09-17) (задача 5502: набор проб строгого режима завёл flang/proof/probes/strict/run.sh, 105 строк; до него 90/15560) (задача 1794: подделка тела К1 прибавила 7 строк в flang/proof/checker/tests/run.sh, вне долга) (ADR-0042, задачи 6432 и 6812: семейства Пр и М прибавили 2 строки в flang/proof/tables-guard.sh; до них 87/15959) (на ветке a/1418-three-moves: обходчик проверок flang/test/обход.sh прибавил 7 строк, задача 1418; на стволе 87/15952), планом «Опись дерева по языкам» (задачи 5332 и 6438 прибавили 42 строки в flang/proof/checker/tests/run.sh и flang/proof/corpus-share.sh, из них долга 14; до них 87/15916) (пары «строка ↔ лемма» в flang/proof/lean/run.sh, задачи 3855 и 1130, прибавили 17 строк; до них 87/15899, снято 2026-09-14) (сверка вердиктов C ↔ Lean, задача 2907, прибавила 152 строки в flang/proof/lean/run.sh; до неё 87/15747, снято 2026-09-12) на стволе 24e6edb34 со слитой уборкой дерева (учебник прибавил 37 строк в scripts/flangtutor-proba.sh, хук — 5 строк в .githooks/pre-push; до них на 4e9a7a8c3 было 102/16682) (8 сентября было 98/15001: задача 3127 завела scripts/module-origin-guard.sh, 277 строк) --><!-- СНЯТО 2026-09-23 файлов *.sh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 99 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 106, снято 2026-09-17) --><!-- СНЯТО 2026-09-24 строк-в *.sh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 24048 (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 24025, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 24629, снято 2026-09-22) (ADR-0046: довод двух сторожей имён прибавил 9 строк; до него 24620, снято 2026-09-17) (задача 1430: записанный довод области сторожа транслита прибавил 57 строк в scripts/guards/translit-file-names-guard.sh; до него 24454, снято 2026-09-17) --> |
| оболочка | 99 | 24 073 | 87 | 15 505 <!-- СНЯТО 2026-09-17 долг файлов/строк оболочки = 87/15505 (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 87/15462, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 94/16157, снято 2026-09-17) (ADR-0046: довод двух сторожей имён прибавил 5 строк; до него 94/16148, снято 2026-09-17) (задача 1430: записанный довод области сторожа транслита прибавил 57 строк в scripts/guards/translit-file-names-guard.sh; до него 93/15982, снято 2026-09-17) (задача 5502: набор проб строгого режима завёл flang/proof/probes/strict/run.sh, 105 строк; до него 90/15560) (задача 1794: подделка тела К1 прибавила 7 строк в flang/proof/checker/tests/run.sh, вне долга) (ADR-0042, задачи 6432 и 6812: семейства Пр и М прибавили 2 строки в flang/proof/tables-guard.sh; до них 87/15959) (на ветке a/1418-three-moves: обходчик проверок flang/test/обход.sh прибавил 7 строк, задача 1418; на стволе 87/15952), планом «Опись дерева по языкам» (задачи 5332 и 6438 прибавили 42 строки в flang/proof/checker/tests/run.sh и flang/proof/corpus-share.sh, из них долга 14; до них 87/15916) (пары «строка ↔ лемма» в flang/proof/lean/run.sh, задачи 3855 и 1130, прибавили 17 строк; до них 87/15899, снято 2026-09-14) (сверка вердиктов C ↔ Lean, задача 2907, прибавила 152 строки в flang/proof/lean/run.sh; до неё 87/15747, снято 2026-09-12) на стволе 24e6edb34 со слитой уборкой дерева (учебник прибавил 37 строк в scripts/flangtutor-proba.sh, хук — 5 строк в .githooks/pre-push; до них на 4e9a7a8c3 было 102/16682) (8 сентября было 98/15001: задача 3127 завела scripts/module-origin-guard.sh, 277 строк) --><!-- СНЯТО 2026-09-23 файлов *.sh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 99 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 106, снято 2026-09-17) --><!-- СНЯТО 2026-09-17 строк-в *.sh,ярлык,packaging/asdf/bin/download,packaging/asdf/bin/install,packaging/asdf/bin/list-all,.githooks/pre-push = 24073 (задача 1416: четырнадцать объявлений ярлыков заведены в скриптах и зов «Сбора» — в хуке; до них 24025, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 24629, снято 2026-09-22) (ADR-0046: довод двух сторожей имён прибавил 9 строк; до него 24620, снято 2026-09-17) (задача 1430: записанный довод области сторожа транслита прибавил 57 строк в scripts/guards/translit-file-names-guard.sh; до него 24454, снято 2026-09-17) --> |
| C | 36 | 859 589 | 0 | 0 <!-- СНЯТО 2026-09-19 файлов *.c,*.h = 36 --><!-- СНЯТО 2026-09-17 строк-в *.c,*.h = 859589 (задача 5502: четыре исхода строгого режима прибавили по 68 строк в каждый из близнецов flang_repl.c; до неё 859487) --> |
| C++ | 1 | 404 | 0 | 0 <!-- СНЯТО 2026-09-05 файлов *.cpp,*.cc,*.hpp,*.hh = 1 --><!-- СНЯТО 2026-09-05 строк-в *.cpp,*.cc,*.hpp,*.hh = 404 --> |
| Python | 16 | 6 029 | 10 | 2 880 <!-- СНЯТО 2026-09-11 файлов *.py = 16 --><!-- СНЯТО 2026-09-11 строк-в *.py = 6029 --> |
Expand Down
29 changes: 27 additions & 2 deletions scripts/доказуемость.sh
Original file line number Diff line number Diff line change
Expand Up @@ -265,6 +265,23 @@ OTVERGNUTO=$(printf '%s\n' "$PROGON_VYVOD" | sed -n 's/.*честных.*/&/p' |
NAB_POYMANO=$(printf '%s\n' "$PROGON_VYVOD" | sed -n 's/^ *набор подделок: поймано \([0-9][0-9]*\) из \([0-9][0-9]*\).*/\1/p')
if [ "$PROGON_KOD" -eq 0 ]; then P3=ДА; else P3=НЕТ; fi

# ПРОГОН, НЕ ДАВШИЙ ЧИСЛА, — ЭТО ПОЛОМКА ПРИБОРА, А НЕ ОСЛАБШИЙ НАБОР.
# Строки «подделок N:» нет — значит прогон кончился, не дойдя до итога. Без
# этой ветки $PODDELOK ниже становился нулём, проверка 4 честно сравнивала 0 с
# храповиком и печатала «выпало 533 (подделка не собралась или проба убрана)» —
# диагноз, указывающий не туда. Так было семь дней подряд, с 18 по 24 сентября
# 2026: в работе Provability не задана FLANG_TMP, прогон падал на `mktemp -d -p
# /srv/tmp` (на раннере такого каталога нет) и уходил кодом 1 молча.
PODDELOK_EST=да
if [ -z "${PODDELOK:-}" ]; then
PODDELOK_EST=нет
NE_IZMERIL=1
P3=НЕТ
LINEYKA_BEDA="набор проб кончился кодом $PROGON_KOD, не напечатав итога («подделок N:») — мерить нечем"
echo "прогон набора проб не дал итоговых чисел (код $PROGON_KOD); последние строки:" >&2
printf '%s\n' "$PROGON_VYVOD" | tail -5 >&2
fi

# ── ПРОВЕРКА 4: набор не ослаб (храповик)? ─────────────────────────────────
P4=ДА; P4_SLOVO=""
if [ ! -f "$HRAPOVIK" ]; then
Expand All @@ -291,7 +308,11 @@ else
# прогона, что не собралась (sed не нашёл строки в перепечатанной записи) или
# убрана, из счёта выпадает молча — здесь убыль громкая.
[ -n "${PODDELOK:-}" ] || PODDELOK=0
if [ "$PODDELOK" -lt "$HR_PR" ]; then
if [ "$PODDELOK_EST" = нет ]; then
P4=НЕТ
if [ -n "$P4_SLOVO" ]; then P4_SLOVO="$P4_SLOVO; "; fi
P4_SLOVO="${P4_SLOVO}проб на подлог НЕ ИЗМЕРЕНО: прогон не дал итога (храповик $HR_PR) — сравнивать не с чем"
elif [ "$PODDELOK" -lt "$HR_PR" ]; then
P4=НЕТ
if [ -n "$P4_SLOVO" ]; then P4_SLOVO="$P4_SLOVO; "; fi
P4_SLOVO="${P4_SLOVO}проб на подлог в прогоне $PODDELOK при храповике $HR_PR — выпало $((HR_PR-PODDELOK)) (подделка не собралась или проба убрана)"
Expand Down Expand Up @@ -325,7 +346,11 @@ if [ "$NE_IZMERIL" -eq 1 ]; then
else
echo "проверка 2 — доля проигрыванием не ниже ${POROG} %? $P2 (${DOLYA} %: ${DOLYA_CH} из ${DOLYA_ZN}; недостижимых мест вынесено ${NEDOST:-0})"
fi
echo "проверка 3 — набор проб пройден? $P3 (набор подделок ${NAB_POYMANO:-?} из ${NAB_STROK:-?}; проб на подлог ${PODDELOK:-?}, принято кодом 0 — ${PRINYATO:-?}; честных ${CHESTNYH:-?}, отвергнуто ${OTVERGNUTO:-?})"
if [ "${PODDELOK_EST:-да}" = нет ]; then
echo "проверка 3 — набор проб пройден? НЕ ИЗМЕРЕНА (прогон кончился кодом $PROGON_KOD, не напечатав итога «подделок N:»)"
else
echo "проверка 3 — набор проб пройден? $P3 (набор подделок ${NAB_POYMANO:-?} из ${NAB_STROK:-?}; проб на подлог ${PODDELOK:-?}, принято кодом 0 — ${PRINYATO:-?}; честных ${CHESTNYH:-?}, отвергнуто ${OTVERGNUTO:-?})"
fi
if [ "$P4" = ДА ]; then
echo "проверка 4 — набор не ослаб? ДА (в манифесте ${NAB_STROK:-?} при храповике ${HR_P:-?}; числитель ${NAB_CHISL:-?} при храповике ${HR_CH:-?}; проб на подлог ${PODDELOK:-?} при храповике ${HR_PR:-?})"
else
Expand Down
Loading