The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
Le jeudi 24 avril 2014 à 13:56 +0200, Beta Ziliani a écrit :
> Hi club,
> 
> The coq_makefile command adds a -q (that is, the "ignore the rcfile"
> flag) to coqc.  That is, when executing "make" it performs
> 
> coqc -q myfile.v
> 
> Is there a way to avoid the -q flag?  I couldn't find it in the doc.
There is nothing but a workaround hack: redefining the variable COQFLAGS
in the makefile by hand !
COQFLAGS is set to
-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
only if it hasn't been defined earlier. So, by defining it to something
that do not include a -q, you avoid the use of -q ...

The justification for using -q seems reasonable to me: when you release
something, it mustn't depend on and be distrub by the rcfile of users.
All the settings you want to ensure have to be describe in the file used
to generate the makefile.

Cannot you do what is done by your rcfile in the Make file ? Are you one
more time in a instance of the problem "I want coqtop to look in the
directory foo but foo is not part of my development" or are you trying
to do something smarter ?
> 
> Thanks!
> Beta
All the best,
Pierre B.