flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub English

Справочник команд

У двоичного flang двенадцать команд. Здесь каждая: зачем она, как её звать, какие у неё ключи, чем она отвечает и с каким кодом уходит.

Источник этой страницы — сама программа: flang --help и flang <команда> --help.

Шпаргалка

КомандаЧто делаетТипичный вызов
checkРазбор, типы, завершаемость, ядро доказательствflang check привет.flang
testПрогон примеров, объявленных внутри функцийflang test привет.flang
runВычисляет одну функцию и печатает значениеflang run привет.flang --function «Удвоить» --args '{"н":21}'
emitПечатает программу в один из восьми целевых языковflang emit привет.flang --target js --file привет.js
astРазобранная и связанная программа деревом в JSONflang ast привет.flang --pretty
tokensПоток токенов: чем стало каждое слово у лексераflang tokens привет.flang
factsПроверяет утверждения на фактахflang facts привет.flang --facts факты.json --claims '["…"]'
ioИсполняет план: файлы, каталоги, процессы, сетьflang io план.flang --pretty
lockПечатает замок: сами зависимости, а не ссылки на нихflang lock привет.flang > flang.lock
packageПечатает пакет: замок с именем, версией и списком доказанногоflang package привет.flang > привет.flang-package
replИнтерактивная оболочкаflang repl привет.flang
lspЯзыковой сервер для редактораflang lsp --stdio

Общие для всех: flang --help, flang --version, flang <команда> --help.

Входной файл: четыре расширения

Расширений у программы четыре, и все четыре равноправны:

РасширениеОткуда имяГде его набирают
.flangимя языкаосновное: команды, документация, работы CI
.fpfunctional programкороткое, без переключения раскладки
.фп«функциональная программа»чтобы русское имя файла не писать транслитом
.флангимя языка кириллицейто же, длинным словом

Файл берётся по пути, а не по расширению: flang check, run, emit, ast, tokens, lock, package и facts принимают любое из четырёх — и любой другой путь тоже. Решения записаны в docs/adr/0016-three-file-extensions.md и docs/adr/0018-file-extensions-are-one-list.md.

Одно исключение, и его надо знать: flang test, получив ОДИН файл, узнаёт его по .flang — довод с другим расширением он считает каталогом и отвечает «не нашлось ни одного .flang», код 2. Это единственное место компилятора, решающее судьбу файла по расширению, и оно ждёт перепечатки точки раскрутки; до неё примеры файла .фп прогоняются командой flang check, которая их тоже считает.

Коды возврата

Коды одни и те же у всех команд, значение — тоже.

КодЧто значит
0Сделано, замечаний нет
1Программа не прошла — или, у facts и io, сказала «нет» сама
2Неверен вызов: не тот ключ, не то значение, нет файла
3Сделано, но проверено не всё; непроверенное названо поимённо

Код 3 бывает у emit и у io. Различайте 1 и 3 в сборочных сценариях: 1 — работа не сделана, 3 — сделана, но ручаться за всё нельзя.

check

Судит программу: разбор, связывание, типы, завершаемость, ядро доказательств. Это команда, которую вы зовёте чаще всех остальных вместе.

flang check <файл.flang> [--proof [--json] [--записать <файл>]]
                          [--предел-шагов N]
КлючЧто делает
--proofОтчёт: чем несётся обещание «тотальная» у каждой функции и чем — каждое утверждение
--jsonТолько вместе с --proof: тот же отчёт машинным видом
--записать <файл>Только вместе с --proof: положить само доказательство в файл. Ключ пишется и латиницей — --record
--предел-шагов NПоднять предел шагов проверяющего на этот один прогон. Умолчание вшито при сборке и ловит зацикливание; исчерпание остаётся внятным — FLANG_RECURSION_LIMIT с числом. Нужен на самых больших файлах: отчёт о доказательствах --proof --json у модуля в тысячу утверждений в умолчание не укладывается. Латиницей — --step-limit

Коды: 0 — замечаний нет; 1 — программа не прошла; 2 — в программе есть объявления, которых двоичный flang не судит вовсе (категорная поверхность, процессы, надзор), и он называет пробел, а не молчит.

$ flang check привет.flang
модуль «Привет»: функций 1, из них с доказанным завершением 1; типов 0
привет.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Не прошла — место и код называются дословно:

$ flang check плохо.flang
модуль «Плохо»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_TYPE в файле плохо.flang, строка 6, столбец 5: функция «Удвоить» объявлена как строка, а тело даёт число
плохо.flang: не проверено — замечаний 1
$ echo $?
1

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

