Это команда coqmktop, которую можно запустить в провайдере бесплатного хостинга OnWorks, используя одну из наших многочисленных бесплатных онлайн-рабочих станций, таких как Ubuntu Online, Fedora Online, онлайн-эмулятор Windows или онлайн-эмулятор MAC OS.
ПРОГРАММА:
ИМЯ
coqmktop - компоновщик пользовательских тактик Coq Proof Assistant
СИНТАКСИС
Кокмктоп [ кредита ] файлов
ОПИСАНИЕ
Кокмктоп создает новый верхний уровень Coq, расширенный пользовательскими тактиками. файлов являются целью
Файлы объекта или библиотеки Caml (т.е. с суффиксом .cmo, .cmx, .cma или .cmxa) для связи с
Система Coq. Компоновщик создает исполняемый файл верхнего уровня Coq, который можно вызывать напрямую.
Или через кокс(1), используя параметр -image.
ДОПОЛНИТЕЛЬНЫЕ УСЛУГИ, НЕ ВКЛЮЧЕННЫЕ В ПАКЕТ
-h Помощь. Перечислите доступные варианты.
-srcdir директория
Укажите, где находятся исходные файлы Coq
-o exec-файл
Укажите название получившегося верхнего уровня
-опт Компилировать в машинном коде
-полный Свяжите тактику высокого уровня
-верхняя Build Coq на верхнем уровне ocaml (несовместимо с -опт)
-R директория Рекурсивно указать каталоги для Ocaml
-v8 Связь с грамматикой V8
Используйте coqmktop онлайн с помощью сервисов onworks.net
