The Coq mailing list

[Gyesik Lee <leegys AT gmail.com>]

Thank you for your help.

Gyesik

2013/7/2 Pierre Courtieu <pierre.courtieu AT gmail.com>

Hello,

I just finish implementing (profgeneral cvs) a new feature in
proofgeneral, following recommendations of coq documentation
(http://coq.inria.fr/coq/refman/Reference-Manual017.html#sec574).

You need a file _CoqProject in the root directory of the library
containing the parameters passed to coq_makefile, and proofgeneral
will look at -R an -I options to set up the coqtop arguments
accordingly (coq-load-path).

I don't know if the the GroupTheory has such a project file, but it is
an alternative to .dir-locals.el. Testing welcome (you need the last
cvs version, the dev version is not yet updated).

Hope this helps,
P.

Example of _CoqProject file:

-R mylib MyLib
-I foo
bar.v
bar2.v
...





2013/7/2 Alan Schmitt <alan.schmitt AT polytechnique.org>:

> leegys AT gmail.com writes:
>
>> The user's contribution library GroupTheory can be well compiled just by
>> using the command 'make'.
>> However, when I like to use g1.v,  I cannot pass the following line:
>>
>> Require Import Laws.
>>
>> Emacs + ProofGeneral complains as below:
>>
>> Error: The file ..../GroupTheory/Laws.vo contains library
>> GroupTheory.Laws and not library Laws
>
> Since you're using ProofGeneral, you could create a file
> `.dir-locals.el' with the appropriate include path. For instance, if the
> path where GroupTheory is install is "../foo/GroupTheory", you could say:
>
> --8<---------------cut here---------------start------------->8---
> ((coq-mode . ((coq-load-path . (("../foo/GroupTheory" "GroupTheory"))))))
> --8<---------------cut here---------------end--------------->8---
>
> You can do a `C-h v coq-load-path' to know more about what this variable
> means.
>
> Hope this helps,
>
> Alan