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
10 changes: 5 additions & 5 deletions .flangrc
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ issues = https://github.com/digitable-lol/flang/issues

unproven = refuse

script.build = sh scripts/bootstrap-reprint.sh --telo && make -C bootstrap -j"$(getconf _NPROCESSORS_ONLN)" && sh flang/proof/corpus-share.sh --отпечаток
script.build = sh scripts/bootstrap-reprint.sh --telo && make -C bootstrap -j"$(getconf _NPROCESSORS_ONLN)" && bootstrap/flang io flang/proof/binary-fingerprint.fscript
script.scripts:check = bootstrap/flang io scripts/shortcut-collector.fscript --plan Целость && bootstrap/flang io scripts/shortcut-collector.fscript --plan Сбор --max-orders 20000
script.licenses:check = bootstrap/flang io scripts/guards/license-guard.fscript
script.claims:check = bootstrap/flang io flang/scripts/claim-guard.fscript --plan 'Утверждения о недостаче сверены с лексером' --max-steps 2000000000 --max-orders 100000 --на-веру
Expand Down Expand Up @@ -54,10 +54,10 @@ script.record-source:forgery = bootstrap/flang io scripts/guards/record-follows-
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:forgery = sh flang/proof/corpus-share.sh --подлог
script.kernel-verdict:check = sh flang/proof/corpus-share.sh --приговор-ядра
script.kernel-verdict:forgery = sh flang/proof/corpus-share.sh --подлог-ядра
script.proof-records:freshness = sh flang/proof/corpus-share.sh --вложенность
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 --проигрыванием --самопроверка
Expand Down
18 changes: 12 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 файлов, 12045 строк), HTML, CSS, пробы на
# язык: JavaScript. Оболочка (54 файлов, 11512 строк), HTML, CSS, пробы на
# СНЯТО 2026-09-17 файлов *.sh = 54 (задача 5821: семь скриптов scripts/** переехали с оболочки на flang; до них 101, снято 2026-09-17)
# СНЯТО 2026-09-17 строк-в *.sh = 12045 (задача 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)
# СНЯТО 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)
# C, Python, awk и Erlang не считались нигде и ни в одной проверке. Долг,
# которого никто не считает, не убывает: его не видно ни в отчёте, ни в
# ленте, и растёт он молча.
Expand Down Expand Up @@ -1460,10 +1460,12 @@ jobs:
# работа охраны.
- name: Probe corpus ledger
run: |
if ! sh flang/proof/corpus-share.sh --подлог; then
if ! bootstrap/flang io flang/proof/share-ledger-forgery.fscript --max-steps 4000000000 --timeout 900000; then
echo "сторож ведомости промолчал на подлоге — проверять им нечего" >&2
exit 1
fi
env:
FLANG_TMP: ${{ runner.temp }}
- name: Check corpus ledger
run: sh flang/proof/corpus-share.sh --набор корпус

Expand Down Expand Up @@ -1594,13 +1596,17 @@ jobs:
# и прибор его для них не требует; шаг сборки чекера при коммите ae42220a2
# отсюда выпал, и `--вложенность` осталась бы без него — возвращён.
- name: Record seed fingerprint
run: sh flang/proof/corpus-share.sh --отпечаток
run: bootstrap/flang io flang/proof/binary-fingerprint.fscript
- name: Probe seed fingerprint
run: sh flang/proof/corpus-share.sh --подлог-отпечатка
run: bootstrap/flang io flang/proof/binary-fingerprint.fscript -- --forgery
env:
FLANG_TMP: ${{ runner.temp }}
- name: Build proof checker
run: make -C flang/proof/checker
- name: Check corpus records
run: sh flang/proof/corpus-share.sh --вложенность
run: bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000
env:
FLANG_TMP: ${{ runner.temp }}

# Предмет тут другой — сторож кодов, — но работа та же по той же причине,
# по которой `imena` не стала шагом в `sborka`: сборка двоичного стоит
Expand Down
6 changes: 3 additions & 3 deletions .github/workflows/provability.yml
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ jobs:
# в обе стороны (кеш отдаёт двоичный со старым временем, checkout кладёт
# семя свежим).
- name: Record seed fingerprint
run: sh flang/proof/corpus-share.sh --отпечаток
run: bootstrap/flang io flang/proof/binary-fingerprint.fscript

# `--вложенность` — единственная проверка этого дерева, где предмет суда
# есть САМ СОБРАННЫЙ ДВОИЧНЫЙ: каждая запись корпуса печатается заново
Expand All @@ -103,7 +103,7 @@ jobs:
# Без этого шага вердикт ниже говорил бы о записях, напечатанных когда-то,
# а не о двоичном, который выйдет в выпуск.
- name: Check corpus records
run: sh flang/proof/corpus-share.sh --вложенность
run: bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000

