Skip to content

flang 0.7.23 — Поле записи проверяется по своему типу, и прогон знает предел памяти

Choose a tag to compare

View all tags
@github-actions github-actions released this 29 Sep 09:34
· 1760 commits to main since this release
v0.7.23
dcfd766

Поле записи проверяется по своему типу, и прогон знает предел памяти

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

  • --memory-limit N (--предел-памяти) — предел памяти прогона. Годится при любой команде. У check, test и run по умолчанию три четверти памяти машины; 0 снимает предел. На пределе прогон останавливается кодом 5 и называет функцию, которая считалась.
$ flang run runaway.flang --function «Раздуть» --args '{"текст":"а","раз":28}' --trust --memory-limit 32M
FLANG_MEMORY: прогон остановлен на пределе памяти 32 МиБ: занято 25 МиБ, просили ещё 25 165 880 байт
  считалась функция «Раздуть», шагов программы 544
                                                                    код 5

Заявка #160.

  • Шаг доказательства называет правило ядра. Строка шага в записи --record кончается словами правило «…», в --proof --json есть поле stepRules. Независимая проверяющая программа сверяет имя с правилом, которое применяет сама.
$ flang check chain.flang --proof --json
… "stepRules":[{"step":1,"line":33,"rule":"цель есть допущение"}, …]

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

  • Поле записи проверяется по объявленному типу. Поле неотрицательное принимало -7, и ядро доказывало обещание, которое прогон потом нарушал. Теперь такая программа не проходит проверку типов.
объект «Мера»
  «шаг»: неотрицательное

тотальная функция «Отрицательный шаг»
  возвращает неотрицательное
  обеспечивает «итог не меньше нуля» результат не меньше 0
  (запись «Мера» с «шаг» равным -7).«шаг»

0.7.22: $ flang check step.flang
step.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет   код 0

0.7.23: $ flang check step.flang --proof
FLANG_TYPE в файле step.flang, строка 9, столбец 33: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое   код 1
  • flang io: истёкший срок процесса — «Сбой» FLANG_IO_TIMEOUT. Раньше хозяин отвечал «Процесс убит» SIG9, как при убийстве снаружи. --timeout — срок тишины, отсчёт от последнего байта вывода, по умолчанию 30000 мс; ключ теперь есть в flang io --help.
$ flang io child.fscript --timeout 1000 -- 'sleep 3'
… "failed FLANG_IO_TIMEOUT: программа «sh» молчала дольше 1000 мс и оборвана хозяином (--timeout)"

Заявка #162.

  • Интерпретатор освобождает память на глубокой рекурсии. На рекурсии глубже примерно 500 вызовов память не освобождалась и росла с каждым шагом. «Числа до» от 1000 раньше упирался в 3,6 ГБ, теперь идёт в 370 МБ.

Заявка #160.

  • разделить … по и содержит в C-рантайме ищут разделитель через memchr. На 100 МБ текста разделить — 0,47 → 0,08 с, содержит — 0,39 → 0,008 с; число шагов то же.

Заявка #161.

  • Ключи .flangrc — по-английски. language, surface, color, page, version, name, license, repository, issues, unproven. Старые ключи пока читаются и называют замену.
$ cat .flangrc
недоказанное = разрешение
$ flang run p.flang --function «Ответ»
flang: .flangrc: запись «недоказанное = разрешение» устарела и пока читается — замените её на «unproven = allow»
42
  • Строковые литералы в записи доказательства печатаются как есть. Раньше пробелы расставлялись и внутри строк: вместо "://" стояло " : //".

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

  • Поиск модуля по имени не выходит выше корня проекта. Корень — ближайший каталог с .flangrc, .git или flang.package. Файл выше корня больше не подменяет модуль проекта или библиотеки; модуль, лежащий только там, не находится.
$ flang check app/main.flang
FLANG_IMPORT_NOT_FOUND в файле app/main.flang, строка 1, столбец 1: не найден модуль «Мера»   код 1

Миграция: перенесите модуль в дерево проекта, ввезите его путём (использует «Мера» из "../mera.flang") или назовите предел поиска переменной FLANG_MODULE_ROOT.

Record fields are checked against their type, and runs have a memory limit

What appeared

  • --memory-limit N (--предел-памяти) — memory cap for a run. Works with any command. check, test and run default to three quarters of the machine's memory; 0 removes the cap. At the cap the run stops with exit code 5 and names the function being evaluated.
$ flang run runaway.flang --function «Раздуть» --args '{"текст":"а","раз":28}' --trust --memory-limit 32M
FLANG_MEMORY: прогон остановлен на пределе памяти 32 МиБ: занято 25 МиБ, просили ещё 25 165 880 байт
  считалась функция «Раздуть», шагов программы 544
                                                                    exit 5

Issue #160.

  • Every proof step names its kernel rule. A step line in a --record file ends with правило «…»; --proof --json has a stepRules field. The independent proof checker compares the name with the rule it applies itself.

What changed

  • A record field is checked against its declared type. A неотрицательное (non-negative) field accepted -7, and the kernel proved a postcondition that the run then violated. Such a program now fails type checking with FLANG_TYPE … поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое, exit 1.
  • flang io: a process that outlives the host timeout is a FLANG_IO_TIMEOUT failure. It used to be reported as «Процесс убит» SIG9, as if killed from outside. --timeout is a silence timeout counted from the last output byte, 30000 ms by default, and is now in flang io --help. Issue #162.
  • The interpreter frees memory on deep recursion. Beyond about 500 nested calls memory was never reclaimed and grew with every step. «Числа до» от 1000 used to hit 3.6 GB and now runs in 370 MB. Issue #160.
  • разделить … по (split) and содержит (contains) in the C runtime find the separator with memchr. On 100 MB of text: split 0.47 → 0.08 s, contains 0.39 → 0.008 s; step counts are unchanged. Issue #161.
  • .flangrc keys are English: language, surface, color, page, version, name, license, repository, issues, unproven. Old keys are still read and name their replacement.
  • String literals are printed verbatim in proof records. Spaces used to be inserted inside strings: " : //" instead of "://".

What broke

  • Module search by name stops at the project root — the nearest directory with .flangrc, .git or flang.package. A file above the root no longer replaces a project or library module, and a module that lives only there is not found (FLANG_IMPORT_NOT_FOUND).

Migration: move the module into the project, import it by path (использует «Мера» из "../mera.flang"), or set FLANG_MODULE_ROOT.

Страница выпусков: по-русски · in English.

Архив flang-0.7.23-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.

Assets 3
Loading