1

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

根据您的安装，修改以下两行，或将它们添加到您的 .coqrc 文件中，替换“。” 带有 aac_tactics 库的路径。

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

有谁知道在哪里可以找到图书馆的位置？

4

1 回答 1

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

于 2016-06-24T18:15:39.843 回答