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 .ai/AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -286,7 +286,7 @@ git fetch /srv/flang-priyom.git main && git checkout -B main FETCH_HEAD
копии, где сошлись ДВЕ невлитые ветки: ключ `--предел-шагов` (`dd5fe0fd`) и
быстрое сравнение имён `fl_name_same` (`b7f3bd5e`). Сплошной перебор 5418
коммитов такого дерева не нашёл; ловит это теперь
`sh scripts/seed/binary-origin.sh` — по именам функций в двоичном, а не по размеру.
`bootstrap/flang io scripts/seed/binary-origin.fscript --plan Check --timeout 300000` — по именам функций в двоичном, а не по размеру.
Ближайший коммит с тем же семенем, `58596087`, даёт 14 068 168 байт
(`090ef472`) — на 80 байт меньше: `.rodata` совпадает байт в байт, расходятся
`.text` (384) и `.eh_frame` (2880). Значит не воспроизводится ДЕРЕВО, а не
Expand Down Expand Up @@ -437,7 +437,7 @@ flang check <файл> --proof ведомость: чем несётся ка

| стек | пишет | НЕ пишет |
|---|---|---|
| **А — печать и семя** | `scripts/bootstrap-reprint.sh`, `scripts/seed/print-progress.fscript`, `scripts/seed/two-prints-identical.sh`, `bootstrap/**`, `.github/workflows/reprint.yml`, `docs/reprint-*.md` | всё `flang/**` |
| **А — печать и семя** | `scripts/bootstrap-reprint.sh`, `scripts/seed/print-progress.fscript`, `scripts/seed/two-prints-identical.fscript`, `bootstrap/**`, `.github/workflows/reprint.yml`, `docs/reprint-*.md` | всё `flang/**` |
| **Б — язык и доказательства** | `flang/**`, `.claude/skills/**`, `docs/zettel/**` | всё, что в стеке А |

