coqIDE неправильно соединяет файлы в проекте и не компилирует - PullRequest
Новая
       70

coqIDE неправильно соединяет файлы в проекте и не компилирует

0 голосов
/ 19 января 2020

Я новичок в использовании coq / coqIDE, и я не разбираюсь в компьютерах, поэтому я не знаю, что не так или как назвать проблему. Я пытался go через книгу «Основы программного обеспечения», но coqIDE не работает правильно. Я использую последнюю версию windows 10 и coqIDE 8.10.2

Первая проблема заключается в том, что когда я go перехожу на вкладку compile -> compile buffer в Basics.v, coqIDE не создает .vo файл или .glob. Ни одна из других кнопок не работала. Запуск coqIDE от имени администратора также не помог, но я понял, что могу обойти это, вручную перетащив Basics.v в файл приложения coq c.

У меня не было проблем с работой coq во время первый урок, но на следующем уроке мы должны импортировать определения из Basics.v в Induction.v, когда я запускаю то, что они говорят 

From LF Require Export Basics.

Я получаю ошибку The file C:\Users\...\Coq Files\Tutorial\lf\Basics.vo contains library Basics and not library LF.Basics, даже если файл _CoqProject содержит «-Q. LF», как и должно быть.

Я тоже могу обойти эту ошибку, просто написав «Требовать основы экспорта». который корректно загружается, пока я не попытаюсь вызвать определение из Basics

Запуск 

Require Export Basics.
Example example: evenb 2 = true.

работает, пока я не доберусь до evenb, а затем выдаст ошибку The reference evenb was not found in the current environment., даже если она находится в Basics.v

Если я получу еще более анальный и попробую 

Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
From LF Require Export Basics.

Я получу ошибку 

Cannot find a physical path bound to logical path matching suffix <> and prefix LF.

И, наконец, если я попытаюсь 

Add LoadPath "C:\Users\...\Coq Files\Tutorial\lf".
Require Export Basics.
Example example: evenb 2 = true.

Загружается правильно.

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

Некоторые люди говорили о «ударе по макету на верхнем уровне», но я понятия не имею, что это значит. Я все равно попробовал и запустил Makefile как .bat, хотя я уже скачал его правильно, так что в этом не должно быть никакой необходимости, но Makefile ничего не изменил.

Не думаю, что я забыл что-нибудь, заранее спасибо.

1 Ответ

0 голосов
/ 20 января 2020

Вместо того, чтобы выбирать Compile > Compile buffer, попробуйте вместо этого Compile > Make (при просмотре любого из местных файлов в логических основах) - я думаю, что это то, что другие подразумевали под "нажатием make на верхнем уровне". Но сначала вы можете удалить обходные пути, добавленные вами, например, Induction.v, и сохранить тривиальное изменение в Basics.v, такое как добавление / удаление новой строки где-нибудь, чтобы убедить make перекомпилировать ее.

...