Где установлен Coq aac_tactics?

Question

Я тестировал библиотеку тактик AAC на предмет переписывания по модулю ассоциативности и коммутативности. Согласно веб-сайту Coq, нужно:

В зависимости от вашей установки, измените следующие две строки или добавьте их в файлы.coqrc, заменив "." с путем к библиотеке aac_tactics.

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

Но я не знаю, как найти путь к библиотеке aac_tactics и использовать "." не работал

Я установил Coq под Ubuntu 16.04 LTS следующим образом:

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 подкаталог, который является префиксом, который нам нужно было добавить к нашему импорту выше.