Це команда coqdep, яку можна запустити в постачальнику безкоштовного хостингу OnWorks за допомогою однієї з наших численних безкоштовних робочих станцій, таких як Ubuntu Online, Fedora Online, онлайн-емулятор Windows або онлайн-емулятор MAC OS
ПРОГРАМА:
ІМ'Я
coqdep - Розрахувати міжмодульні залежності для програм Coq і Caml
СИНТАКСИС
coqdep [ -w ] [ -I каталог ] [ -coqlib каталог ] [ -c ] [ -i ] [ -D ] [ - коса частина ]
ім'я файлу ... каталог ...
ОПИС
coqdep обчислює міжмодульні залежності для програм Coq і Caml і друкує файл
залежності від стандартного виводу у форматі, доступному для читання make. Коли каталог є
наведений як аргумент, він рекурсивно розглядається.
Залежності модулів Coq обчислюються шляхом перегляду Вимагати команди (Вимагати, Вимагати
Експорт, Вимагати імпорту), Декларуйте ML Модулі команди і Навантаження команди. Залежності
відносно модулів з бібліотеки Coq не друкуються.
Залежності модулів Caml обчислюються, дивлячись на відкрити директиви та крапка
позначення модуль.значення.
ВАРІАНТИ
-c Друкує залежності модулів Caml. (У модулях Caml така поведінка
точно так само, як ocamldep).
-w Друкує попередження, якщо команда Coq Декларуйте ML Модулі є неправильним. (Наприклад,
ви написали `Оголосити модуль ML "A".', але модуль A містить #open "B"). The
надруковано правильну команду (див. опцію -D). Попередження надруковано на стандарті
помилка
-D Ця команда шукає кожну команду Декларуйте ML Модулі кожного файлу Coq, зазначеного як
аргумент і заповніть (якщо потрібно) список модулів Caml. Нова команда
надруковано на стандартному виході. За допомогою цієї опції не обчислюється жодна залежність.
- коса частина Друкує шляхи з використанням косої риски замість роздільника, специфічного для ОС. Цей варіант є
корисно при розробці під Cygwin.
-I каталог
Файли .v .ml .mli каталогу каталог враховуються під час
обчислення залежностей, але їхні власні залежності не друкуються.
-coqlib каталог
Вказує, де знаходиться бібліотека Coq. Значення за замовчуванням визначено в
час встановлення, і тому цей параметр не слід використовувати у звичайному режимі
обставини.
Використовуйте coqdep онлайн за допомогою служб onworks.net
