Agda可以在批處理模式下更快地編譯？

當我編譯使用標準庫的阿格達程序，編譯器花費很長的時間打印出線路如：Agda可以在批處理模式下更快地編譯？

Skipping Relation.Binary.Consequences (/home/owen/install/lib-0.6/src/Relation/Binary/Consequences.agdai). 
Skipping Relation.Binary.Indexed.Core (/home/owen/install/lib-0.6/src/Relation/Binary/Indexed/Core.agdai). 
Skipping Relation.Binary (/home/owen/install/lib-0.6/src/Relation/Binary.agdai).

我猜它安全地「跳過」他們的理由是，他們已編譯（目錄中已有.agdai文件）。但它仍然花費大量時間跳過它們，編譯花費的時間不止一分鐘。

有沒有辦法在每次編譯時避免所有這些額外的工作？

來源

2012-03-15 Owen

通過編譯你的意思是生產一個可執行文件或只是typechecking？ – Saizan 2012-10-21 01:15:56

@saizan好問題。我認爲只需進行類型檢查就足夠了，因爲它是最重複的任務。雖然生成一個可執行文件也很好。 – Owen 2012-10-21 04:42:00

Agda和其他類似的coq軟件系統有交互界面可用，通常通過安裝在emacs中的Proof General。

模塊化編譯在其他上下文中起作用，因爲編程語言傾向於依賴對外部符號的淺名稱檢查，如果它們檢查的話。 Agda是一個證明系統，所以如果它要完成它的工作，它必須每次都從頭開始，並深入驗證整個證明。

來源

2012-09-16 21:41:46 NovaDenizen

嗯....我想我並不是在尋找模塊化編譯，我只是喜歡在編輯器之外的命令行中運行編譯器;即因爲Agda可以在emacs中快速重新檢查類型，如果它可能作爲惡魔運行......你明白我的意思了嗎？ – Owen 2012-10-21 04:45:02

Agda必須將至少一些.agdai文件加載到內存中，以便能夠檢查自己的代碼，這可能是爲什麼即使跳過檢查這些模塊仍需要一些時間。

來源

2012-10-21 01:18:58 Saizan

Agda可以在批處理模式下更快地編譯？

回答

相關問題