查看所有已安装的库以及如何在Coq中导入这些库

Question

我一直想使用coq-vpl，而且我已经安装好了。我可以从opam list确认这一点

ubuntu@ubuntu-xenial:~$ opam list
# Installed packages for system:
...
coq                    8.6  Formal proof management system.
coq-vpl                0.2  Coq interface to VPL abstract domain of convex polyhedra.
coq-vpltactic          0.2  A Coq Tactic for Arithmetic (based on VPL).
coqide                 8.6  IDE of the Coq formal proof management system.
...

但是，我如何找出该库的实际名称以及我需要导入的内容？vpl页面上没有文档。

Answer 1

你可以运行

coqc -config

以获取配置变量的列表。在我的系统上，这给出了

LOCAL=0
COQLIB=/home/jgross/.local64/coq/coq-8.7.1/lib/coq/
DOCDIR=/home/jgross/.local64/coq/coq-8.7.1/share/doc/coq/
OCAMLFIND=/home/jgross/.opam/system/bin/ocamlfind
CAMLP4=camlp5
CAMLP4O=/home/jgross/.opam/system/bin/camlp5o
CAMLP4BIN=/home/jgross/.opam/4.02.2/bin/
CAMLP4LIB=/home/jgross/.opam/system/lib/camlp5
CAMLP4OPTIONS=-loc loc
CAMLFLAGS=-thread -rectypes -w +a-4-9-27-41-42-44-45-48-50 -bin-annot -safe-string
HASNATDYNLINK=true
COQ_SRC_SUBDIRS=config dev lib kernel library engine pretyping interp parsing proofs tactics toplevel printing intf grammar ide stm vernac plugins/btauto plugins/cc plugins/derive plugins/extraction plugins/firstorder plugins/fourier plugins/funind plugins/ltac plugins/micromega plugins/nsatz plugins/omega plugins/quote plugins/romega plugins/rtauto plugins/setoid_ring plugins/ssr plugins/ssrmatching plugins/syntax plugins/xml

如果您查看COQLIB提供的路径的user-contrib目录，您应该会看到包含已安装的各种库的文件夹。对于这些文件夹名称中的任何一个，都可以将From FolderName Require Import FileName添加到您的Coq文件中。

Answer 2

根据https://github.com/VERIMAG-Polyhedra/VplTactic的说法，您需要运行coq，例如，通过启动coqide (已安装)，并在左侧窗口中键入以下行并执行它们(使用窗口顶部的向下绿色箭头)。

Require Import VplTactic.Tactic.
Add Field Qcfield: Qcft (decidable Qc_eq_bool_correct, constants [vpl_cte]).

等等，请阅读上面给出的链接的页面。我还没试过呢。