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

Я тестировал библиотеку тактик 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

Кто-нибудь знает, где найти библиотеку?


coq coq-plugin opam
person tinlyx    schedule 24.06.2016    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Кажется, это сработает (по крайней мере, для этого урока):

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

person Anton Trunov    schedule 24.06.2016