Инструмент: команды flang и контракт вывода

Прежде чем разбирать синтаксис, нужен инструмент, который скажет, правы вы или нет. У flang это один двоичный файл flang: компилятор написан на самом flang, напечатан в C и собран. Ни Node, ни другой среды для работы не нужно. Всё ниже прогнано на выпуске 0.7.29 — готовой сборке для Linux x86_64.

Установка

С выпуска 0.7.29 у каждого выпуска есть готовые сборки: Linux x86_64 и aarch64 (статические, под любой дистрибутив), macOS arm64 и x86_64. Пакет называется flang-package, команда — flang.

Скрипт install.sh выбирает сборку под систему, сверяет архив с SHA256SUMS выпуска и кладёт его в ~/.local без sudo; версию задаёт переменная FLANG_VERSION=0.7.29, место — PREFIX. Без установки язык можно попробовать в браузере: на странице playground работает тот же компилятор, собранный в WebAssembly.

Одна ловушка с именем: компилятор Фортрана из LLVM тоже ставит команду flang (формула flang в Homebrew, пакет flang в Fedora). Какой из двух вызовется, решает порядок в PATH. Проверка — первая строка flang --version:

$ flang --version
flang 0.7.29

Что лежит в готовой сборке

Архив flang-package-0.7.29-linux-x86_64.tar.gz весит 38 МБ в распакованном виде:

$ ls bin share/flang
bin:
flang  flangtutor

share/flang:
c  cpp  csharp  elixir  go  java  js  python  rust  stdlib  ts

flang — компилятор, flangtutor — пошаговый учебник в терминале (уроки лежат в share/flang-tutor). share/flang/stdlib — стандартная библиотека: с 0.7.29 программа из любого каталога может написать использует «Lists» только «Длина», и библиотека найдётся. Остальные каталоги — рантаймы десяти целевых языков для flang emit.

Чего в готовой сборке 0.7.29 нет — проверено запуском:

• независимой проверяющей программы. flang check --proof заканчивает отчёт строкой «НЕЗАВИСИМО НЕ ПРОВЕРЕНО»: программа на C, которая перепроверяет доказательства, в архив не входит, её собирают из клона (make -C flang/proof/checker) и называют переменной FLANG_CHECKER;
• вычисления в оболочке. flang repl при запуске пишет «вычислять нечем: не найден flang_runtime.h … не найден libcompiler_flang.a» и дальше только проверяет объявления и выражения, не считая их. Двоичный, собранный в клоне (make -C bootstrap), считает: 2 плюс 3 даёт 5;
• английских сообщений. FLANG_LANG=en flang check … отвечает «no message catalog was found … answering in Russian»: каталог сообщений лежит в клоне, в flang/messages, и подключается переменной FLANG_MESSAGE_DIR;
• образца для flang new. Команда отвечает FLANG_NEW: не найден образец fspec/ и пакет не создаёт; с FLANG_FSPEC_TEMPLATE_DIR=<клон>/fspec работает.

Пятнадцать команд

flang --help перечисляет пятнадцать команд, у каждой есть своя справка flang <команда> --help. Голый flang на терминале — та же оболочка, что flang repl.

Отдельно от команд есть ключ --mcp-mode: тот же компилятор как служба для ИИ-помощника по протоколу MCP (средства flang_check, flang_prove и другие — flang --mcp-mode --help).

Ниже везде одна и та же программа, сохранённая как проба.flang:

модуль «Проба»

тотальная функция «Удвоить»
  принимает н: неотрицательное
  возвращает число
  обеспечивает «не меньше исходного» результат не меньше н
  пример «два»
    дано н равно 2
    ожидается 4
  н плюс н

check

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

Пример внутри функции прогоняется при каждой проверке. Если ожидание неверно, check отвечает кодом 1 и называет обе стороны:

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

Ключи, которые стоит знать:

• --proof — отчёт о доказательствах: чем доказано завершение каждой функции и чем держится каждое утверждение. Слова отчёта разные по смыслу: «доказано» — для всех входов; «сетка N» — посчитано на N значениях, это не доказательство; «объявлено, не доказано» — утверждение есть, доказательства нет. Разбор — в главе «Тотальность»;
• --proof --json — тот же отчёт машинным видом; без --proof ключ --json отвергается кодом 2: «без отчёта о доказательствах печатать в JSON нечего»;
• --proof --strict — исходы разведены кодами: 0 — все утверждения доказаны (и хотя бы одно есть), 1 — опровергнуто, 3 — что-то держится только на примерах или не доказано, 2 — не поддерживается;
• --proof --record <файл> — записать само доказательство в файл, чтобы его перепроверила отдельная программа;
• --fast — только связывание, типы и завершаемость, без ядра и примеров. Код возврата 4 — «часть проверок не запускалась», и об этом сказано словами.

