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

Каталог примеров

Все примеры-программы на flang лежат в одном каталоге — docs/examples/: 348 файлов в двадцати пяти наборах и одном полноразмерном проекте. Второго каталога с примерами в репозитории нет.

Число пересчитывается одной командой: git -c core.quotepath=false ls-files docs/examples | grep -c '\.flang$' → 348.

Наборы

КаталогФайлов .flangПро что
leetcode/82решения задач LeetCode; каждый файл самодостаточен нарочно — почему, сказано в index.json. Разбор этого набора — 82 задачи
rosetta/28канонические задачи Rosetta Code, каждая на русской и на английской поверхности языка. Разбор набора — Rosetta Code
web/13HTTP: служба заказов, сокращатель ссылок и API маркетплейса из трёх служб — каталог, корзина, заказы
io/10поручения ввода-вывода: двоичный файл туда и обратно, октеты по проводу, потомок, запрос по HTTPS, временный каталог, разбор пакета, полоса на экране терминала
crypto/8AES, ECDSA, X25519, X.509, список отзыва, привет TLS — на настоящих контрольных векторах, которые лежат рядом
library-api/7предметная половина REST-сервиса библиотеки: выдача книг, каталог, штрафы. Единственный набор, показывающий раскладку проекта целиком
db/6разговор с PostgreSQL (в том числе SCRAM), с Redis и чтение файла SQLite
service-on-processes/4служба на процессах, а не пример на три функции: заявление о своей замене OTP, проверенное в полный рост
behavior/4бизнес-правила для таблицы поведения и её диффа: доступ к отчёту в двух версиях и рефакторинг, скидка от суммы. Рассказ — таблица поведения правила
frameworks/6ядро решения на flang под хозяином-фреймворком на JavaScript: NestJS, React, Vue. Ядро напечатано в JS и лежит рядом с хозяином — см. ниже
https/3TLS: записи RFC 8448, системное хранилище доверия, привет настоящему узлу
proof-probes/3пробы самого ядра доказательств: дверь к типизированному дереву, отказ от общего спуска, вариант с полями
driver/2драйверы железа там, где каждая функция обязана доказано завершаться: UART и MSI
measure/3завершаемость по объявленной мере: Евклид, двоичный поиск, натуральные числа
errors/2отказ значением, а не падением: итог столбца пришедших строками чисел, разбор чисел
surfaces/2факториал на китайской и эсперанто-поверхности языка
wal/2журнал упреждающей записи: разбор, печать, восстановление после обрыва
monad/1итог заказа на форме в монаде
money/1деньги на точном десятичном типе сотых
paths/1кратчайший путь по сети с недостижимыми узлами
allocator/1распределитель памяти как чистый автомат: можно ли написать malloc на flang и что про него возьмёт ядро
host-boundary/1стык: flang считает решение, хозяин на C исполняет — напечатано в C, собрано системным cc, прогнано целиком
service/1обращение к службе
import-check.flang1проба связывания модулей по имени

Как прогонять

Примеры объявлены внутри функций, а не в отдельных файлах проверок, и прогоняются двоичным:

bootstrap/flang test docs/examples/rosetta/   # один набор
bootstrap/flang test docs/examples/           # весь каталог

Наборы считаются очень по-разному, и это стоит знать до запуска. На общей машине: leetcode — 82 файла, 806 примеров, около 14 секунд; crypto — 8 файлов, 1802 примера (своих 77, остальные — из модулей библиотеки, которые набор подключает), около 19 минут, потому что считает настоящие контрольные векторы AES и ECDSA. Файл, который двоичный не взял, он называет вместе с кодом отказа, а не пропускает молча.

Про library-api

library-api стоит в этом ряду особняком. Остальные наборы — программы: файл, а в нём объявления со своими примерами (у frameworks/ рядом с такими файлами лежит хозяин на TypeScript, см. ниже). library-api — проект: семь модулей на flang, из них один свой, со своей раскладкой каталогов. Пример показывает не HTTP, а границу: что уезжает в язык, где у куска логики есть выполняемый пример, и что остаётся хозяину. Хозяина в дереве нет: остаётся половина на flang, и она проверяется командой. Правила, выведенные из этой раскладки, собраны в Раскладке репозитория.

Под JS-фреймворками

docs/examples/frameworks/ — три приложения с одной границей: ядро логики написано на flang и напечатано в JavaScript (bootstrap/flang emit … --target js), а хозяин — JS-фреймворк. Хозяин держит сокет, HTTP, состояние формы и рендер, а решение зовёт у ядра. Признак границы тот же, что у docs/examples/host-boundary/ с хозяином на C: на flang пишется то, что решает; хозяину остаётся то, что ждёт и держит управление между решениями.

КаталогХозяинЯдроЧто решает ядро
docs/examples/frameworks/nestjs-orders/NestJScore/orders-api.flangREST-служба заказов: разбор строки запроса, обязательные поля, маршрут по методу и пути, код ответа (201/200/400/404/405)
docs/examples/frameworks/react-invoice/Reactcore/cart.flang, core/catalog.flangсчёт корзины целым числом копеек: сумма, ступени скидки, итог, строки счёта
docs/examples/frameworks/vue-roman/Vuecore/roman-numerals.flangримские цифры туда и обратно в диапазоне 1..3999
docs/examples/frameworks/react-ts-pure/React + TypeScriptcore/storefront.flangвитрина, где в компонентах ноль строк логики: корзина, ступени скидки, запись рублей и редьюсер — всё на flang

Напечатанный модуль лежит в printed/ каждого примера и самодостаточен: без зависимостей, идёт и в Node, и в браузере. Хозяин импортирует его напрямую (src/orders.controller.ts, src/App.tsx, src/App.vue). Значения на стыке: список → массив, запись → объект; записи строятся фабриками sozdat… из объектов с русскими ключами. Имена функций — транслитерация русских: «Обработать запрос» → obrabotatZapros, «Сумма корзины» → summaKorziny, «В римские» → vRimskie.

Что проверено на дереве: каждое ядро проходит bootstrap/flang check; у кода в printed/ стоит шапка с лицензией и командой переиздания; напечатанный модуль отвечает верно под node прямым вызовом:

cd docs/examples/frameworks/vue-roman && node --input-type=module -e \
  'import("./printed/roman_numerals.js").then(m => console.log(m.vRimskie(2024), m.izRimskih("MCMLXXXIV")))'
# MMXXIV 1984

Сборка хозяина — командами фреймворка из package.json каждого примера: npm install, npm run typecheck, npm run build. На дереве она не проверяется: ей нужны пакеты из сети. node_modules/ и dist/ в примеры не входят. Переиздать ядро — из корня дерева, например bootstrap/flang emit docs/examples/frameworks/vue-roman/core/roman-numerals.flang --target js --out docs/examples/frameworks/vue-roman/printed; файлы в printed/ печатает компилятор, руками их не правят.

Куда идти дальше