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 ?

score 27 · Accepted Answer · answered Apr 24 '13 at 23:01

27

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.

answered Apr 24 '13 at 23:01

3

Is there a Coq load path environment variable? – Greg Nisbet Jun 30 '15 at 05:42
1

@GregoryNisbet Yes, COQPATH: https://coq.inria.fr/refman/Reference-Manual016.html#sec587 – Langston Jan 27 '17 at 20:18
1

it says `LoadPath` is not valid syntax `Syntax error: illegal begin of vernac.` – Charlie Parker Nov 29 '18 at 02:52
you need `Add` see answer bellow. – Charlie Parker Nov 29 '18 at 03:09
On later versions of Coq you have to add also a suffix "as ...", like: `Add LoadPath "/Users/myuser/cpdt/src" as Cpdt.` – The_Ghost Jan 17 '22 at 18:00

score 7 · Answer 2 · answered Mar 22 '16 at 22:02

7

I realize this is an old thread, however there are not many resources on this problem. I just spent some time solving it so I figured it would be good to post it on the first topic I got from googling. I'm using Coq 8.4p16 compiled with no additional configuration on Arch Linux.

So, the manual says variables like $COQPATH, ${XDG_DATA_DIRS}/coq/ and ${XDG_DATA_HOME}/coq/ are checked, however I've had no luck with those.

I also tried putting coqc -I /folder/path the Edit->Preferences->Externals of CoqIde, however, still no luck there.

I write these as they may work for someone.

The only GLOBAL way which works for me is writing a coqrc file with Add LoadPath "<directory-path>". in it. On Linux the file needs to be in the home folder.

Hope this saves someone some time.

answered Mar 22 '16 at 22:02

najtofni

71
1
1

2

This works if you are using coqIDE (command line always works). I wish coqIDE would automatically add current PWD to the load path but it's not. – Negative Zero Sep 19 '16 at 16:28
It seems there might be a way to get this to work using _CoqProject, but I'm not sure how: http://coq-club.inria.narkive.com/q5jGTrgk/configuring-coqide-using-coqproject – Blaisorblade Oct 19 '16 at 14:59
1

The same for me: the only way `coqc cli tool`works is using coqrc file, but I'm under x64 win7 for coq 8.6 December 2016. – valaxy Feb 08 '17 at 06:47

score 4 · Answer 3 · answered Jun 29 '17 at 14:21

To be able to load a source file in coqtop, coqc, CoqIDE, or Proof General there are several ways, one method is as follows:

Suppose you have downloaded code files for the book titled Certified Programming with Dependent Types written by Adam Chlipala that are available here and extract them in a path we call CODEHOME. As you can see there are this first line in any source files Require Import Bool Arith List Cpdt.CpdtTactics.

First type coqc -v in a cli (command line interface), the output would be something like The Coq Proof Assistant, version 8.4pl4 ...., then create a file named coqrc.8.4pl4, the file extension should be in accord with the version of the coq you are using, in $HOME/.config/coq directory if it does not exist and write this line in it Add LoadPath "CODEHOME/cpdt/src" as Cpdt . and that's it.

DerMann · Answer 4 · 2017-06-07T23:17:53.403

-1

If you started your file.v with Module file. just get rid of it (Also get rid of the End file.) and your problem is solved.

edited Jun 07 '17 at 23:17

answered May 17 '17 at 13:32

DerMann

223
1
2
13

coqide - can't load modules from same folder

4 Answers4

Linked