$ flang check проба.flang --proof | tail -1
проба.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1, условно 0, сетка 0, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 0

На стандартной библиотеке тот же ключ показывает, что «проверено» и «доказано» — разные ответы: flang/stdlib/lists.flang проходит check с кодом 0, а check --proof отвечает кодом 3 — «утверждений 66: доказано 42, … сетка 24».

test

$ flang test проба.flang
проба.flang: примеров 1, прошло 1, не прошло 0
$ flang test проба.flang --json
{"valid":true,…,"files":1,"taken":1,"refused":0,"total":1,…,"passed":1,"failed":0,…}

Сначала программа проходит те же проверки, что в check: пример, сошедшийся на программе с ошибкой типов, ничего не значит. Довод, который не кончается на .flang, или маска со звёздочкой — набор файлов: flang test flang/stdlib/ обходит каталог вглубь. С 0.7.29 test исполняет и сценарии процессов прогон (глава «Синтаксис»).

run

$ flang run проба.flang --function Удвоить --args '{"н": 21}'
доказано: утверждений 1
42
$ flang run проба.flang --function Удвоить --args '{"н": -3}'
доказано: утверждений 1
FLANG_TYPE: вызов функции «Удвоить»: аргумент «н»: -3 вне неотрицательное

Перед вычислением run считает вердикт по всей программе вместе с импортами и пишет его строкой в поток ошибок. Аргументы сверяются с объявленными типами до вычисления. Программу, у которой есть недоказанное утверждение, run не запускает и отвечает кодом 3; запустить её всё же можно ключом --trust (по-русски --на-веру) или раз и навсегда ключом unproven в .flangrc. --args принимает только плоский объект скаляров — список так не передать, для этого пишут функцию-обёртку.

facts

Проверка утверждений на фактах. Утверждение — строка <терм> <оператор> <терм>; терм — факт, поле факта, вызов функции от фактов или литерал. Вызывать можно только функцию с доказанным завершением.

модуль «Факты»

тотальная функция «Сумма больше порога»
  принимает суммы: список из число, порог: число
  возвращает признак
  (свёртка суммы начиная с 0 как акк и ч → акк плюс ч) больше порог

$ cat факты.json
{"суммы": [1, 2], "порог": 10}
$ flang facts факты.flang --facts факты.json \
    --claims '["«Сумма больше порога» от суммы, порог равно да"]'
{"ok":false,"results":[{"claim":"«Сумма больше порога» от суммы, порог равно да","holds":false,
 "why":"«Сумма больше порога» от факта «суммы», факта «порог» = нет, а утверждение требует «равно да». …",
 "steps":[…],"status":"refuted"}]}
$ echo $?
1

Код 1 здесь значит «опровергнуто», а не «сломалось»: вердикт уходит в stdout, код нужен, чтобы на нём падал CI. Массив steps — след разбора, проверки завершения и вычисления. Подробно — в главе «Факт-чекинг».

emit

Перевод программы в целевой язык. Целей десять, и печатается только проверенное: перед выводом программа проходит те же проверки, что в check, и при замечании не пишется ни одного файла.

$ flang emit проба.flang --target python --out py
…
напечатано файлов 4, байт 101845, в py
…
$ ls py
Makefile  flang_cli.py  flang_runtime.py  proba.py
$ flang emit проба.flang --target zzz
flang emit: цели «zzz» у этой сборки flang нет — целей здесь ДЕСЯТЬ — «c», «cpp», «go», «rust», «java», «js», «ts», «elixir», «python», «csharp».

Примеры при этом не прогоняются — перед выводом стоит запустить flang test. --max-steps и --max-depth здесь вписывают пределы в выведенную программу, а не в текущий прогон. Разбор целей — в главе «Кодогенерация».

ast и tokens

flang ast печатает разобранную и связанную программу деревом в JSON — то, что получает кодогенерация. Типы и завершаемость здесь не проверяются: дерево — это то, что прочитано. flang tokens показывает, чем стало каждое слово у лексера, а --keyword отвечает на частый вопрос «можно ли так назвать переменную»:

