The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Hello.

For my own development, I do not possess all my .v files in the same directory, (as most people)

I have several subfolders, each containing Coq Modules (and other stuff).

I use the standard coq_makefile, and get my .vo's on these subfolders.

Since I'm editing these files, for ease of use, I have 

Add LoadPath "/explicit/path/my/development/Xyz" as Xyz.Module.

in all of them. This allows me to simply fire up Coq on any of them, and start editing...

This works for me. However, when distributing my development, I naturally do not want to put an explicit path on top of each module. 

That said, relative paths does not seem to work for me..  Does LoadPath doesn't support relative paths or am I doing something wrong? I always get a "Warning: Cannot open Xyz/"

Moreover, in all other Coq developments I checked, nobody is using LoadPath (at least not in the files they distribute..). Not really popular apparently.. Don't you consider it useful?

For coqc, we can always use the -I switch to include dirs, and perhaps there is a equivalent one for coqide (I checked, doesn't seem to exists..), but in any case I would rather simply have a LoadPath approach that would work not just on my laptop :-)

Perhaps there is an easy solution for this rather silly thing.

Any help?

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.