# Сторож, которого нельзя покрасить, неотличим от выключенного. Двоичный
# уносится в RUNNER_TEMP и возвращается при ЛЮБОМ исходе: иначе неудача
Expand All @@ -112,7 +112,7 @@ jobs:
run: |
set +e
mv bootstrap/flang "$RUNNER_TEMP/flang.отложен"
sh flang/proof/corpus-share.sh --вложенность > "$RUNNER_TEMP/без-двоичного.log" 2>&1
bootstrap/flang io flang/proof/records-nesting.fscript --max-steps 4000000000 --timeout 900000 > "$RUNNER_TEMP/без-двоичного.log" 2>&1
kod=$?
mv "$RUNNER_TEMP/flang.отложен" bootstrap/flang
cat "$RUNNER_TEMP/без-двоичного.log"
Expand Down
2 changes: 1 addition & 1 deletion .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ bootstrap/*.a
bootstrap/flang
bootstrap/flang_cli
# Отпечаток семени при двоичном (sha256 двоичного и входов сборки) — пишет
# `sh flang/proof/corpus-share.sh --отпечаток` после make; по нему прибор
# `bootstrap/flang io flang/proof/binary-fingerprint.fscript` после make; по нему прибор
# `--вложенность` судит, из этого ли семени собран двоичный, не глядя на время.
bootstrap/flang.seed-sha256

Expand Down
4 changes: 2 additions & 2 deletions docs/ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -325,7 +325,7 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000
«100 % утверждений дерева доказаны». О собранном коде оно не говорит ничего (этап 2), и о
собранном ДВОИЧНОМ тоже: замер 19 сентября 2026 — `bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000` печатает
ДОКАЗУЕМ и кодом 0 даже тогда, когда `bootstrap/flang` из дерева убран. Двоичный судит
отдельная проверка `sh flang/proof/corpus-share.sh --вложенность`, и она заведена в ту же
отдельная проверка `bootstrap/flang io flang/proof/records-nesting.fscript`, и она заведена в ту же
работу CI. Полный разбор четырёх покрытий — [`docs/four-coverages.md`](four-coverages.md).

**Правила.** 109 строк перечня `flang/proof/tables/inference-rules.tsv`, у всех 109 есть лемма в
Expand Down Expand Up @@ -511,7 +511,7 @@ make -C bootstrap -j8 собрать комп
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 --проигрыванием из чего сложена доля первого покрытия
sh flang/proof/corpus-share.sh --вложенность записи — то, что печатает СОБРАННЫЙ двоичный
bootstrap/flang io flang/proof/records-nesting.fscript записи — то, что печатает СОБРАННЫЙ двоичный
bootstrap/flang run-script checker:check пробы на подлог у независимого проверяющего
./bootstrap/flang check --proof ФАЙЛ отчёт о доказательствах файла
./bootstrap/flang check --proof ФАЙЛ --записать З запись доказательства
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
перепечаткой.

**В корпус эти записи не положены.** Корпус обязан быть печатью семени байт в
байт — это стережёт `sh flang/proof/corpus-share.sh --вложенность` на каждом
байт — это стережёт `bootstrap/flang io flang/proof/records-nesting.fscript` на каждом
пуше, и две записи шага А, положенные в корпус, покрасили его в PR #21
(«РАЗОШЛАСЬ» ×2). Путь тот же, что у 6205: печать ядра живёт здесь пробой, а в
корпус ложится перепечаткой партии. Доля «после перепечатки» мерится тем же
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -34,4 +34,4 @@
Записи — печать ядра, снятая толкованием исходников `flang/self` семенем 0.7.19
(зонд `flang/self/bootstrap/check-with-source-compiler.flang`): семя правок `zapis.flang` не несёт,
в двоичное они доедут перепечаткой (задача 5190). В корпус записи не положены —
корпус обязан быть печатью семени байт в байт (`corpus-share.sh --вложенность`).
корпус обязан быть печатью семени байт в байт (`records-nesting.fscript`).
2 changes: 1 addition & 1 deletion docs/four-coverages.md
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@ bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 90000
- Не «100 % программ доказаны». Знаменатель — обязательства этих записей, а не ваши программы.
- Не утверждение о собранном двоичном. Записи лежат в дереве готовыми; совпадают ли они с тем, что
печатает `bootstrap/flang` СЕГОДНЯ, — отдельный вопрос и отдельная проверка
(`sh flang/proof/corpus-share.sh --вложенность`).
(`bootstrap/flang io flang/proof/records-nesting.fscript`).
- Не «проверено всё, что есть в наборе». Часть записей проверяющий отвергает ЦЕЛИКОМ — это нарочные
подделки, и их обязательства вынесены из знаменателя; сколько именно, прибор печатает отдельной
строкой.
Expand Down
Loading
Loading