Coq aac_tacticsはどこにインストールされていますか？

Question

私はモジュロの結合性と可換性を書き直すためにAACの戦術ライブラリをテストしていました。 Coq websiteによると、一つはすべき：インストールに応じ

、次の2行、 を変更したり、.coqrcファイルに追加し、交換のどちらか「」 aac_tacticsライブラリへのパスは です。

Add Rec LoadPath "." as AAC_tactics. 
Add ML Path ".". 
Require Import AAC. 
Require Instances. 

しかし、私はaac_tacticsライブラリへのパスを見つけ、そして使用する方法がわかりません「」うまくいかなかった。

私はの線に沿って16.04 LTSのUbuntuの下にコックをインストール：

opam repo add coq-released https://coq.inria.fr/opam/released 
opam install coq-mathcomp-ssreflect.1.6 
opam install coq-aac-tactics.8.5.1 

誰がどこライブラリの場所を見つけるために知っていますか？

Answer 1

（少なくともこのチュートリアルのために）動作しますようです：

(* 
Add Rec LoadPath "." as AAC_tactics. 
Add ML Path ".". 
*) 
Require Import AAC_tactics.AAC. 
Require Import AAC_tactics.Instances. 

通常、OPAMは~/.opamにそのようなものを格納します。あなたのターミナルで次のコマンドでそれを見ることができます：

$ opam config var root 

その後、あなたはスイッチ（それはOCamlのコンパイラの異なるバージョンを維持するための主だ）と呼ばれる複数の構成を持つことができます。現在のスイッチのルートは、この方法で見つけることができます：

$ opam config var prefix 

を、現在のスイッチのためのライブラリは、あなたがここに調べることができますどのディレクトリに保存されています

あり

$ opam config var lib 

あなたは見つけることができますAAC_tacticsサブディレクトリ。これは上記のインポートに追加する必要があるプレフィックスです。