$ flang ast проба.flang | head -c 120
{"flang":1,"module":"Проба","types":[],"functions":[{"name":"Удвоить","total":true,"params":[{"name":"н","type":{"kind":
$ flang tokens --keyword "код символа"
«код символа» — ключевое слово, конструкция «charCode»

io

Единственная команда, которая трогает внешний мир. Программа объявляет план: тип состояния, начальную функцию и функцию шага. Шаг возвращает не результат действия, а его описание — «прочитать такой-то файл»; flang io исполняет действие и вызывает шаг снова с откликом. Поэтому все функции плана остаются тотальными и проверяются обычными примерами, без файлов и без сети. Устройство — в главе «Синтаксис».

Прогон примера из репозитория языка, который читает файл и считает в нём строки:

$ cd docs/examples/guide
$ flang io read-file.flang --in-dir --pretty
доказано: утверждений 0
{
  "plan": "Сосчитать строки",
  "result": 3,
  "orders": 1,
  "log": [
    {
      "поручение": {
        "variant": "Прочитать файл",
        "fields": {
          "путь": "words.txt"
        }
      },
      "отклик": {
        "variant": "Прочитано",
        "fields": {
          "содержимое": "раз\nдва\nтри\n"
        }
      }
    }
  ]
}

log — полный журнал: что программа попросила и что ей ответили. Права сужаются ключами --no-read, --no-write, --no-net, --no-clock, --no-random, --no-spawn, --no-env, --no-args, --no-screen; --in-dir запирает пути в каталоге файла, --seed N делает случайные числа повторимыми. Запрет приходит программе отказом FLANG_IO_DENIED (с --no-read этот прогон кончается кодом 1). Коды возврата io: 0 — план дошёл до конца, 1 — программа сдалась сама и назвала причину, 2 — кривой вызов, 3 — сломался инструмент или план не доказан. Запрос по https с 0.7.27 выполняет клиент TLS 1.3, написанный на flang, без curl.

Программы-сценарии с планом принято хранить в файлах .fscript — это тот же язык, другое расширение; запускаются они той же командой flang io.

lint, lock, package, new, run-script

• flang lint [путь…] меряет длину строк и глубину вложенных если/разбор; пределы — ключами или в .flangrc. Без пределов ничего не меряет и говорит об этом: max-line-length: без предела.
• flang lock программа.flang > flang.lock кладёт в один JSON исходники всех импортированных модулей с их sha256. Если рядом лежит flang.lock, команды берут импорты из него, а испорченный замок — отказ FLANG_LOCK.
• flang package — то же плюс имя, версия и отчёт о доказанном; подключается строкой использует «Строки» из "strings.flang-package". Собирается только из проверенного.
• flang new имя заводит каталог пакета: модуль с функцией и примером, манифест flang.package, каталог fspec/ со спецификацией.
• flang run-script имя исполняет строку script.имя = … из ближайшего .flangrc; без имени печатает перечень.

repl

$ flang repl
…
Оболочка flang.

Объявление вводится в несколько строк; пустая строка заканчивает ввод:
…
Команды (строка с точки — точкой не может начаться ни одна конструкция языка):
  .помощь                    эта справка
  .объявления                что объявлено в сессии
  .исходник                  исходник сессии целиком
  .сохранить <файл>          записать исходник сессии в файл
  .загрузить <файл>          добавить объявления из файла .flang
  .сбросить                  забыть всё объявленное
  .силлогизм [<файл>]        рассудить текст: …
  .очистить                  очистить экран
  .выход                     закончить работу
По-английски: .help .list .source .save .load .reset .syllogism .clear .quit

Объявление проходит ту же проверку, что в check, и не прошедшее в сессию не попадает. Команда начинается с точки, потому что с точки не начинается ни одна конструкция языка — путать нечего. С 0.7.29 в оболочке можно писать утверждение, теорема и следует: она зовёт check --proof --strict и отвечает «доказано», «опровергнуто» с контрпримером или «не доказано». Выражение оболочка считает так: печатает сессию в C, собирает системным cc и запускает. Нет cc или рантайма — выражение только проверяется (см. выше про готовую сборку).

Языковой сервер

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

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

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

Настройки для Vim и VS Code лежат в репозитории, в docs/editors/.

Контракт вывода

• По умолчанию вывод — для человека: строка итога и замечания с кодом FLANG_*, файлом, строкой и столбцом.
• JSON — там, где он нужен программе: facts и ast всегда, test --json, check --proof --json, io (с --pretty — с отступами), lsp и --mcp-mode.
• Код возврата: 0 — всё в порядке; 1 — программа не прошла проверку, пример не сошёлся или утверждение опровергнуто; 2 — ошибка вызова (нет файла, неизвестный ключ или команда); 3 — недоказанное без согласия на запуск; 4 — check --fast, часть проверок не запускалась; 5 — исчерпан предел памяти.

Коды диагностик и форма JSON на версиях 0.x — то, на что можно опираться в скриптах; синтаксис языка пока не заморожен.

Входной файл

Исходник — файл .flang (принимаются и .fp, .фп, .фланг); файл с другим расширением читается как исходник flang. Стандартного ввода у check нет: flang check - отвечает «непонятный ключ «-»». Чтение старых моделей FTS разобрано в главе «Старые модели».

Дальше — глава «Синтаксис по факту».