**Спорные файлы — у каждого ОДИН хозяин, записано здесь:**
Expand Down
2 changes: 1 addition & 1 deletion .githooks/pre-push.fscript
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
возвращает список «Check»
обеспечивает «there are exactly eighteen checks» (длина результат) равен 18
[запись «Check» с «name» равным "prose-numbers-guard" и «command» равным "sh scripts/guards/prose-numbers-guard.sh",
запись «Check» с «name» равным "seed-runtime-is-source" и «command» равным "sh scripts/seed/seed-runtime-is-source.sh",
запись «Check» с «name» равным "seed-runtime-is-source" и «command» равным "bootstrap/flang io scripts/seed/seed-runtime-is-source.fscript --plan Check",
запись «Check» с «name» равным "seed-refresh" и «command» равным "sh scripts/seed/seed-refresh.sh --check",
запись «Check» с «name» равным "version-derivations-guard" и «command» равным "sh scripts/guards/version-derivations-guard.sh",
запись «Check» с «name» равным "who-calls-the-guards" и «command» равным "sh scripts/guards/who-calls-the-guards.sh --check",
Expand Down
20 changes: 10 additions & 10 deletions .github/workflows/binary.yml
Original file line number Diff line number Diff line change
Expand Up @@ -280,10 +280,10 @@ jobs:
# зеленеет. Второй шаг подкладывает ему программу с заведомо чужим именем
# и требует отказа; без него первый шаг ничего не доказывает.
- name: Check binary origin
run: sh scripts/seed/binary-origin.sh --чем "работа «Binary»"
run: bootstrap/flang io scripts/seed/binary-origin.fscript --plan Check --timeout 300000 -- --what "работа «Binary»"

- name: Probe binary origin
run: sh scripts/seed/binary-origin.sh --подлог
run: bootstrap/flang io scripts/seed/binary-origin.fscript --plan Forgery --timeout 300000

# Собралось — ещё не значит работает. Проверяется то, что человек наберёт
# первым, и настоящий файл дерева, а не выдуманный.
Expand Down Expand Up @@ -393,9 +393,9 @@ jobs:
#
# Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md,
# docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН
# язык: JavaScript. Оболочка (89 файлов, 22907 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-17 файлов *.sh = 89 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 22907 (задача 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. Оболочка (79 файлов, 21020 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-17 файлов *.sh = 79 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 21020 (задача 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 не считались нигде и ни в одной проверке. Долг,
# которого никто не считает, не убывает: его не видно ни в отчёте, ни в
# ленте, и растёт он молча.
Expand Down Expand Up @@ -940,7 +940,7 @@ jobs:
#
# ПЕРВАЯ ПОЛОВИНА ДОКАЗАНА 6 сентября 2026: пара печатей с дерева `d3b121b5`
# (клоны одного коммита), 16 404 с и 16 929 с, обе кодом 0;
# `scripts/seed/two-prints-identical.sh` — код 0, «печати совпали побайтово:
# `scripts/seed/two-prints-identical.fscript` — код 0, «печати совпали побайтово:
# файлов 4, байт 1 229 825». ВТОРАЯ осталась открытой: сверку позвала рука.
#
# ТОЙ ЖЕ ПАРОЙ ВТОРУЮ ПОЛОВИНУ НЕ ЗАКРЫТЬ. 2 x 4,6 ч машины на пуш не ставят.
Expand All @@ -955,8 +955,8 @@ jobs:
# процессов), и сверка байт в байт.
#
# ЦЕНА, ЗАМЕР 6 сентября 2026 на машине отряда, `bootstrap/flang` 0.7.11:
# sh scripts/seed/print-is-repeatable.sh 24,4 с (две печати по 12,2 с)
# sh scripts/seed/print-is-repeatable.sh --подлог 12,3 с (одна печать)
# bootstrap/flang io scripts/seed/print-is-repeatable.fscript --plan Check --timeout 600000 24,4 с (две печати по 12,2 с)
# bootstrap/flang io scripts/seed/print-is-repeatable.fscript --plan Forgery --timeout 600000 12,3 с (одна печать)
# Для сравнения, тем же прогоном и тем же двоичным:
# sh scripts/bootstrap-reprint.sh --telo 0,15 с
# sh scripts/bootstrap-reprint.sh --bystro 1,50 с
Expand Down Expand Up @@ -1026,11 +1026,11 @@ jobs:
# прибором). Проба подкладывает сверщику изменённый байт и пропавший
# файл и требует красноты, а от дословной копии — молчания.
- name: Probe print determinism
run: sh scripts/seed/print-is-repeatable.sh --подлог
run: bootstrap/flang io scripts/seed/print-is-repeatable.fscript --plan Forgery --timeout 600000
env:
FLANG_TMP: ${{ runner.temp }}
- name: Check print determinism
run: sh scripts/seed/print-is-repeatable.sh
run: bootstrap/flang io scripts/seed/print-is-repeatable.fscript --plan Check --timeout 600000
env:
FLANG_TMP: ${{ runner.temp }}

Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -206,8 +206,8 @@ jobs:
# 31 августа 2026 в дереве нашлось 31 место в 14 файлах, где записанное рукой
# число разошлось с тем, что лежит рядом: `docs/tree-inventory.md` считала
# `seed-parses-sources-guard.sh` в 83 строки при 195, оболочку — в 66 файлов
# при 71 тогдашних — сегодня их 89;
# СНЯТО 2026-09-17 файлов *.sh = 89 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22;
# при 71 тогдашних — сегодня их 79;
# СНЯТО 2026-09-17 файлов *.sh = 79 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22;
# `flang/PLAN.md` — пять вариантов «Поручение» при 22. Каждое из этих чисел
# было ВЕРНО В ДЕНЬ ЗАПИСИ и солгало назавтра, и сторожа не было ни на одном.
#
Expand Down Expand Up @@ -1684,7 +1684,7 @@ jobs:
# отпечаток семени снят с чистого дерева. На стволе 15 сентября 2026 он снят
# с правленого («ОТПЕЧАТОК СНЯТ С ПРАВЛЕНОГО ДЕРЕВА»): оба отвечают кодом 3,
# «судить нельзя», и пробы при них честно красны — отказ судить не краснота
# сторожа. Сверх того `доказанное` при `SEMYA_OTSTALO_ZNAYU=1` на том же
# сторожа. Сверх того `доказанное` при `FLANG_SEED_LAG_KNOWN=1` на том же
# стволе говорит «numbers.flang — было доказано 5, стало 0»: это суд старым
# семенем, и перемерять его до перепечатки нечем.
#
Expand Down
28 changes: 17 additions & 11 deletions .github/workflows/provability.yml
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ name: Provability
# ВЕРДИКТ «ДОКАЗУЕМ / НЕ ДОКАЗУЕМ» СНИМАЕТСЯ ПРИБОРОМ ПО РАСПИСАНИЮ, А НЕ
# ВПИСЫВАЕТСЯ РУКОЙ.
#
# Работа зовёт `sh scripts/доказуемость.sh`: четыре проверки, у каждой число,
# Работа зовёт `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000`: четыре проверки, у каждой число,
# слово выводится из чисел (шапка скрипта). Код возврата несёт вердикт:
# 0 — ДОКАЗУЕМ, 1 — НЕ ДОКАЗУЕМ, 2 — не смог измерить. Работа отвечает тем же
# 0 — ДОКАЗУЕМ, 1 — НЕ ДОКАЗУЕМ, 3 — не смог измерить. Работа отвечает тем же
# кодом, поэтому её цвет — это вердикт, а не «прошла ли сборка».
#
# ── Когда работа красна, и почему это законно ───────────────────────────────
Expand All @@ -18,7 +18,7 @@ name: Provability
# рукой или опустить порог, чтобы работа позеленела, — подлог.
#
# ── ЧТО ЭТА РАБОТА МЕРИТ, А ЧЕГО НЕ МЕРИТ (пункт 11 внешнего аудита) ────────
# Замер 19 сентября 2026 на дереве 404c4ec0a: `sh scripts/доказуемость.sh`
# Замер 19 сентября 2026 на дереве 404c4ec0a: `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000`
# печатает ДОКАЗУЕМ и отвечает кодом 0 ДАЖЕ ТОГДА, когда `bootstrap/flang` из
# дерева убран. Все четыре его проверки читают записи корпуса, манифест
# подделок и сверщика — и ни одна не зовёт собранный двоичный. Шаг
Expand All @@ -40,7 +40,7 @@ name: Provability
# расписаний: reprint.yml — воскресенье 02:00 UTC, target-twins.yml — понедельник
# 04:00 UTC, install-path.yml — ежедневно 04:17 UTC.
#
# ── Что нужно прибору (шапка scripts/доказуемость.sh) ───────────────────────
# ── Что нужно прибору (шапка scripts/provability.fscript) ───────────────────────
# Дерево под учётом git (линейка берёт ведомость из `git archive HEAD`, глубины
# 1 довольно); исходник сверщика flang/proof/checker/checker.c — скрипт соберёт
# его сам, если двоичного нет, но здесь он собирается заранее тем же Makefile,
Expand All @@ -60,7 +60,7 @@ jobs:
runs-on: ubuntu-latest
timeout-minutes: 45
# FLANG_TMP НА ВСЮ РАБОТУ, а не по шагам. Прогон набора проб чекера
# (flang/proof/checker/tests/run.sh, его зовёт scripts/доказуемость.sh)
# (flang/proof/checker/tests/run.sh, его зовёт scripts/provability.fscript)
# берёт времянку как `mktemp -d -p "${FLANG_TMP:-/srv/tmp}"`. На раннере
# каталога /srv/tmp нет, mktemp падает, и при `set -eu` прогон кончается
# НЕМЕДЛЕННО кодом 1, не напечатав ни одной строки итога. Вердикт читает
Expand Down Expand Up @@ -123,16 +123,19 @@ jobs:
echo "проба сошлась: без двоичного шаг отвечает кодом $kod"

# Четыре покрытия публикуются ПОРОЗНЬ — доля корпуса, формализация,
# известные нарушения состоятельности, трансляция. Код 2 значит «Lean на
# известные нарушения состоятельности, трансляция. Код 3 значит «Lean на
# раннере нет, блоки вне приёмки здесь не сняты» и работу не роняет:
# прибор МЕРИТ, а не судит.
- name: Measure four coverages
run: |
set +e
export LC_ALL=C.UTF-8
log="$RUNNER_TEMP/покрытия.log"
sh scripts/four-coverages.sh > "$log" 2>&1
raw="$RUNNER_TEMP/coverages.raw"
log="$RUNNER_TEMP/coverages.log"
bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000 > "$raw" 2>&1
kod=$?
grep '^{' "$raw" | jq -r '.result // .error' > "$log"
[ -s "$log" ] || cp "$raw" "$log"
cat "$log"
{
echo "## Четыре покрытия — порознь (код $kod)"
Expand All @@ -141,15 +144,18 @@ jobs:
cat "$log"
echo '```'
} >> "$GITHUB_STEP_SUMMARY"
[ "$kod" -le 2 ] || exit 1
[ "$kod" -eq 0 ] || [ "$kod" -eq 3 ] || exit 1

- name: Report verdict
run: |
set +e
export LC_ALL=C.UTF-8
log="$RUNNER_TEMP/доказуемость.log"
sh scripts/доказуемость.sh > "$log" 2>&1
raw="$RUNNER_TEMP/provability.raw"
log="$RUNNER_TEMP/provability.log"
bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 > "$raw" 2>&1
kod=$?
grep '^{' "$raw" | jq -r '.result // .error' > "$log"
[ -s "$log" ] || cp "$raw" "$log"
cat "$log"
{
echo "## Доказуемость — вердикт прибора, код $kod"
Expand Down
Loading
Loading