CODEWITHSUNDEEP
coq
Siddharth Bhat
Siddharth Bhat

Reputation: 843

View all installed libraries and how they are to be imported in Coq

I've been wanting to use coq-vpl, and I have it installed. I can confirm this from 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.
...

However, how do I find out what the library is actually called and what I need to import? The vpl page does not have docs on it.

Upvotes: 1

Views: 723

Answers (2)

Jason Gross
Jason Gross

Reputation: 6128

You can run

coqc -config

To get a list of configuration variables. On my system, this gives

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

If you look at the user-contrib directory of the path given by COQLIB, you should see folders with the various libraries you've installed. For any of these folder names, you can add From FolderName Require Import FileName to your Coq file.

Upvotes: 5

Yves
Yves

Reputation: 4236

According to https://github.com/VERIMAG-Polyhedra/VplTactic, you need to run coq, for instance by launching coqide (which you installed) and by typing the following lines in the left-hand-side window and executing them (using the downward green arrows on top of the window).

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

And so on, please read the page at the link given above. I did not try it yet.

Upvotes: 1

Related Questions