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