Skip to content

flang 0.7.21 — Недоказанное не запускается молча, а у хозяина появились среда и экран

Choose a tag to compare

View all tags
@github-actions github-actions released this 21 Sep 22:30
· 1649 commits to main since this release
v0.7.21
df4aa50

Недоказанный код больше не запускается по умолчанию

Что сломалось

  • flang run и flang io выходят кодом 3, если обещание функции не доказано. Раньше такая программа запускалась и отвечала кодом 0.

    $ flang run price.flang --function 'Скидка' --args '{"цена": 100, "скидка": 150}'
не доказано: утверждений 1: доказано 0, сетка 1 — запуск только по явному согласию: --trust
код 3

    Миграция: добавьте --trust — вердикт не будет считаться вовсе.

    Затронуты сценарии, звавшие flang run или flang io на программах, где обеспечивает закрыто только примерами. Проверить заранее: flang check --proof <файл> — итог «доказано 0, сетка N» значит, что программа попадёт под новое правило.

Что появилось

  • Переменные окружения и доводы командной строки в планах. Поручения были в словаре языка, а рантайм отвечал на них FLANG_IO_UNKNOWN.

    вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "HOME")

    Ответ — «Значение среды» с полем значение, либо «Переменной среды нет» отдельным вариантом, а не пустой строкой. Доводы плана — всё, что стоит после --:

    $ flang io script.fscript -- build --verbose

    Запретить: --no-env, --no-args.

  • Вывод на терминал. «Показать» кладёт кадр, «Ждать событие» ждёт клавишу:

    вариант «Сделать» с поручение равным (вариант «Показать» с место равным "экран" и текст равным кадр)
вариант «Сделать» с поручение равным (вариант «Ждать событие» с срок равным 5000)

    Клавиша приходит как «Случилось» с полями откуда и значение; по сроку — «Срок вышел». Имена клавиш: ввод, пробел, таб, возврат, выход, вверх, вниз, влево, вправо; печатный знак приходит собой.

    Рабочий пример — docs/examples/io/progress-bar-on-screen.flang. Кадр идёт на /dev/tty, а не в stdout: там итог плана в JSON. Нет терминала (труба, файл, CI) — ответ прежний, FLANG_IO_NO_SCREEN. Ctrl-C по-прежнему убивает программу. Запретить: --no-screen.

  • sh scripts/four-coverages.sh печатает четыре покрытия порознь, у каждого своя строка «чего это не значит», и рядом с числом стоят дата и коммит.

Что изменилось

  • Независимый сверщик перестал принимать ложное доказательство. Две дыры: подстановка доводов шла последовательно вместо одновременной, подстановка тела не спрашивала захват имени. Ни 529 мутационных проб, ни четыре проверки дерева их не ловили.

  • Он же перестал отвергать честные записи — вердикт зависел от порядка, в котором напечатаны блоки.

  • Доля мест, которые сверщик переигрывает независимо, — 650 из 650. Мест, где он верил ядру на слово, не осталось; прежде их было 12 посылок и 4 шага.

Unproved code no longer runs by default

Breaking

  • flang run and flang io exit with code 3 when a function's promise is not proved. Such a program used to run and exit 0.

    $ flang run price.flang --function 'Скидка' --args '{"цена": 100, "скидка": 150}'
не доказано: утверждений 1: доказано 0, сетка 1 — запуск только по явному согласию: --trust
exit 3

    Migration: add --trust and the verdict is not computed at all.

    Affected: scripts calling flang run or flang io on programs where обеспечивает is backed by examples only. Check in advance with flang check --proof <file> — a summary reading «доказано 0, сетка N» means the program falls under the new rule.

Added

  • Environment variables and command-line arguments in plans. The orders were in the language's vocabulary, but the runtime answered FLANG_IO_UNKNOWN.

    вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "HOME")

    The reply is «Значение среды» with field значение, or «Переменной среды нет» as its own variant — not an empty string. A plan's arguments are whatever follows --:

    $ flang io script.fscript -- build --verbose

    Deny with --no-env, --no-args.

  • Terminal output. «Показать» draws a frame, «Ждать событие» waits for a key:

    вариант «Сделать» с поручение равным (вариант «Показать» с место равным "экран" и текст равным кадр)
вариант «Сделать» с поручение равным (вариант «Ждать событие» с срок равным 5000)

    A key arrives as «Случилось» with fields откуда and значение; a timeout as «Срок вышел». Key names: ввод, пробел, таб, возврат, выход, вверх, вниз, влево, вправо; a printable character arrives as itself.

    Working example: docs/examples/io/progress-bar-on-screen.flang. The frame goes to /dev/tty, not stdout — stdout carries the plan's JSON result. With no terminal (pipe, file, CI) the answer is the same FLANG_IO_NO_SCREEN as before. Ctrl-C still kills the program. Deny with --no-screen.

  • sh scripts/four-coverages.sh prints four coverages separately, each with its own line saying what it is not, and every number carries a date and a commit.

Changed

  • The independent checker no longer accepts a false proof. Two holes: arguments were substituted sequentially rather than simultaneously, and body substitution did not check for name capture. Neither 529 mutation probes nor four tree gates had caught them.

  • The same checker no longer rejects honest records — the verdict depended on the order the blocks were printed in.

  • The share of places the checker replays independently is 650 of 650. Not one place is taken on the kernel's word any more; there used to be 12 premises and 4 steps.

Assets 3
Loading