Известное ограничение. Бюджет шагов у check один на всю команду, а не свой на каждое вычисление. Кончился — команда отвечает FLANG_RECURSION_LIMIT. Ключа, которым этот предел поднимают, у check НЕТ: ни --max-steps, ни любого другого. Большой файл упирается в предел, и обойти это ключом нельзя.

Что делать вместо: прогоняйте flang test <файл> — у примеров бюджет свой, и он задаётся ключом --max-steps. Печать flang emit тоже проходит: она судит программу, но не считает примеры.

test

Прогоняет примеры, объявленные внутри функций. Сначала проверяет программу теми же проверками, что и check: «пример сошёлся» на программе с ошибкой типов не значит ничего.

flang test <файл.flang | каталог | маска> [--no-check] [--json] [--proof report]
                                          [--max-steps N] [--max-depth N]
КлючЧто делает
--no-checkНе проверять программу — смотреть на поведение примеров, пока она ещё в правке
--jsonМашиночитаемый итог одной строкой
--proof reportПо строке на файл, чтобы сверять результаты диффом
--max-steps NПредел шагов вычислителя
--max-depth NПредел глубины

Довод, не кончающийся на .flang, и всякий довод со звездой или вопросом — это набор файлов, а не файл:

flang test flang/stdlib/                весь каталог, вглубь
flang test 'examples/**/*.flang'  по маске (кавычки — от оболочки)

Коды: 0 — взяты все файлы и сошлись все примеры; 1 — что-то не сошлось или файл не взят; 2 — кривой вызов.

$ flang test привет.flang
привет.flang: примеров 1, прошло 1, не прошло 0

У не сошедшегося примера называются обе стороны: ожидалось и получено. Длинное значение обрезается на 200 знаках, и полная длина сказана числом.

run

Вычисляет одну функцию и печатает значение. Считает сам flang — ни Node, ни компилятора C для этого не нужно.

flang run <файл.flang> --function «Имя» [--args '{"н":10}'] [--max-steps N]
                       [--max-depth N]
КлючЧто делает
--function «Имя»Что вычислять. Обязателен
--args '{…}'Аргументы: плоский объект скаляров. Списка и вложенного объекта здесь не принимают
--max-steps NПредел шагов вычислителя
--max-depth NПредел глубины

Аргументы сверяются объявленным типам до вычисления: «Факториал» от −3 отвергается FLANG_TYPE, а не считается.

$ flang run привет.flang --function «Удвоить» --args '{"н":21}'
42

emit

Печатает программу в целевой язык — во все восемь целей, без Node. Каталог из --out заводится сам, вместе с промежуточными и с подкаталогами, которых просит цель.

flang emit <файл.flang> --target c|go|rust|java|js|elixir|python|csharp
                        [--out каталог | --file имя] [--cli|--no-cli] [--repl]
                        [--runtime каталог] [--index-base 0|1]
                        [--max-steps N] [--max-depth N]
КлючЧто делает
--target <цель>c, go, rust, java, js, elixir, python, csharp. Обязателен
--out каталогЗаписать все файлы в каталог
--file имяОдин файл на стандартный вывод
--cli, --no-cliПечатать ли прогонщик
--replНапечатать ещё и человеческий вход. Только для цели c
--runtime каталогГде лежат исходники рантайма цели
`--index-base 0\1`Объявить базу индексов у программы
--max-steps NПредел шагов, попадающий в напечатанный код
--max-depth NПредел глубины
--no-checkНе гонять ядро доказательств. Разбор, типы и завершаемость судятся по-прежнему

Ключ «печатать без проверки» снимает ровно ядро доказательств

Печатается только проверенное. Перед печатью программа судится той же дорогой, что и flang check. Замечание — печать отменена, код 1, ни одного файла не записано.

--no-check снимает из этой дороги ровно ядро доказательств, и больше ничего: разбор, связывание, типы и завершаемость судятся и с ним, и программа, их не прошедшая, не печатается по-прежнему.

Напечатанное с этим ключом не годится в ствол. Без ядра не снимается ни одно доказанное постусловие — в вывод уезжают все, поэтому он толще, отпечаток семени не сойдётся, а собранный из такого семени двоичный поведёт следующую печать медленнее. Перепечатка семени идёт без этого ключа, всегда. Двоичный говорит это вслух после каждой печати с ключом.

