Я не могу загружать модули, которые находятся в одной папке в CoqIde.
Я пытаюсь загрузить источники из Software Foundations, я запускаю coqide в папке, содержащей источники SF с coqide или coqide ./, после открытия и запуска файла я получаю эту ошибку:
Error: Cannot find library Poly in loadpath
в этой строке:
Require Export Poly.
а также для всех других команд require.
Итак, как вы, люди, загружаете программы из SF в coqide?
Вам нужно скомпилировать файлы .v в файлы .vo и добавить их каталог в свой путь загрузки, если вы собираетесь их требовать. Чтобы скомпилировать их, запустите coqc <file-path> в командной строке. Чтобы добавить каталог файлов в ваш путь загрузки в CoqIde, вы можете вставить строку Add LoadPath "<directory-path>". в начале .v файлов.
Я понимаю, что это старый поток, однако ресурсов по этой проблеме недостаточно. Я просто потратил некоторое время на его решение, поэтому решил, что было бы неплохо опубликовать его на первой теме, которую я получил от googling. Я использую Coq 8.4p16, скомпилированный без дополнительной настройки в Arch Linux.
Итак, в руководстве указано, что переменные, такие как $COQPATH, ${XDG_DATA_DIRS}/coq/ и ${XDG_DATA_HOME}/coq/, отмечены, однако мне не повезло с ними.
Я также попробовал поставить coqc -I /folder/path Edit->Preferences->Externals в CoqIde, но пока не везет.
Я пишу их, поскольку они могут работать для кого-то.
Единственный GLOBAL-способ, который работает для меня, - это записать файл coqrc с Add LoadPath "<directory-path>". в нем. В Linux файл должен находиться в домашней папке.
Надеюсь, что это кому-то поможет.
Чтобы иметь возможность загружать исходный файл в coqtop, coqc, CoqIDE или Proof General, существует несколько способов, один из которых заключается в следующем:
Предположим, что вы загрузили файлы кода для книги под названием Certified Programming with Dependent Types, написанные Adam Chlipala, которые доступны здесь и извлеките их в путь, который мы называем CODEHOME. Как вы можете видеть, есть первая строка в любых исходных файлах Require Import Bool Arith List Cpdt.CpdtTactics.
Первый тип coqc -v в cli (интерфейс командной строки), результат будет чем-то вроде The Coq Proof Assistant, version 8.4pl4 ...., затем создайте файл с именем coqrc.8.4pl4, расширение файла должно быть в согласитесь с версией используемого coq в каталоге $HOME/.config/coq, если он не существует, и напишите в нем эту строку Add LoadPath "CODEHOME/cpdt/src" as Cpdt . и это.
Если вы начали свой file.v с Module file., просто избавитесь от него (также избавитесь от End file.), и ваша проблема решена.
В соответствии с этим: https://github.com/coq/coq/issues/3995#issuecomment-337530500
Использование coqc -R '' '' работает в CoqIDE, хотя вам все равно нужно сначала скомпилировать отпечатки. Но самое неприятное: использование coqtop -R '' '' приведет к тому, что CoqIDE не запустится, мне пришлось отредактировать $HOME/AppData/Local/coq/coqiderc (в Windows), изменить его на cmd_coqtop = "coqtop".