The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

_CoqProject primary goal is to generate a makefile with coq_makefile
-f _CoqProject. It is also read by IDEs to adapt options on the fly to
be consistent with the makefile. It is therefore preferable to put all
the options in this file, so that the makefile and IDEs use the same
options.

P.

2016-04-21 10:54 GMT+02:00 Théo Zimmermann 
<theo.zimmermann AT ens.fr>:
> My understanding is that you can ask which options you can pass to
> "coq_makefile --help" because option "-f" is defined as just a way of taking
> arguments for this command in a file (such as _CoqProject). So, for
> instance, while coq_makefile is generally called like that:
> coq_makefile -f _CoqProject -o Makefile
> You can also rather choose to put the "-o Makefile" option inside the
> _CoqProject file and then just call:
> coq_makefile -f _CoqProject
>
> Le mer. 20 avr. 2016 à 23:08, Tej Chajed 
> <tchajed AT mit.edu>
>  a écrit :
>>
>> It looks like _CoqProject is parsed in some hacky way. Skimming the code
>> (ide/project_file.ml4) it looks like you can pass -I, -Q and -R normally,
>> but for custom args you need -arg. Thus your file should look something
>> like:
>>
>> -R . Top
>> -arg -l -arg Utf8
>>
>> which does indeed work for me (running CoqIDE from 8.5beta2).
>>
>> Note that in my version of CoqIDE other other stuff in the file does not
>> trigger a warning or error from the parsing code; "-l Utf8" is just 
>> ignored.
>>
>> On Wed, Apr 20, 2016 at 4:43 PM, scott constable 
>> <sdconsta AT syr.edu>
>>  wrote:
>>>
>>> Follow-up question: What kinds of arguments am I allowed to put into a
>>> _CoqProject file? Are they coqide arguments, coqtop arguments, or 
>>> something
>>> else? I tried adding in "-l Utf8" to automatically load the unicode 
>>> library,
>>> but this doesn't seem to work. However it does work if I invoke it 
>>> manually
>>> from the command line, e.g.
>>>
>>> $ coqide -l Utf8
>>>
>>> or
>>>
>>> $ coqtop -l Utf8
>>> Coq < Print Libraries.
>>> ...
>>> Coq.Unicode.Utf8_core
>>> ...
>>>
>>> Thanks,
>>>
>>> ~Scott Constable
>>>
>>> On Wed, Apr 20, 2016 at 12:01 PM, scott constable 
>>> <sdconsta AT syr.edu>
>>> wrote:
>>>>
>>>> Thanks to both of you for the help! Indeed my CoqIDE preferences were
>>>> set to ignore arguments from the _CoqProject file, which must have been 
>>>> the
>>>> default since I never set this myself. I changed this to "appended to
>>>> arguments". And yes, I also needed to set the first line of my 
>>>> _CoqProject
>>>> file to "-R . <LibName>".
>>>>
>>>> ~Scott Constable
>>>>
>>>> On Wed, Apr 20, 2016 at 11:45 AM, Théo Zimmermann
>>>> <theo.zimmermann AT ens.fr>
>>>>  wrote:
>>>>>
>>>>> Additionally, with Coq 8.5, I have observed that you have to provide a
>>>>> first line with options, such as "-R . MyLibrary". Otherwise a default 
>>>>> "-R .
>>>>> Top" is implicitly added when doing make but not when loading CoqIDE. 
>>>>> (This
>>>>> behavior might be a bug actually.)
>>>>>
>>>>>
>>>>> Le mer. 20 avr. 2016 à 17:13, Tej Chajed 
>>>>> <tchajed AT mit.edu>
>>>>>  a écrit :
>>>>>>
>>>>>> When you open a file with a file called _CoqProject in the same
>>>>>> directory, CoqIDE should load it. If it works, you'll see "Reading 
>>>>>> options
>>>>>> from <path to _CoqProject>" in the status bar at the very bottom 
>>>>>> briefly
>>>>>> (eventually it will just say "Ready").
>>>>>>
>>>>>> You might also check the IDE's settings for project files: there's a
>>>>>> Project section of the settings that controls both the filename and 
>>>>>> what
>>>>>> CoqIDE does with it (replace args, append to args, or nothing). It's
>>>>>> possible that configuration is wrong for you.
>>>>>>
>>>>>> Hope that helps!
>>>>>> Tej
>>>>>>
>>>>>> On Wed, Apr 20, 2016 at 11:04 AM, scott constable 
>>>>>> <sdconsta AT syr.edu>
>>>>>> wrote:
>>>>>>>
>>>>>>> Hi All,
>>>>>>>
>>>>>>> I have a simple coq project with a _CoqProject file in the source
>>>>>>> directory. According to the reference manual (Section 15.3), CoqIDE 
>>>>>>> should
>>>>>>> be able to use the _CoqProject file to automatically configure itself 
>>>>>>> at
>>>>>>> launch. However, I can't figure how to do this, and coqide --help 
>>>>>>> isn't
>>>>>>> offering much assistance. Any help would be much appreciated.
>>>>>>>
>>>>>>> ~Scott Constable
>>>>>>
>>>>>>
>>>>
>>>
>>
>