6
Я использую CoqIDE для выполнения упражнений в книге Software Foundations о Coq. Я могу успешно скомпилировать Basics.v, в результате чего Basics.vo и Basics.glob в моем каталоге. Когда я пытаюсь запустить Induction.v, он работает. Когда я пытаюсь скомпилировать его, он жалуется на тонны недостающих ссылок, например evenb и negb_involutive. Если я скопирую содержимое Basics.v в Induction.v, он скомпилируется, но, очевидно, это не путь.Ссылка «X» не найдена в текущей среде
Это не дублирует вопрос Coq error: The reference evenb was not found in the current environment, как я уже делал эти вещи:
Compile Basics.v. Проверьте, находится ли файл basics.vo в каталоге. Теперь скомпилируем Induction.v. Этот последний шаг не удался.
Я попробовал это сейчас (скачал новую копию SF и скомпилировал из меню внутри CoqIDE), и у меня не было никаких ошибок. Не могли бы вы объяснить немного больше, что вы делаете? Какая версия Coq у вас есть? У меня есть 8.5pl2. – larsr
Я решил все внутри Basics.v и Induction.v. У меня такая же версия, как и вы. Возможно, мне стоит попробовать скомпилировать «пустые» версии. Я отчитаю. – RaptorDotCpp
@larsr Я также загрузил новую копию. Я открыл CoqIDE, открыл Basics.v, а затем скомпилировал его. Это было успешно. Когда я открыл Induction.v и попытался скомпилировать его, я получил ту же ошибку, что и раньше. Поэтому даже свежая копия, похоже, не компилируется в моей системе. Я использую Mac OS X El Capitan. – RaptorDotCpp