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

Пакеты

Пакет flang — это один файл, в котором лежит библиотека вместе со всем, от чего она зависит. Ни реестра, ни хранилища, ни ~/.flang. Опубликовать пакет — закоммитить файл в git; взять чужой — написать одну строку; собрать на другой машине — перенести два файла и запустить flang check.

package и lock есть у flang, поставленного через npm install (четвёртый путь установки, node_modules/.bin/flang). У отдельного двоичного их нет, и он об этом говорит:

$ flang package skidka/discount.flang
flang: неизвестная команда «package». «flang --help» — что умеет бинарник.

Возьмите чужой пакет

Положите файл пакета рядом с программой и напишите одну строку:

модуль «Витрина»
  использует «Скидка» из "discount.flang-package"
$ ls
discount.flang-package  shop.flang

$ flang check shop.flang
{"valid":true,"module":"Витрина","functions":[{"name":"Скидка в копейках","total":true},
 {"name":"Цена за вычетом","total":true},{"name":"Цена в витрине","total":true},
 {"name":"Сколько скинули","total":true}],"types":[],"diagnostics":[]}

$ flang test shop.flang
… "total":7,"passed":7,"failed":0 …

Исходников библиотеки в этом каталоге нет: её функции приехали внутри файла пакета — с примерами, типами и доказательствами. Эти два файла и есть весь проект.

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

