Ссылка "X" не найдена в текущей среде

Question

Я использую CoqIDE для выполнения упражнений в книге "Основы программного обеспечения" о Coq. Я могу успешно скомпилировать Basics.v, в результате чего в моем каталоге появятся Basics.vo и Basics.glob. Когда я пытаюсь запустить Induction.v, это работает. Когда я пытаюсь скомпилировать его, он жалуется на тонны отсутствующих ссылок, таких как evenb а также negb_involutive, Если я копирую содержимое Basics.v в Induction.v, оно компилируется, но, очевидно, это не тот путь.

Это не дубликат вопроса Coq error: Ссылочная чётка не была найдена в текущей среде, так как я уже сделал эти вещи:

Основы компиляции. Проверьте, находится ли Basics.vo в каталоге. Теперь скомпилируйте Induction.v. Этот последний шаг терпит неудачу.

Answer 1

Я испытал эту ошибку сам. Попробуйте открыть CoqIDE из той же директории, где находятся файлы Software Foundations, и скомпилировать оттуда. Если вы работаете в Linux, просто откройте терминал, перейдите в этот каталог и введите coqide там. Я не совсем знаю, как это сделать на других системах, например, Mac OS, но я заметил, что простое открытие приложения с помощью значка приводит к сбою.