Сколько он экономит — число не одно: на flang/self/builtins.flang круг «печать и сборка» идёт 148,8 с без ключа и 18,9 с с ним, а на flang/self/lexer.flang ключ вредит (6,5 против 6,9 с), потому что лишние сторожа дороже обходятся сборке. Главное же не скорость: flang/self/distributed.flang и flang/self/bounded.flang без ключа не печатаются вовсе — ядру не хватает шагов. Подробности и доводы — ADR-0010, поправка 30 августа 2026.

Коды emit и что каждый значит:

КодЧто значит
0Напечатано, пробелов в проверке нет
1Не прошло проверку — не записано ничего
2Неверен вызов: нет такой цели, нет файла, не то значение ключа
3Напечатано, но проверено не всё: категорную поверхность и процессы эта сборка не судит. Непроверенное названо поимённо

Примеры emit не прогоняет, и говорит об этом. Прогоняйте их отдельно — flang test <файл>.

$ flang emit привет.flang --target c --out вывод
напечатано файлов 6, байт 296845, в вывод
аргументы напечатанной программы по типам не проверяются: это ограничение двоичного flang, полная проверка есть в версии для Node
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>

$ ls вывод
Makefile  flang_cli.c  flang_runtime.c  flang_runtime.h  привет.c  привет.h

Цель названа неверно — код 2, и отказ перечисляет все восемь:

$ flang emit привет.flang --target нету
flang emit: цели «нету» у этой сборки flang нет — целей здесь ВОСЕМЬ — «c», «go», «rust», «java», «js», «elixir», «python», «csharp».
$ echo $?
2

ast

Печатает разобранную и связанную программу деревом в JSON — то же самое, что видит печать в целевой язык.

flang ast <файл.flang> [--pretty]
КлючЧто делает
--prettyС отступами в два пробела

Проверок типов и завершаемости здесь нет намеренно: дерево — это то, что прочитано, а не то, что признано годным. Команда отказывает только на том, из чего дерева не выходит вовсе, — на разборе и на связывании.

