The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

Thanks Pierre for the quick answer!

On Thu, Apr 24, 2014 at 2:33 PM, Pierre Boutillier
<pierre.boutillier AT pps.univ-paris-diderot.fr>
 wrote:
> 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.

Sure, I understand why it's there.  What I'm trying to do is one of
those things with sign "DON'T TRY THIS AT HOME" ;-)  I just thought
that maybe there was a way of avoiding it, but I'm not surprised there
isn't.

>
> 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 ?

I'm just setting up some options.  I'll do it in a file and include
that in the Make file instead in the rcfile.

>>
>> Thanks!
>> Beta
> All the best,
> Pierre B.
>
>