$ flang check shop.flang
{"error":"модуль в …/discount.flang-package называется «Скидка»,
 а импортируется как «Скидочка»","diagnostics":[{"code":"FLANG_IMPORT_NAME", …}]}

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

$ flang check shop.flang
{"code":"FLANG_PRECONDITION_CALL",
 "message":"вызов «Скидка в копейках» в функции «Сколько скинули» не снимает
  предусловие «доля не больше ста»: …"}

Объявите свой пакет

Положите flang.package рядом с входным файлом библиотеки — три поля, два из них обязательны:

{
  "имя": "Скидка",
  "версия": "1.0.0",
  "источник": "https://github.com/digitable-lol/flang"
}

имя обязано совпадать с именем модуля в первой строке файла: по этому имени пакет и импортируют. Разошлись — отказ до всякой сборки:

$ flang package skidka/discount.flang
{"error":"в flang.package пакет назван «Не Скидка», а модуль в
 skidka/discount.flang называется «Скидка»", …}

Ни одного нового слова в языке для этого не завелось: skidka/discount.flang — обычный модуль с обычной шапкой модуль / экспортирует.

Соберите пакет

$ flang package skidka/discount.flang > skidka/discount.flang-package

$ ls -la skidka/
-rw-rw-r-- 1 b b 3644 discount.flang
-rw-rw-r-- 1 b b 4343 discount.flang-package
-rw-rw-r-- 1 b b  122 flang.package

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

Пакет — файл JSON. Вот он же, с вырезанным для читаемости грузом (поле адрес в base64):

{
  "схема": 1,
  "имя": "Скидка",
  "версия": "1.0.0",
  "вход": "./discount.flang",
  "модули": [
    { "имя": "Скидка", "путь": "./discount.flang", "функций": 2,
      "печать": "f859823c12859d95a764b801914fdc0e481a3d68e4997e69ff24590570959ea1" }
  ],
  "ведомость": [
    { "функция": "Цена за вычетом",
      "утверждение": "цена за вычетом не выходит за точный потолок",
      "сила": "доказано" }
  ],
  "источник": "https://github.com/digitable-lol/flang",
  "печать": "bac0aa0fc8fe3c0b39885d79bdd628cedf8063fad686d76838b248bd4c7fda13"
}

Поле ведомость — отчёт о доказательствах: что ядро сказало о функциях автора (доказано, сетка N, объявлено, не доказано). Это запись для выбора библиотеки, а не приговор на веру: кто импортирует пакет, доказывает всё заново — тела функций приехали целиком.

Выложите пакет

Закоммитьте один файл:

$ git add skidka/discount.flang-package
$ git commit -m "Скидка 1.0.0"
$ git push

Кто берёт пакет — скачивает этот файл: по прямой ссылке, из релиза, почтой, с флешки. Реестра, куда заливать, нет, и flang publish нет.

Библиотека из нескольких модулей

Если библиотека — несколько файлов, едут все:

$ flang package examples/library-api/lib/api.flang > api.flang-package
$ ls -la api.flang-package
-rw-rw-r-- 1 b b 13161 api.flang-package

Замыкание идёт по рёбрам импорта и выходит за каталог библиотеки, если автор так написал: catalog.flang тянет «Списки» из "../../../flang/stdlib/lists.flang", и lists.flang едет вместе со всеми. Кто пользуется пакетом, знать об этом не обязан.

Груз не сжимается. Адрес модуля — sha256 его исходника, 64 знака, и груз сверяется с ним при использовании пакета: поменяйте байт — поменяется адрес.

Пакет может стоять на пакете:

verh.flang            использует «Скидка» из "discount.flang-package"
verh.flang-package    держит и «Верх», и «Скидка»

У того, кто импортирует verh.flang-package, никакого discount.flang-package на диске нет, и flang check его не ищет: он едет грузом внутри.

Закрепите версию

Версия живёт в flang.package и покрыта печатью пакета. Поднять её — поправить манифест и пересобрать:

$ sed -i 's/"версия": "1.0.0"/"версия": "1.1.0"/' skidka/flang.package
$ flang package skidka/discount.flang --pretty | grep '"версия"'
  "версия": "1.1.0",

Править версию внутри собранного пакета бессмысленно: печать пересчитывается при чтении и не сойдётся.

$ sed -i 's/"версия":"1.0.0"/"версия":"9.9.9"/' vitrina/discount.flang-package
$ flang check vitrina/shop.flang
{"error":"печать пакета «Скидка» не сходится: пакет правлен или испорчен", …}

Диапазонов версий (^1.2, ~> 1.2) нет. Программа получает ровно тот файл, который рядом с ней положили, и обновиться сам он не может.

Соберите без сети

Флага для этого нет, и он не нужен. Сборка не ходит в сеть: качать нечего, код уже в файле.

$ ls
discount.flang-package  shop.flang
$ flang check shop.flang
{"valid":true,"module":"Витрина", …}

Это же и ответ на «соберётся ли на другой машине»: перенесите два файла — и соберётся. Чтобы убедиться, что пакет даёт то же, что исходники, напечатайте программу дважды и сравните каталоги:

flang emit shop.flang --target c --out ./from-package   # где лежит пакет
flang emit shop.flang --target c --out ./from-sources   # где лежат исходники
diff -r ./from-package ./from-sources && echo одинаково

Как читается испорченный пакет

Что подменилиОтвет
один знак в грузе модуляFLANG_PACKAGE: «груз модуля «Скидка» в пакете «Скидка 1.0.0» не разворачивается»
версиюFLANG_PACKAGE: «печать пакета «Скидка» не сходится»
имя пакетаFLANG_PACKAGE: «печать пакета не сходится»
адрес источникаFLANG_PACKAGE: «печать пакета не сходится»
число функций модуляFLANG_PACKAGE: «печать пакета не сходится»

Печать покрывает всё, что пакет говорит о себе: имя, версию, источник и число функций каждого модуля. Это не подпись — она отвечает «файл не правили», а не «файл от того, о ком вы думаете».

Два пакета, привёзшие один путь модуля с разным содержимым, названы прямо:

FLANG_PACKAGE: путь …/obshee.flang привезли два пакета с разным содержимым:
  «Библиотека а 1.0.0» и «Библиотека б 1.0.0». Двух версий одной библиотеки
  в одной программе не бывает: поднимите обе стороны до одной версии

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

Замок и пакет

Оба кладут код внутрь файла, и их легко перепутать.

flang lockflang package
отвечает на«из чего собрана ЭТА программа»«вот библиотека, берите»
имя и версиянетобязательны
как используетсялежит рядом, зовётся flang.lockпишется как использует … из "…"
сколько на программуодинсколько угодно
печать покрываетгрузгруз, имя, версию, источник, число функций

Друг другу они не мешают: у программы могут быть и flang.lock, и пакеты.

Чего нет

Куда дальше