The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

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