Coq aac_tactics 安装在哪里？

Question

我正在测试 AAC 策略库以重写模关联性和交换性。根据Coq website，应该：

Depending on your installation, either modify the following two lines, or add them to your .coqrc files, replacing "." with the path to the aac_tactics library.

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

但我不知道如何找到 aac_tactics 库的路径，并使用“.”没用。

我按照以下方式在 Ubuntu 16.04 LTS 下安装了 Coq：

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 子目录，这是我们需要添加到上面导入的前缀。

Coq aac_tactics 安装在哪里？

where is Coq aac_tactics installed?

coq

opam

coq-plugin