Coq makefile "Top". Префикс
Я использую автоматический генератор make-файлов Coq 8.5. Этот makefile ставит перед всеми модулями префикс "Top"., Теперь предположим, что вы запускаете много файлов по make, а затем хотите изменить / отладить некоторый файл в IDE. Тогда раздражает тот факт, что Coq жалуется, что не может найти скомпилированные другие файлы, потому что в IDE он принимает имена без префикса "Top". Я попытался настроить make-файл, чтобы избавиться от этого префикса. Но я всегда заканчивал каким-то сообщением об ошибке. Может ли кто-нибудь показать мне, как удалить префикс "Top" в make, или указать IDE использовать префикс "Top".
2 ответа
Вы можете запустить CoqIDE со следующими аргументами coqide -R . Top,
Это избавит от следующей ошибки Error: The file ..../Logic.vo contains library Top.Logic and not library Logic,
Это действительно раздражает. Чтобы избежать такого раздражения, всегда начинайте _CoqProject с вариантами списка строк:
-Q . MyProject
Примечание: варианты, которые вы можете поставить в первой строке вашего _CoqProject те, которые указаны при звонке coqtop -help,