compatibility.vo содержит библиотеку Top.comparable, а не библиотеку, сопоставимую

Question

Я очень плохо знаком с Coq.

В нашем проекте мы перешли на использование утилиты coq_makefile и столкнулись со следующей проблемой.

Выполнение сценария проверки приведет к эта ошибка:

Require Import comparable.

Error:
The file /Users/ayman/open-source/regex-reexamined-coq/comparable.vo contains library
Top.comparable and not library comparable

Наш _CoqProject файл очень прост (возможно, в этом проблема), он просто перечисляет все файлы в проекте https://github.com/awalterschulze/regex-reexamined-coq/blob/2c865aecc00276e0a926c1729cc35553c1cc6767/_CoqProject.

Answer 1

Библиотеки Coq имеют логический путь. Например, все файлы из стандартной библиотеки имеют логический путь, начинающийся с Coq. В вашем случае вы ничего не указали относительно логического пути, поэтому Coq произвольно помещает скомпилированные файлы в путь, начинающийся с Top. Позже, при попытке загрузить файл, Coq сравнивает логический путь Top с физическим путем . и жалуется на несоответствие.

Самое простое решение - добавить следующую строку в _CoqProject файл: -R . Top. Опция -R отображает физический путь (здесь .) на логический путь (здесь Top), который исправит несоответствие.

Но Top - плохое имя для библиотеки, поэтому Вы должны заменить это чем-то другим. Более того, это имя будет служить путем установки вашей библиотеки, поэтому выберите значимое имя (например, RegexDerivatives), так как это имя будет использоваться пользователями.