我無法加載位於CoqIde中同一文件夾中的模塊。coqide - 無法從同一文件夾加載模塊
我試圖從軟件基金會加載來源，我跑在包含有coqide或coqide ./ SF sources文件夾coqide，然後打開並運行該文件後，我得到這個錯誤：
Error: Cannot find library Poly in loadpath
在這一行：
Require Export Poly.
和它的同每隔require命令。
那麼你們如何從SF加載程序到coqide？
如果你需要它們，你需要將.v文件編譯成.vo文件並將它們的目錄添加到你的加載路徑。要編譯它們，請在命令提示符下運行coqc <file-path>。要將文件的目錄添加到CoqIde中的加載路徑中，可以在.v文件的開頭插入行Add LoadPath "<directory-path>".。
我知道這是一箇舊的線程，但是在這個問題上沒有太多的資源。我只是花了一些時間解決問題，所以我認爲將它發佈在Google搜索的第一個主題上會很好。我在Arch Linux上使用Coq 8.4p16編譯而沒有額外的配置。
因此，手冊中說像$COQPATH, ${XDG_DATA_DIRS}/coq/和${XDG_DATA_HOME}/coq/這樣的變量已被檢查，但是我沒有運氣。
我也嘗試過coqc -I /folder/path CoqIde的Edit->Preferences->Externals，但是，那裏仍然沒有運氣。
我寫這些，因爲他們可能爲某人工作。
對我來說唯一的GLOBAL方式是在其中寫入一個Add LoadPath "<directory-path>".的coqrc文件。在Linux上，文件需要位於主文件夾中。
希望這節省了一些人的時間。
如果您使用coqIDE（命令行總是有效），這將起作用。我希望coqIDE會自動將當前PWD添加到加載路徑，但事實並非如此。 – 2016-09-19 16:28:06
似乎可能有一種方法可以使用_CoqProject來實現此功能，但我不確定如何： http://coq-club.inria.narkive.com/q5jGTrgk/configuring-coqide-using-coqproject – Blaisorblade 2016-10-19 14:59:39
對我來說也是一樣：coqc cli tool'works使用coqrc文件的唯一方法，但我在2016年12月8.6版的x64 win7下。 – valaxy 2017-02-08 06:47:13
如果你開始file.v與Module file.只是擺脫它（也擺脫End file.），你的問題就解決了。
爲了能夠加載coqtop，coqc，CoqIDE一個源文件或證明一般有幾種方式，一種方法如下：
假設你已經下載的代碼文件名爲認證的編程書與依賴類型由Adam Chlipala編寫，可用here並在我們稱之爲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 .就是這樣。
根據此： https://github.com/coq/coq/issues/3995#issuecomment-337530500
使用在CoqIDE，coqc -R '' ''工作雖然你仍然需要先編譯DEPS。但最令人沮喪的是，使用coqtop -R '' ''將導致CoqIDE無法啓動，我不得不編輯$HOME/AppData/Local/coq/coqiderc（在Windows上），將其更改回cmd_coqtop = "coqtop"。
是否有Coq加載路徑環境變量？ – 2015-06-30 05:42:09
@GregoryNisbet是的，COQPATH：https：//coq.inria.fr/refman/Reference-Manual016.html#sec587 – Langston 2017-01-27 20:18:25