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

Question

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

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