CODEWITHSUNDEEP
coqcoqide
LyX2394
LyX2394

Reputation: 131

How to Manually Set up a Library in GitHub for Use in CoqIDE?

I need to use a library in GitHub different from Coq's standard library. But I do not know how to manually set it up so that I can use it in CoqIDE.

I need to use this library in CoqIDE. I have downloaded and saved the folder to my computer, but when I open CoqIDE and write "Require Import StringEq", where StringEq is the name of a Coq file from the library, I get the error message "Unable to locate library StringEq".

Is there any way I can manually set up this libray so that I can use it with CoqIDE? (There are no instructions on the READme file on the library's GitHub page.)

Upvotes: 2

Views: 171

Answers (1)

Li-yao Xia
Li-yao Xia

Reputation: 33509

The official usage seems to be add kami to the $COQPATH environment variable.

On Linux, add this line to .bashrc or .zshrc or whatever initialization your shell uses and restart your shell:

export COQPATH=/path/to/kami:$COQPATH
# That path must be so that `/path/to/kami/Kami/Lib/StringEq.v` is the path to `StringEq` for example

Below is another way I am using.
It doesn't seem like intended usage. Maybe I'm just resistant to changing my ways, but I also prefer being explicit about my dependencies, and I'm not sure the COQPATH environment variable makes it as easy to have different versions of the same library in different projects.

Add a _CoqProject that tells CoqIDE where to find kami.

Here's an example layout:

kami/           # The Kami repository
myproject/      # Your workspace
  _CoqProject
  theories/
    MyProject.v

Where myproject/_CoqProject contains:

-Q ../kami/Kami Kami
# and possibly other options

Either way, remember to build Kami:

cd kami/
make

Upvotes: 3

Related Questions