Take the 2-minute tour ×

I can't load modules that are in same folder in CoqIde.

I'm trying to load sources from Software Foundations, I'm running coqide in folder that contains SF sources with coqide or coqide ./, then after opening and running the file, I'm getting this error:

Error: Cannot find library Poly in loadpath

in this line:

Require Export Poly.

and it's same for every other require commands.

So how are you people loading programs from SF into coqide ?

share|improve this question
add comment

1 Answer

up vote 3 down vote accepted

You need to compile the .v files into .vo files and add their directory to your load path if you're going to require them. To compile them, run coqc <file-path> in the command prompt. To add the files' directory to your load path in CoqIde, you can insert the line Add LoadPath "<directory-path>". at the beginning of the .v files.

share|improve this answer
add comment

Your Answer


