coqide - can't load modules from same folder

Question

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 ?

Answer 1

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.