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
8 changes: 4 additions & 4 deletions .flangrc
Original file line number Diff line number Diff line change
Expand Up @@ -48,19 +48,19 @@ script.target-words:check = bootstrap/flang io flang/scripts/target-words.fscrip
script.file-extensions:check = bootstrap/flang io scripts/guards/file-extensions.fscript --на-веру
script.kernel-forgeries:check = bootstrap/flang run-script seed:freshness --what kernel-forgeries:check >&2 && bootstrap/flang io flang/scripts/kernel-forgeries.fscript --plan 'Подделки остаются недоказанными' --на-веру
script.axioms:check = bootstrap/flang io flang/scripts/kernel-forgeries.fscript --plan 'Аксиом ноль' --на-веру
script.proof-record:check = bootstrap/flang run-script seed:freshness --what proof-record:check >&2 && sh flang/proof/forgeries/run.sh
script.proof-record:check = bootstrap/flang run-script seed:freshness --what proof-record:check >&2 && bootstrap/flang io flang/proof/forgeries/run.fscript --max-steps 4000000000 --timeout 14400000
script.record-source:check = bootstrap/flang io scripts/guards/record-follows-its-source.fscript --plan Проверка
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.translation:check = sh flang/translation/run.sh
script.proved-share:check = sh flang/proof/corpus-share.sh --набор корпус
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
script.kernel-verdict:forgery = bootstrap/flang io flang/proof/kernel-verdict-forgery.fscript --max-steps 4000000000 --timeout 900000
script.proof-records:freshness = bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000
script.provability = bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000
script.share:replay = sh flang/proof/corpus-share.sh --проигрыванием
script.share:forgery = sh flang/proof/corpus-share.sh --проигрыванием --самопроверка
script.share:replay = bootstrap/flang io flang/proof/replay-share.fscript --max-steps 4000000000 --timeout 900000
script.share:forgery = bootstrap/flang io flang/proof/replay-share.fscript --max-steps 4000000000 --timeout 900000 -- --forgery
script.child-timeout:check = bootstrap/flang io scripts/guards/child-timeout.fscript --timeout 120000
script.conc-link:emit = bootstrap/flang io scripts/targets/conc-link-emit.fscript --на-веру
script.release:check = bootstrap/flang io scripts/guards/release-guard.fscript --на-веру
Expand Down
14 changes: 8 additions & 6 deletions .github/workflows/binary.yml
Original file line number Diff line number Diff line change
Expand Up @@ -394,9 +394,9 @@ jobs:
#
# Счётчиков долга в дереве было три — раздел «Вне языка» в docs/ROADMAP.md,
# docs/javascript-inventory.md и числа сайта, — и все три считали ОДИН
# язык: JavaScript. Оболочка (54 файлов, 11512 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-17 файлов *.sh = 54 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 11512 (задача 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. Оболочка (52 файлов, 9762 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-17 файлов *.sh = 52 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 9762 (задача 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 All @@ -407,9 +407,9 @@ jobs:
# оболочке или на Python останавливает работу в тот же день.
#
# Замер на этом дереве: 17,7 с и 471 МБ, двоичному хватает `git` и `wc`.
# Предел шагов поднят с умолчания (10 млн): опись обходит 196 файлов и
# Предел шагов поднят с умолчания (10 млн): опись обходит 194 файлов и
# семнадцать языков, и в умолчание не укладывается.
# СНЯТО 2026-09-17 файлов *.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 = 196 (задача 5821: семь проверок scripts/** стали планами; до них 251, снято 2026-09-27) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-17)
# СНЯТО 2026-09-17 файлов *.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 = 194 (задача 5821: семь проверок scripts/** стали планами; до них 251, снято 2026-09-27) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-17)
#
# СКОЛЬКО ИЗ ЭТИХ ПЯТИДЕСЯТИ МИЛЛИОНОВ УХОДИТ, замер 29 августа 2026.
# Меряно перебором самого предела: при 10 500 000 опись умирает
Expand Down Expand Up @@ -1467,7 +1467,9 @@ jobs:
env:
FLANG_TMP: ${{ runner.temp }}
- name: Check corpus ledger
run: sh flang/proof/corpus-share.sh --набор корпус
run: bootstrap/flang io flang/proof/share-measure.fscript --max-steps 4000000000 --timeout 900000 -- --set corpus
env:
FLANG_TMP: ${{ runner.temp }}

