2017-06-09 61 views
0

我正在使用Coq(版本8.5-6),安裝w/Nix。我想安裝ssreflect,最好也是w/Nix。我發現的唯一信息是here。但是,這不是關於安裝ssreflect,只是嘗試它。儘管如此,我試圖嘗試一下,但最終得到了數百個警告(關於各種文件的內容.v.ml4),並且不能等待該過程結束。一個相當典型的警告是這樣的:Nix:安裝ssreflect

文件 「./algebra/ssralg.v」,線路856字符0-39:警告: 隱參數已被棄用;使用參數,而不是

所以現在的問題:如何在地球上我安裝 ssreflect W /尼克斯?

編輯:在閱讀ejgallego的評論後,似乎可能不可能安裝ssreflect w/Nix - esp。如果只想安裝ssreflect w/out其他模塊(fingroup,代數等)。所以我也有以下問題:

請問standard Opammake install安裝ssreflect工作w /一個NIX安裝Coq?

+2

這些警告是可悲的是正常的,因爲開發商沒有固定的他們。 ssreflect需要花費時間來構建,特別是如果你想構建整個包和它的許多庫。您可以編輯ssreflect的Make來刪除一些庫,或者只是將包分開。 這取決於您的需求,例如,由於OPAM的大小,OPAM將數學comp分發爲5個獨立的包。 – ejgallego

+1

如果你打算只使用戰術插件,它被包含在隊列8.7中,但是請注意,如果沒有至少它的主庫,戰術真的不是很有用。 – ejgallego

回答

2

還有,你需要知道的幾件事情:

  • 尼克斯是一個二進制緩存基於源的包管理器。很多軟件包是預先構建的,並且可以在二進制緩存中使用,因此它們的安裝不需要很長時間;一些軟件包(特別是開發庫)不是預先構建的,而Nix在安裝時需要花費時間編譯它們。請耐心等待:您只需等待第一次完整編譯(是的,編譯時數學comp會發出很多警告);下一次,該軟件包將在您當地的Nix商店中提供。

  • 由於OPAM也是基於源代碼的,所以使用OPAM代替Nix不會節省時間。你不能混用Nix安裝的Coq和OPAM安裝的SSReflect,因爲後者會希望前者作爲OPAM依賴。

  • Nix使用庫的方式不是安裝它們,而是使用nix-shell來代替它們。 nix-shell將「安裝」庫併爲您設置一些環境變量(例如,在這種情況下爲$COQPATH)。

  • 您也可以使用Nix安裝的Coq自己編譯軟件包,但無法運行make install,因爲這會嘗試在安裝Coq的同一位置安裝SSReflect,但Nix存儲區不可變。相反,您可以跳過此步驟,並手動設置$COQPATH

  • 事實上,編寫完整的數學comp需要很長的時間。有一個較輕的Coq ssreflect軟件包。你可以使用獲得它:

    nix-shell -p coqPackages_8_6.ssreflect 
    
+0

「Nix使用庫的方式不是安裝它們,而是使用nix-shell來加載它們。」謝謝,這解釋了很多 – jaam

+0

瞭解這一點花了我很長時間。特別是在Coq的情況下,因爲我沒有把它當作一種編程語言來思考。 –

+0

我有一個[新問題](https://stackoverflow.com/questions/44553350/nix-querying-packages-packages)與此相關 – jaam