Це команда coqchk, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн емулятор Windows або онлайн емулятор MAC OS
ПРОГРАМА:
ІМ'Я
coqchk - перевірка скомпільованих бібліотек Coq Proof Checker
СИНТАКСИС
coqchk [ опції ] Модулі
ОПИС
coqchk є автономною перевіркою скомпільованих бібліотек (файлів .vo, створених coqc) для
помічник Coq Proof Assistant. Додаткову інформацію див. у Довідковому посібнику. Воно повертається з
код виходу 0, якщо всі запитані завдання виконані успішно. Ненульовий код повернення означає це
щось пішло не так: деяку бібліотеку не знайдено, пошкоджений вміст, перевірка типу
невдача тощо.
Модулі це список модулів, які потрібно перевірити. На модулі можна посилатися за допомогою короткого або
кваліфіковане ім'я.
ВАРІАНТИ
-I реж., --включати реж
додати каталог реж у шляху включення
-R реж coqdir
рекурсивно відображати фізичні реж до логічного coqdir
- мовчазний
робить coqchk менш багатослівним.
- зізнатися Модулі
позначте вказаний модуль і всі його залежності як надійні, і не буде
перевірено повторно, якщо цього явно не вимагають інші варіанти.
-норек Модулі
вказує, що даний модуль має бути перевірений без запиту на його перевірку
залежності.
-м, --пам'ять
відображає підсумок пам'яті, яку використовує засіб перевірки.
-о, --контекст вихідних даних
відображає підсумок логічного змісту, який було перевірено: припущення та
використання непредикативності.
-імприкативний-набір
дозволяє засобу перевірки приймати бібліотеки, які були скомпільовані з цим прапором.
-v роздрукувати версію coqchk і вийти.
-coqlib реж
замінює стандартне розташування стандартної бібліотеки.
-де print coqchk стандартна бібліотека розташування та вихід.
-h, --допомога
роздрукувати список опцій
Використовуйте coqchk онлайн за допомогою служб onworks.net
