The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Oh, I see, you want to use it to locate projects.  I thought you were using it for settings.  (Just imagine how hard it would be to track down failures when someone decided that [Set Primitive Projections. Set Universe Polymorphism. Set Asymmetric Patterns. Set Keyed Unification.] was a good resource file to have.)  I think COQPATH is the standard way of doing this, however annoying it may be.  (I think it's actually better than resource files, given that I use my resource files for things like "disable the display of dependent evars in emacs" and other settings.)

On Tue, Aug 2, 2016 at 6:46 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 08/02/2016 03:53 AM, Jason Gross wrote:
> Makefiles should be portable.  A Makefile that only works on your machine
> is not very useful.  Consider instead having an extra file, maybe
> Settings.v, which you build with a separate Makefile, and pass -require
> MyProject.Settings along to your build process.

Jason,

How does the mechanism you propose help matters?  The Settings.v file
then becomes the point of conflict.  If each project must have its own
Settings.v file that tells it where all other projects are on that
machine, then each time that project is transferred to a different
machine, the project's local Settings.v must change.  If, instead, one
uses something like a symbolic link to a global Settings.v file for that
machine, then that effectively re-creates the resource file mechanism.

But, supposing you are correct - why isn't this mechanism documented
instead of resource files and COQPATH?  RTFM-GF'd?

-- Jonathan

>
> On Mon, Aug 1, 2016, 1:17 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
>
>> Why do Makefiles generated via coq_makefile pass -q to coqc?
>>
>> If a user decides they want to use a resource file (one that for example
>> Adds to the LoadPath), how do they configure coq_makefile to use it?
>>
>> -- Jonathan
>>
>>
>>