The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Frederic --

That syntax doesn't seem to work either

coq_makefile -I foo bar a.v

produces:

...

COQLIBS?=-I .\                                                                        

  -I foo

...

If you look in the source code, there are only rules for parsing '-R A B' and '-I A', no other rules.

I wrote a patch yesterday for this, but mostly for the parser, I don't know what semantic things need to be chnaged inside coq_makefile. 

On Mon, May 13, 2013 at 8:16 PM, Frédéric Blanqui <frederic.blanqui AT inria.fr> wrote:

Hi.

You should use the following syntax instead:

coq_makefile -R my_lib_dir Lib


Le 14/05/2013 02:27, Gregory Malecha a écrit :

Hello --

Is there a way to get coq_makefile to notice the -as option that is allowed after -I by
coqc? For example:

coqc -I my_library -as Lib ...

works, but when I pass '-as Lib' to coq_makefile, it seems to completely ignore it:

coq_makefile -I my_library -as Lib ....

will generate a Makefile that runs commands like

coqc -I my_library ....

If it isn't implemented yet, I might be able to write a patch if someone can point me to the right place.

Thank you.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/ <http://www.people.fas.harvard.edu/%7Egmalecha/>

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/