The Coq mailing list

[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