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
1 change: 1 addition & 0 deletions .flangrc
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
23 changes: 23 additions & 0 deletions .github/workflows/binary.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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) ───────
#
# ПОЧЕМУ ОТДЕЛЬНАЯ РАБОТА, А НЕ ШАГ У СОСЕДЕЙ ВЫШЕ. Эта проба собирает ВТОРОЙ
Expand Down
10 changes: 7 additions & 3 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
6 changes: 3 additions & 3 deletions docs/course/03-totality.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 не снята
заново: пересчёт не укладывается в отведённое время.*

Разберём таблицу.

Expand Down
4 changes: 2 additions & 2 deletions docs/course/09-eight-targets.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`;
Expand Down
2 changes: 1 addition & 1 deletion docs/course/13-where-next.md
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ node docs/site/build.mjs --check
половины, и родословная у них разная: «дешёвая» (файлы, строки, версия выпуска)
пересчитана 18 сентября 2026 на коммите `d6e88d50`, «дорогая» (функции,
тотальность, утверждения, словарь) — 23 августа 2026 на коммите `252606e8`,
прогоном двоичного по всему корпусу в несколько часов.
прогоном двоичного по всем программам репозитория в несколько часов.

**И честная оговорка, которая пережила все правки.** Проверка чисел не входит в
`npm test`, и расхождение между файлом и деревом может стоять неделями. Так и
Expand Down
4 changes: 2 additions & 2 deletions docs/guide/how-to-write-flang.ru.md
Original file line number Diff line number Diff line change
Expand Up @@ -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`, их комментарии уходят со следующей
печатью) и пять проб сверщика, где комментарий и есть подделка
Expand Down
12 changes: 12 additions & 0 deletions docs/jargon.json
Original file line number Diff line number Diff line change
Expand Up @@ -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",
"слово": "свидетель",
Expand Down
2 changes: 1 addition & 1 deletion docs/site/roadmap.ru.md
Original file line number Diff line number Diff line change
Expand Up @@ -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). Что внешний проверяющий перепроверит сам, по требованию на
Expand Down
Loading
Loading