How to import a file in Coq?

Using Coq
1

I’m having trouble finding elementary explanations of how to use Coq.

Let’s say I make a Coq file with some definitions and theorems, and I want to use these in another file. How would I do that (with Emacs/Proof General)?

I think I have to make a _CoqProject file and compile my files and then import them. But I don’t know how to do any of this, or how to organize the files. I’m new to Coq and Emacs. My background is in Mathematics.

2

Let us suppose you have two files foo.v and bar.v. Create a _CoqProject file next to them that contains:

-R . MyProofs
foo.v
bar.v

Then, run coq_makefile -f _CoqProject -o Makefile.

If the bar.v file depends on foo.v, have it start with Require Import foo.

Whenever you modify foo.v and want the changes to be visible from bar.v, just run make. That will cause a foo.vo file to be created, which Require will then be able to load in bar.v.

1 Like
3

Where do I run coq_makefile -f _CoqProject -o Makefile and make? (I’m using Mac OS X.)

4

In the same directory as the _CoqProject file and your .v files.

If the question is how to actually run the commands, then use the shell from your terminal emulator (named just Terminal under macOS, if I remember correctly), use the cd command to move to the corresponding directory, and then type the commands. But I am no user of macOS, so I am only guessing. There are certainly better venues than this forum to learn about shells, makefiles, etc.

1 Like
5

Okay, I did that and it seems to have worked correctly. However, when I tried to compile my file foo.v by selecting Compile... from the Tools menu, it said coqc: command not found and coqdep: command not found. Is this the correct way to compile? If so, how can I fix these errors?

6

I always type make in a terminal when I want to compile. So, I cannot help you with this issue. My guess is that you have to configure ProofGeneral, so that its customization variables coq-compiler and coq-dependency-analyzer point to the correct executable files.

7

On macOS, programs started by clicking an icon (which I ncludes your Emacs, I guess) don’t see changes to the PATH done in your shell configuration (e.g. .bashrc/.bash_profile/.profile). Solutions include using https://github.com/purcell/exec-path-from-shell, but I’m not sure it’s so easy…