代码之家 › 专栏 › 技术社区 › Siddharth Bhat

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

coq

Siddharth Bhat · 技术社区 · 6 年前

我一直想用 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 页面上没有文档。

2 回复 | 直到 6 年前

Jason Gross 6 年前

你可以跑步

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

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

Yves 6 年前

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

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

等等,请阅读上面链接的页面。我还没有试过。

推荐文章

Mei Zhang · 定义“依赖类型”模函子

6 年前

Jason Hu · 参见Ltac中的Hintbase

6 年前

lllllllllllll · 通过两个实现对阶乘程序进行Coq验证

6 年前

MikkelBybjerg · 如何延迟lambda评估,以便替换lambda

6 年前

user9335697 · 实例化参数以评估函数定义

6 年前

Jian Wang · Coq中的背景目标、搁置目标和放弃目标是什么?

6 年前

Pablo Inostroza · 有没有可能表达一个定理,说明应用了哪些构造函数?

6 年前

jmite · Coq:在校样脚本编写期间查看校样术语

6 年前

ConfusedFormalizer · a是怎样的。vo文件的结构是否便于coqchk使用?

6 年前

Siddharth Bhat · 查看所有已安装的库以及如何在Coq中导入它们

6 年前