Запуск проверенного байткода

Используйте Native CLI. ВМ Лиспекса выполняет скомпилированный и проверенный байткод Лиспекса. Руководство Core IR объясняет промежуточный файл из этого примера.

Подготовьте исходник и ввод

Сохраните всё правило как heading-core.lspx.

(define (место-заголовка осталось-строк)
  (if (< осталось-строк 2) 'следующая-страница 'оставить))

(место-заголовка input)

Сохраните входное значение как request.lspx.

1

Команда передаёт это значение в input. Core IR и байткод записывают требование explicit-input.

Создайте два файла

lispex core-ir build --source heading-core.lspx --out heading-core.lpxir
lispex bytecode build --ir heading-core.lpxir --out heading-core.lpxbc

Обе команды завершаются с кодом 0 и печатают JSON-отчёты с execution: "not-run". Первая сохраняет heading-core.lpxir. Вторая читает его и сохраняет heading-core.lpxbc. Выбирайте новые пути назначения. Если файл уже существует, команда завершается с кодом 3. Если вы уже прошли руководство Core IR, используйте готовый .lpxir и выполните только вторую команду.

Первый отчёт содержит core_ir_build: "lispex.core-ir-build/v1". Второй содержит bytecode_build: "lispex.bytecode-build/v1". Отчёты описывают сохранённые файлы.

Просмотрите и проверьте байткод

lispex bytecode inspect --bytecode heading-core.lpxbc
lispex bytecode validate --bytecode heading-core.lpxbc

Обе команды завершаются с кодом 0. inspect печатает JSON-отчёт со следующими значениями.

Отчёт также содержит идентификаторы исходника, Core IR и байткода, число инструкций по видам и позиции в исходнике. Все 22 инструкции связаны с позицией в исходнике. validate печатает отчёт с bytecode_validation: "lispex.bytecode-validation/v1" и valid: true.

Выполните с вводом

lispex bytecode run --bytecode heading-core.lpxbc --input request.lspx

следующая-страница

Команда завершается с кодом 0. Одна оставшаяся строка меньше двух, поэтому результат равен следующая-страница. Native проверяет весь файл байткода до создания состояния VM и использования ввода.

В этом примере пропуск --input приводит к E300 для несвязанной переменной input и коду завершения 1. Передача ввода байткоду без такого требования приводит к коду 2. Справочник байткода перечисляет правила проверки и пределы.

Один поток стандартного ввода может передавать либо байткод, либо входное значение. Следующая команда завершается с кодом 2 и печатает в stderr указанную диагностику.

lispex bytecode run --bytecode - --input -

lispex bytecode run: bytecode and input cannot both read stdin

Передайте один из объектов через именованный файл.

Выполните непосредственно из исходника

Для запуска исходника и сравнения движков сохраните эту полную программу как rule.lspx. Она передаёт 1 внутри программы и печатает решение с помощью display и newline.

(define (место-заголовка осталось-строк)
  (if (< осталось-строк 2) 'следующая-страница 'оставить))
(display (место-заголовка 1))
(newline)

lispex run --backend rust --engine vm rule.lspx
lispex run --backend rust --engine tree rule.lspx

Каждая команда печатает следующая-страница с переводом строки и завершается с кодом 0. По умолчанию используется движок Лиспекса tree. Движок vm компилирует и проверяет программу в памяти перед выполнением.

При явном выборе vm ошибки компиляции, проверки, ресурсов и выполнения возвращаются от выбранного движка. Повторного запуска через tree нет. Параметр --engine работает только с --backend rust. Сочетание с реестром внешних реализаций считается ошибкой использования и даёт код 2. Текущие способы выполнения описаны в справочнике движков.

Прочитайте отчёт сравнения движков

lispex compare-engines --receipt tree-vm.json rule.lspx

Native создаёт tree-vm.json, печатает следующую сводку и завершается с кодом 0.

{
  "all_agree": true,
  "receipt": "tree-vm.json",
  "schema": "lispex.compare-engines-summary/v1",
  "semantic_mismatch_axes": []
}

Оба движка записывают следующая-страница\n в stdout и успешно завершаются. Поле all_agree: true означает совпадение проверенных семантических результатов. Пустой массив semantic_mismatch_axes показывает, что различий не обнаружено.

Откройте tree-vm.json и прочитайте observations.tree, observations.vm и semantic_mismatch_axes. Отчёт также содержит идентификаторы исходника, Core IR и байткода, расход ресурсов VM и счётчики запасных способов выполнения. Native записывает полный отчёт по новому пути за один шаг. Если tree-vm.json уже существует, команда завершается с кодом 3 и не изменяет его. Этот JSON нужен для сравнения. VM принимает файл .lpxbc.

Продолжите с Ваучером Лиспекса

Справочник байткода описывает проверки верификатора и сравнение с ВМ Лиспекса.

Ваучер Лиспекса принимает исходник профиля csk.checked-profile/v1 для скомпилированного контейнера. Приведённое правило размещения заголовка не соответствует этому профилю, и vouch compiled build отклоняет его с кодом 1. Подготовьте подходящий исходник и контейнер по отдельному примеру Ваучера в справочнике.