Це команда coqide, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
coqide - графічний інтерфейс Coq Proof Assistant
СИНТАКСИС
coqide [ опції ]
ОПИС
coqide це графічний інтерфейс gtk для помічника Coq proof.
Про використання Coq, орієнтованого на командний рядок, див coqtop(1) ; щодо пакетного використання Coq див
coqc(1).
ВАРІАНТИ
-h Показати повний список варіантів, які приймає coqide.
-I реж, -включати реж
Додайте каталог dir у шлях включення.
-R реж coqdir
Рекурсивно відображати фізичне реж до логічного coqdir.
-src Додайте вихідні каталоги в шлях включення.
-є f, -вхідний стан f
Читати стан з f.coq.
- шум Почніть з порожнього стану.
- вихідний стан f
Записати стан у файл f.coq.
-load-ml-object f
Завантажити об’єктний файл ML f.
-load-ml-source f
Завантажити файл ML f.
-l f, -load-vernac-source f
Завантажте файл Coq f.v (Завантажити f).
-лв f, -load-vernac-source-verbose f
Завантажте файл Coq f.v (дослівне завантаження f).
-load-vernac-object f
Завантажте об’єктний файл Coq f.vo.
-вимагають f
Завантажте об’єктний файл Coq f.vo та імпортуйте його (потрібно f).
-компілювати f
Скомпілювати файл Coq f.v (припускає - партія).
-компілювати-багато f
Детально компілюйте файл Coq f.v (припускає - партія).
-опт Запустіть версію Coq або Coq_SearchIsos з рідним кодом.
-байт Запустіть версію байт-коду Coq або Coq_SearchIsos.
-де Роздрукуйте стандартне розташування бібліотеки Coq і вийдіть.
-v Роздрукуйте версію Coq і вийдіть.
-q Пропустити завантаження rc-файлу.
-ініціальний файл f
Встановіть файл rc f.
- партія Пакетний режим (виходить відразу після розбору аргументів).
- черевик Режим завантаження (мається на увазі -q та - партія).
-emacs Повідомляє Coq, що він виконується під Emacs.
- dump-glob f
Дамп глобалізацій у файл f (для використання coqdoc(1)).
-імприкативний-набір
Встановити сортування Встановити непредикативне.
-незавантаження
Не завантажуйте непрозорі докази в пам'ять.
-xml Експортуйте файли XML або в ієрархію, вкорінену в каталозі
COQ_XML_LIBRARY_ROOT (якщо встановлено) або на стандартний вихід (якщо не встановлено).
Використовуйте coqide онлайн за допомогою служб onworks.net