The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/02/2016 12:26 PM, Jason Gross wrote:
> 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.)

Yes - I was only intending to use it to locate projects, by having Add 
LoadPath lines in the resource file, per section 14.3.1 of the refman.  
I have instead used COQPATH, but am not happy with that:

Using COQPATH to tie together separate projects means that the logical 
names have to match the physical names.  So, this can't be the final 
answer, can it?  Isn't segregating logical from physical names supposed 
to be the new best-practice?  And, isn't it more important to segregate 
logical names from physical names between distinct projects than it is 
to do so within a single project?

Also, using environment variables for settings that are to be shared by 
many tools is often problematic, due to the way different tools pick up 
environment variable settings from different places.  For example, in 
order to get PG to respect the same COQPATH env var I use for shells, I 
had to install exec-path-from-shell, and put 
(exec-path-from-shell-copy-env "COQPATH") in my coq-mode-hook.  Just 
because I launch Emacs from a toolbar instead of from a shell.  I could 
have instead put a bash shell script wrapper around Emacs and launch 
that script instead from the toolbar - but the point is that something 
has to be done specially to pick up env vars in many cases.

But, why put in refman section 14.3.1, and have coq_makefile hardwire 
the -q option?  And at the same time have the Coq tools always ignore 
-init-file if -q is anywhere on the same command line?

If you want to enforce that resource files for Coq only have useful and 
benign settings in them - like Add LoadPath, but not Set Asymmetric 
Patterns - then enforce that when loading the resource file.  And put it 
in the refman, without contradicting it in the tools!

Sorry, should have warned you to put on your flame-proof goggles before 
saying that....

-- Jonathan

> 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