В Coq необходимо ли добавлять текущий каталог в путь загрузки для доступа к скомпилированным файлам для импорта или экспорта?

Question

Я недавно переключился с Windows на Mac, и теперь CoqIde ведет себя не так, как я привык.Я использую Coq 8.9.1, и я не помню версию, которую я использовал, но это было последнее обновление осенью 2018.

На моей старой машине я мог скомпилировать файл (например, file1.vполучить file1.vo и file1.glob), а затем импортировать или экспортировать его в другой файл в том же каталоге (например, записав Require Export file1.) без изменения пути загрузки.Теперь мне нужно явно добавить текущий каталог в путь загрузки, или я получаю сообщение об ошибке «Невозможно найти библиотеку ...».

Это ожидаемое поведение?Я был вдали от Coq некоторое время, но я почти уверен, что раньше мне не приходилось это делать.Добавление текущего каталога в путь загрузки не входит ни в одну из моих старых работ.Есть ли способ всегда иметь текущий каталог в пути загрузки?

Я прочитал этот вопрос и ответы, но предложения там выглядят так, как будто все они сводятся к добавлению любого каталога, который яя работаю по пути загрузки (либо в файле, над которым я работаю, либо где-то еще).

Обновление:

Мне удалось получить решениеоткрытия из терминала в месте расположения файла для работы (в результате чего путь к текущему файлу находится в LoadPath), но это было больше головной боли, чем я привык в Windows.

Мне пришлосьнапишите небольшой скрипт Bash в ~ / bin / coqide, который просто вызывает /Applications/CoqIDE_8.8.0/Contents/MacOS/coqide.При добавлении символической ссылки в каталог бинарных файлов моего домашнего пользователя не удалось найти файлы, которые, как ожидается, будут относительно места, где была названа символическая ссылка.

Мне не удалось получить второе решение, использующее файл _CoqProject для работы вCoqIde и в конечном итоге увидел странное поведение.Компиляция из терминала с использованием coqc работала.

Я добавил это в систему отслеживания проблем Coq GitHub (см. здесь и здесь ).

Answer 1

Когда вы открываете файл с CoqIDE, он не найдет другие файлы, от которых вы зависите, относительно местоположения файла, который вы открыли, но относительно местоположения, где вы открыли CoqIDE (см. Также https://github.com/coq/coq/issues/5124).

Так что одним из возможных решений является то, которое я упомянул в своем комментарии выше (откройте CoqIDE из консоли, где находятся ваши файлы). Но, к счастью, есть другое решение, которое я бы порекомендовал, как только вы работаете над проектом с несколькими файлами, и которое имеет преимущество в том, что позволяет открывать CoqIDE так, как вам хочется: это использовать файл _CoqProject.

Так что просто создайте файл _CoqProject, где бы ни находились ваши файлы Coq, только с этой строкой:

-R . MyProjectNamespace

и тогда все должно работать магическим образом (при условии, что вы перекомпилируете все файлы).