# ── СЛИЧИТЕЛЬ ПЕРЕВОДА: ПРОТОКОЛ ПЕЧАТНИКА ПЕРЕИГРЫВАЕТСЯ НА C ──────────────
#
Expand Down
4 changes: 2 additions & 2 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 тогдашних — сегодня их 54;
# СНЯТО 2026-09-17 файлов *.sh = 54 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22;
# при 71 тогдашних — сегодня их 52;
# СНЯТО 2026-09-17 файлов *.sh = 52 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-21) `flang/cat/SPEC.md` обещала восемнадцать поручений при 22;
# `flang/PLAN.md` — пять вариантов «Поручение» при 22. Каждое из этих чисел
# было ВЕРНО В ДЕНЬ ЗАПИСИ и солгало назавтра, и сторожа не было ни на одном.
#
Expand Down
8 changes: 4 additions & 4 deletions docs/ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -59,8 +59,8 @@ Haskell. flang целится в одно: язык, на котором и до
### Этап 1 (ЗАКРЫТ 18 сентября 2026). Независимый проверяющий переигрывает ВСЁ в собственных записях компилятора

**Снято 18 сентября 2026** (ветка `a/5190-seed-reprint-0-7-20` над `main` `d366fc8f2`,
сверщик собран заново из исходника): `sh flang/proof/corpus-share.sh --набор корпус
--проигрыванием` → **650 из 650 = 100,00 %**; `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000` → **ДОКАЗУЕМ**,
сверщик собран заново из исходника): `bootstrap/flang io
flang/proof/replay-share.fscript` → **650 из 650 = 100,00 %**; `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000` → **ДОКАЗУЕМ**,
код 0. Разбивка числителя печатается прибором: на слово ядра — посылок и утверждений 0,
шагов 0; снято калькулятором, а не игрой, — 0. Знаменатель 650 — это все 672 обязательства
набора за вычетом 22 мест четырёх записей, которые сверщик отверг целиком и которые манифест
Expand Down Expand Up @@ -100,7 +100,7 @@ Haskell. flang целится в одно: язык, на котором и до
рода в принципе переигрывается — а переиграется ли он у вас, говорит только прогон
проверяющего на вашей паре «исходник + запись».

**Чем проверяется.** `corpus-share.sh --проигрыванием` печатает
**Чем проверяется.** `replay-share.fscript` печатает
«на слово ядра: посылок и утверждений 0; шагов 0; снято калькулятором 0», а
`bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000` по-прежнему ДОКАЗУЕМ.

Expand Down Expand Up @@ -510,7 +510,7 @@ make -C bootstrap -j8 собрать комп
./bootstrap/flang --version версия собранного двоичного
bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000 четыре покрытия порознь, с датой и SHA
bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 ДОКАЗУЕМ / НЕ ДОКАЗУЕМ по четырём числам, ≈18 с
sh flang/proof/corpus-share.sh --проигрыванием из чего сложена доля первого покрытия
bootstrap/flang io flang/proof/replay-share.fscript из чего сложена доля первого покрытия
bootstrap/flang io flang/proof/records-nesting.fscript записи — то, что печатает СОБРАННЫЙ двоичный
bootstrap/flang run-script checker:check пробы на подлог у независимого проверяющего
./bootstrap/flang check --proof ФАЙЛ отчёт о доказательствах файла
Expand Down
2 changes: 1 addition & 1 deletion docs/flang/proof/forgeries.md
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@
| читатель | что берёт |
|---|---|
| `flang/proof/checker/tests/run.sh` | класс каждой записи корпуса и ожидаемый по нему код |
| `flang/proof/corpus-share.sh` | какие места вынести из знаменателя доли |
| `flang/proof/replay-share.fscript` | какие места вынести из знаменателя доли |
| `scripts/provability.fscript` | проверки 3 и 4 вердикта: набор пойман целиком и не усох |