$ flang ast привет.flang --pretty | head -8
{
  "flang": 1,
  "module": "Привет",
  "types": [],
  "functions": [
    {
      "name": "Удвоить",
      "total": true,

tokens

Печатает поток токенов — то, что прочитал лексер, до разбора и до связывания. Вопрос, ради которого команда есть, один: чем станет это слово, если его написать. Грепом он не решается: слово в комментарии, слово внутри строкового литерала и имя в ёлочках ключевым словом не становятся никогда.

flang tokens <файл.flang> [--json] [--pretty]
flang tokens --keyword «фраза»
КлючЧто делает
--jsonМашинный вид: те же ключи, что у flang astkind, value, text, quoted и span со строкой и столбцом
--prettyС отступами в два пробела; машинный вид включает сам
--keyword «фраза»Ключевое ли это слово. Фраза из нескольких слов проверяется как фраза. Файл при этом ключе не называется

Отказ бывает там же, где отказал сам лексер, — незакрытый литерал, рваный отступ; тогда код 1, а машинный вид всё равно печатается, с пустым tokens и заполненным diagnostics.

$ flang tokens привет.flang | head -4
1:1	слово module
1:8	ёлочка Привет
1:16	/
3:1	слово total

$ flang tokens --keyword 'элемент или беда'
«элемент или беда» — не ключевое слово языка: одним ключевым токеном лексер это не отдаёт

facts

Проверяет утверждения на фактах. Утверждение имеет вид «что-то оператор что-то»; слева бывает факт, поле факта или вызов функции от фактов, справа — то же самое или литерал.

flang facts <файл.flang> --claims '["…"]' [--facts факты.json] [--steps N] [--pretty]
КлючЧто делает
--claims '[…]'Что проверять, JSON-массивом строк. Обязателен
--facts файлФакты JSON-объектом. Без ключа фактов нет
--steps NПредел шагов вычисления. По умолчанию 10000
--prettyJSON с отступами

Коды: 0 — подтверждено; 1опровергнуто, а не «сломалось»: вердикт всё равно уходит в стандартный вывод, и код нужен, чтобы на нём падала сборка; 2 — отказ вызова: не назван файл, не разобран JSON, не связалась программа.

Вызов зовётся только у функции, чьё завершение доказано: нетотальная даёт отказ до всякого вычисления.

$ cat факты.json
{"н": 21}

$ flang facts привет.flang --facts факты.json --claims '["«Удвоить» от н равно 42"]' --pretty | head -7
{
  "ok": true,
  "results": [
    {
      "claim": "«Удвоить» от н равно 42",
      "holds": true,
      "why": "«Удвоить» от факта «н» = 42; требование «равно 42» выполнено",

io

Исполняет план поручений — единственное место языка, где программа встречается с миром. Встречается не сама: каждый шаг возвращает описание действия, а делает его хозяин. Поэтому все функции плана остаются тотальными и проверяются обычными примерами — без файлов и без сети.

flang io <файл.flang> [--plan 'Имя'] [--max-orders N] [--seed N] [--in-dir]
                      [--max-steps N] [--pretty]
КлючЧто делает
--plan 'Имя'Какой план исполнять, если их несколько
--max-orders NПредел поручений за прогон. По умолчанию 10000
--max-steps NПредел шагов вычисления на один виток
--timeout NВремя ожидания одного поручения, миллисекундами. По умолчанию 30000
--seed NСемя случайности: прогон становится повторимым
--in-dirЗапретить пути за пределы каталога входного файла
--prettyJSON с отступами

Имя плана пишется БЕЗ ёлочек, а пробел в нём закрывается кавычками оболочки. Ёлочки — способ языка писать имена в исходнике, но ключ --plan берёт имя как есть, вместе с ними:

$ flang io ярлыки.flang --plan «Целость»
{"error":"не найден план ««Целость»»", … "code":"FLANG_UNKNOWN_PLAN" …}
$ flang io ярлыки.flang --plan Целость
{"plan":"Целость","result":"ярлыков 102; …
$ echo $?
0

Имя из двух слов без кавычек оболочка разбивает на два довода, и до ключа доезжает только первое:

$ flang io flang/scripts/kernel-forgeries.flang --plan «Аксиом ноль»
flang io: непонятный ключ «ноль»»
$ echo $?
2
$ flang io flang/scripts/kernel-forgeries.flang --plan 'Аксиом ноль'
{"plan":"Аксиом ноль","result":"… аксиом ноль, нарушений 0", …
$ echo $?
0

Собственная справка двоичного (flang io --help) пишет при этом --plan «Имя» и тем сбивает: ёлочки в ней — способ показать, что здесь стоит имя, а не часть имени. Справка живёт в flang/self/cli.flang, то есть меняется только перепечаткой семени; до тех пор верная форма записана здесь.

Полномочия сужаются по одному: --no-read, --no-write, --no-net, --no-clock, --no-random, --no-spawn. Умолчание — «можно всё»: запуск программы этой командой и есть согласие на её действия.

Ключа --args у io нет: аргументы плану не передаются — план начинается со своей функции «начинает с», а не с доводов вызова.

$ flang io examples/crypto/revocation.flang --args '{}'
flang io: непонятный ключ «--args»
$ echo $?
2

Время ожидания есть, и это --timeout N, миллисекундами, по умолчанию

  1. До 29 августа 2026 здесь стояло обратное, и показан был отказ, которого

двоичный не печатает: ключ принимается, значение проверяет (--timeout 0 и --timeout abc отвергаются кодом 2), и шестнадцать ярлыков этого же дерева его передают (ярлыки.flang). Сверх него предел прогона задаётся числом поручений и числом шагов.

Коды возврата — контракт: 0 — план дошёл до конца; 1 — программа сдалась сама, то есть нашла беду и назвала её; 2 — кривой вызов; 3 — сломался инструмент. Первое и второе различает не код отказа, а то, кто принял решение.

$ flang io план.flang --pretty
{
  "plan": "Записать привет",
  "result": 6,
  "orders": 1,
  "log": [
    {
      "поручение": {
        "variant": "Записать файл",
        "fields": {
          "путь": "привет.txt",
          "содержимое": "привет"
        }
      },
      "отклик": {
        "variant": "Записано",
        "fields": {
          "сколько": 6
        }
      }
    }
  ]
}

Отняли полномочие — план видит отказ и сдаётся сам, с кодом 1:

$ flang io план.flang --no-write
{"error":"ждали подтверждение записи","diagnostics":[{"code":"FLANG_IO_ORDER","message":"ждали подтверждение записи","severity":"error","span":{"line":38,"column":1}}]}
$ echo $?
1

Чего у двоичного хозяина нет: экрана («Показать», «Ждать событие» отвечают FLANG_IO_NO_SCREEN) и своего шифрования. https у поручения «Запросить» работает, но исполняет его внешняя программа curl: нет её — отказ FLANG_IO_NO_TLS; --no-spawn запрещает и https тоже, отказом FLANG_IO_DENIED. Отзыв сертификата не проверяется ни по OCSP, ни по CRL.

lock

Печатает замок программы — JSON, в котором лежат сами зависимости, а не ссылки на них: у каждого импортированного модуля записан его исходник целиком, а адресом ему служит sha256 по этому исходнику. Склада нет — скачивать неоткуда, потому что всё уже в замке.

flang lock <файл.flang> [--pretty]
КлючЧто делает
--prettyС отступами в два пробела

Если рядом с входным файлом лежит flang.lock, все команды берут импорты из него и исходников зависимостей не читают вовсе. Испорченный замок — отказ FLANG_LOCK, а не тихая сборка из чего попало.

$ flang lock привет.flang
{"схема":2,"вход":"./привет.flang","модули":[],"печать":"dcf9b0c54a6a814573047949d66a78d7e4706c67ae8873e637823fa799609779"}

package

Печатает пакет — тот же груз, что в замке, плюс имя, версия, источник и список доказанного.

flang package <файл.flang> [--pretty]
КлючЧто делает
--prettyС отступами в два пробела

Имя и версию команда берёт из объявления flang.package рядом со входным файлом, а не из ключей вызова. Нет объявления — отказ с кодом 1:

$ flang package привет.flang
FLANG_PACKAGE: рядом с привет.flang нет объявления flang.package: пакету нужны имя и версия, и берутся они оттуда, а не из вызова
$ echo $?
1

Положите рядом flang.package — и пакет собирается:

$ cat flang.package
{"имя": "Привет", "версия": "1.0.0"}

$ flang package привет.flang | cut -c1-96
{"схема":2,"имя":"Привет","версия":"1.0.0","вход":"./привет.flang","модули":[{"имя":"Привет",

Пакет собирается только из проверенного. Как его подключить — на странице Как писать пакеты.

repl

Интерактивная оболочка — то же самое, что голая команда flang на терминале. Объявления накапливаются в сессии, выражения вычисляются сразу, .помощь показывает команды. Файл в аргументе загружается в сессию при запуске.

flang repl [<файл.flang>] [--max-steps N] [--max-depth N]
КлючЧто делает
--max-steps NПредел шагов вычислителя
--max-depth NПредел глубины

Выражение считается так: сессия печатается в C тем же способом, что у flang emit, собирается системным cc и запускается. Нет cc — оболочка не выключается, а проверяет разбор, типы и завершаемость и говорит об этом при запуске:

$ flang repl привет.flang
вычислять нечем: не найден libcompiler_flang.a ($FLANG_LIB_DIR, ../lib или каталог самого бинарника).
Разбор, типы и завершаемость проверяются по-прежнему; выражение отвечает «проверено».
объявлено: тотальная функция «Удвоить» — завершение доказано
загружено из привет.flang

Где искать компилятор C и его окружение: FLANG_CC, FLANG_INCLUDE_DIR, FLANG_LIB_DIR.

lsp

Языковой сервер flang по стандартному вводу-выводу: рамки Content-Length, тело JSON, как требует спецификация LSP. Запускается редактором, а не человеком: вручную он будет молча ждать сообщений.

flang lsp [--stdio]
КлючЧто делает
--stdioГоворить по стандартному вводу-выводу

Умеет: диагностику той же дорогой, что flang check — разбор, связывание, типы, завершаемость, — дополнение, наведение с подписью и переход к объявлению.

Печатать в стандартный вывод что-либо, кроме сообщений протокола, нельзя: редактор читает оттуда рамки. Всё человеческое уходит в поток ошибок.

Проверить, что сервер жив, можно так — послать ему одно сообщение и прочитать ответ:

$ printf 'Content-Length: 104\r\n\r\n{"jsonrpc":"2.0","id":1,"method":"initialize","params":{"processId":null,"rootUri":null,"capabilities":{}}}' | flang lsp --stdio
Content-Length: 311

{"jsonrpc":"2.0","id":1,"result":{"capabilities":{"positionEncoding":"utf-16","textDocumentSync":{"openClose":true,"change":1,"save":{"includeText":false}},"completionProvider":{"triggerCharacters":["«","."]},"hoverProvider":true,"definitionProvider":true},"serverInfo":{"name":"flang-lsp","version":"0.1.0"}}}

Расхождение одно, и оно названо: у программы с использует беда импортированного модуля уходит в журнал редактора, а не подчёркивается в его буфере.

Переменные окружения

ПеременнаяЧто задаёт
FLANG_RUNTIME_DIRГде искать исходники рантайма цели для emit, если не задан --runtime
FLANG_CCКакой компилятор C зовёт repl
FLANG_INCLUDE_DIR, FLANG_LIB_DIRГде repl ищет заголовки и библиотеку

FLANG_RECURSION_LIMIT — это не переменная, а код отказа: так называется исчерпание бюджета шагов.

Дальше