Це команда coqmktop, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
coqmktop - Помічник Coq Proof Assistant для компонування тактики користувача
СИНТАКСИС
coqmktop [ опції ] файли
ОПИС
coqmktop створює новий верхній рівень Coq, доповнений тактикою користувача. файли є Метою
Об’єкт або файли бібліотеки Caml (тобто із суфіксом .cmo, .cmx, .cma або .cmxa) для зв’язування з
Система Coq. Компонувальник створює виконуваний файл Coq верхнього рівня, який можна викликати безпосередньо
Або через coqc(1), використовуючи параметр -image.
ВАРІАНТИ
-h Допоможіть. Перелічіть доступні варіанти.
-srcdir реж
Укажіть, де знаходяться вихідні файли Coq
-o exec-файл
Вкажіть назву отриманого верхнього рівня
-опт Компіляція в рідному коді
-повні Посилання на тактику високого рівня
-поверх Створіть Coq на верхньому рівні ocaml (несумісно з -опт)
-R реж Вкажіть рекурсивно каталоги для Ocaml
-v8 Посилання на граматику V8
Використовуйте coqmktop онлайн за допомогою служб onworks.net
