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

Пакеты

Пакет flang — один файл, в котором лежит библиотека вместе со всем, что она импортирует. Кеша пакетов нет, а реестр — список имён, а не склад кода: команды двоичного у него нет, он отвечает адресом. Чтобы опубликовать пакет, закоммитьте файл в git; чтобы им пользоваться, положите файл рядом с программой и напишите одну строку импорта. Для сборки на другой машине нужны только ваша программа и файл пакета, в сеть сборка не ходит никогда.

Работают две команды двоичного flang: flang package собирает пакет, flang lock пишет lock-файл для всей программы. У обеих есть --help. Примеры ниже — на docs/examples/package/.

Подключите пакет

  1. Положите файл пакета рядом со своей программой.
  2. Импортируйте его по имени модуля:
модуль «Shop»
  использует «Скидка» из "discount.flang-package"
  1. Проверяйте и тестируйте как обычно:
$ ls
discount.flang-package  shop.flang

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

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

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

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

$ flang check shop.flang
FLANG_IMPORT_NAME, строка 1, столбец 1: модуль в …/discount.flang-package называется «Скидка», а импортируется как «Скидочка»
shop.flang: не проверено — замечаний 1

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

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

Сделайте свой пакет

Шаг 1. Напишите манифест. Положите flang.package рядом с входным файлом библиотеки:

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

имя и версия обязательны, источник (адрес исходников) — нет. имя обязано совпасть с именем модуля в первой строке входного файла: по этому имени пакет импортируют. Разошлись — flang package отказывает:

$ flang package skidka/discount.flang
FLANG_PACKAGE: в flang.package пакет назван «Не Скидка», а модуль в skidka/discount.flang называется «Скидка»
$ echo $?
1

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

В примере из репозитория именно такое расхождение: модуль в docs/examples/package/discount.flang называется «Discount», а манифест рядом говорит «Скидка». Поэтому flang package docs/examples/package/discount.flang отказывает с FLANG_PACKAGE. Пакет shop/discount.flang-package, с которым работает shop.flang, собран из версии модуля с именем «Скидка».

Шаг 2. Соберите пакет.

$ 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):

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

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

Шаг 3. Опубликуйте. Закоммитьте один файл:

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

Пользователь скачивает этот файл любым способом: прямой ссылкой, из релиза, письмом. Реестра нет, flang publish нет.

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

Если в библиотеке несколько файлов, в пакет попадают все: flang package идёт по импортам от входного файла. Пользователь пакета этого не видит.

У многомодульного примера docs/examples/library-api/lib/ манифеста нет, поэтому flang package docs/examples/library-api/lib/api.flang отвечает FLANG_PACKAGE: рядом с … нет объявления flang.package. Положите flang.package рядом с api.flang — и шаги те же, что выше.

У каждого модуля в пакете есть адрес — sha256 его исходника, 64 шестнадцатеричных знака. При использовании пакета исходник сверяется с адресом, поэтому изменение даже одного байта обнаруживается.

Пакет может импортировать другой пакет:

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

Тому, кто импортирует verh.flang-package, файл discount.flang-package на диске не нужен: он внутри.

Смените версию

Версия живёт в 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
FLANG_PACKAGE: печать пакета «Скидка» не сходится: пакет правлен или испорчен
$ echo $?
1

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

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

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

$ ls
discount.flang-package  shop.flang
$ flang check shop.flang
модуль «Shop»: функций 4, из них с доказанным завершением 4; типов 0; файлов вместе с импортами 2
shop.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

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

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: «адрес модуля «Скидка» не сходится с его исходником: правлен или испорчен»
версиюFLANG_PACKAGE: «печать пакета «Скидка» не сходится: пакет правлен или испорчен»
имя пакетато же, в кавычках — правленое имя
адрес исходниковFLANG_PACKAGE: «печать пакета «Скидка» не сходится: пакет правлен или испорчен»
число функций модуляFLANG_PACKAGE: «печать пакета «Скидка» не сходится: пакет правлен или испорчен»

Контрольная сумма показывает, что файл не правили после сборки. Это не подпись: кто собрал файл, она не говорит.

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

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

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

Lock-файл и пакет

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

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

У программы могут быть одновременно flang.lock и пакеты.

Чего нет

Дальше