在當前環境中未找到參考「X」

我正在使用CoqIDE完成軟件基礎本手冊中關於Coq的練習。我可以成功編譯Basics.v，在我的目錄中生成Basics.vo和Basics.glob。當我嘗試運行Induction.v時，它可以工作。當我嘗試編譯它時，它會抱怨大量缺失的引用，如evenb和negb_involutive。如果我將Basics.v內容複製到Induction.v中，它會進行編譯，但顯然這不是要走的路。在當前環境中未找到參考「X」

這不是問題Coq error: The reference evenb was not found in the current environment的副本，因爲我已經做了那些事：

編譯Basics.v。檢查Basics.vo是否在目錄中。現在編譯Induction.v。最後一步失敗。

來源

2016-10-19 RaptorDotCpp

我剛剛嘗試了它（下載了SF的全新副本，並從CoqIDE中的菜單進行編譯），但沒有發現任何錯誤。你能解釋一下你做了什麼嗎？你有哪個Coq版本？我有8.5pl2。 – larsr

我已經解決了Basics.v和Induction.v中的所有內容。我有和你一樣的版本。也許我應該嘗試編譯「空白」版本。我會回報。 – RaptorDotCpp

@larsr我也下載了新鮮的副本。我打開CoqIDE，打開Basics.v然後編譯它。這是成功的。當我然後打開Induction.v並嘗試編譯它時，我得到了和以前一樣的錯誤。所以即使是新鮮的副本似乎並沒有在我的系統上編譯。我正在使用Mac OS X El Capitan。 – RaptorDotCpp

我自己也經歷過這個錯誤。嘗試從Software Foundations文件所在的同一目錄打開CoqIDE，然後從那裏進行編譯。如果你在Linux上，只需打開一個終端，進入該目錄，然後在那裏輸入coqide。我不太清楚在其他系統上如何做到這一點，例如Mac OS，但我注意到只是通過圖標打開應用程序會導致失敗。

來源

2016-10-19 13:46:36

我可以確認從macOS上打開同一個目錄下的CoqIDE：cd ; /應用程序/ CoqIDE_8.5.app /目錄/ MacOS/coqide' –

我也開始從命令行coqide，同時在sf目錄內。 – larsr

在當前環境中未找到參考「X」

回答

相關問題