Запись корпуса с именем `poddelka-*` или `forgery-*`, которой нет в манифесте,
Expand Down
2 changes: 1 addition & 1 deletion docs/flang/proof/known-soundness-violations.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@
в которой доказанным не числится ничего. Код успеха читается как «доказано», а
проверено в такой записи ноль мест; отличить можно только по тексту вывода.
Сколько таких записей в корпусе, печатает
`sh flang/proof/corpus-share.sh --набор корпус`.
`bootstrap/flang io flang/proof/share-measure.fscript -- --set corpus`.

## `theorem-hypothesis-not-discharged` — открыто

Expand Down
2 changes: 1 addition & 1 deletion docs/flang/proof/ratchets.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
| `checker-code-lines` | строк кода в `flang/proof/checker/checker.c` без комментариев и пустых | замер не больше числа | `flang/proof/tables-guard.fscript`, проверка С-6 |
| `checker-primitives` | имён в массиве `ПРИМИТИВЫ[]` проверяющей программы | замер равен числу | там же |

`flang/proof/corpus-share.sh` печатает `forgeries` и `forgery-numerator` рядом со
`flang/proof/replay-share.fscript` печатает `forgeries` и `forgery-numerator` рядом со
своим замером, чтобы просадку было видно там же, где число.

## Что делает вердикт при нарушении
Expand Down
2 changes: 1 addition & 1 deletion docs/four-coverages.md
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000
а не принял на слово у ядра. Записи лежат готовыми в
`flang/proof/checker/tests/records/corpus/` — по одной на программу-образец, всего 91.
<!-- СНЯТО 2026-09-19 файлов flang/proof/checker/tests/records/corpus/*.record = 91 -->
Снимается: `sh flang/proof/corpus-share.sh --проигрыванием`.
Снимается: `bootstrap/flang io flang/proof/replay-share.fscript`.

**Что это даёт сказать.** Что у этого набора записей слово «доказано» в отчёте компилятора не
опирается на веру компилятору: вторая программа, в которой нет ни строки компилятора, прошла те же
Expand Down
4 changes: 2 additions & 2 deletions docs/javascript-inventory.md
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,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) (26 сентября 2026: 196 файлов вне flang,
<!-- СНЯТО 2026-09-17 файлов *.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 = 196 (задача 4413: flang/scripts/proof-ledger.mjs и word-guard.mjs сняты — свод корпуса считает двойник на flang; до них 51 файл и 24 386 строк, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-21) -->
считает [`tree-inventory.md`](tree-inventory.md) (26 сентября 2026: 194 файлов вне flang,
<!-- СНЯТО 2026-09-17 файлов *.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 = 194 (задача 4413: flang/scripts/proof-ledger.mjs и word-guard.mjs сняты — свод корпуса считает двойник на flang; до них 51 файл и 24 386 строк, снято 2026-09-17) (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 256, снято 2026-09-21) -->
долг вне JavaScript — **97 файлов, 18 427 строк при потолке 63**: храповик
красен, разбор — задачи 4838 и 7405). Там же названы 569 строк
JavaScript, лежащих ВНУТРИ файлов `.html`: счёт по именам файлов их не видит, и
Expand Down
2 changes: 1 addition & 1 deletion docs/road-to-one-hundred-measured.md
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@
## 0. Откуда 134 и как они названы поимённо

```
sh flang/proof/corpus-share.sh --проигрыванием
bootstrap/flang io flang/proof/replay-share.fscript
ЧИСЛИТЕЛЬ 517 = ходами/тотальностью 390 + по существу 93 + узлы 34
ЗНАМЕНАТЕЛЬ 651 доля = 517 / 651 = 79.42 % порог 95 %: НЕТ
на слово ядра: посылок и утверждений 109; шагов 17; снято вычислением 8
Expand Down
Loading
Loading