The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-04-24, Guillaume Melquiond wrote:
> Le dimanche 24 avril 2011 à 16:18 -0400, Tom Prince a écrit :
> 
> > Python has this, an uses $HOME/.local/lib/python$VERSION/site-packages
> > I would suggest $HOME/.local/lib/coq for this. I am curious if people 
> > think this is a good idea, and if so, what their opinions on location
> > are.
> 
> Rather than deciding on a specific location, you could just as well
> follow the XDG Base Directory Specification [1] and use
> $XDG_DATA_HOME/coq as the default path (possibly followed by /$VERSION,
> so as to avoid incompatible .vo files when changing version). Basically,
> it means that, on a system without any environment variable set, the
> files would end up in $HOME/.local/share/coq/...

I think this is a good idea (and part of why I suggested .local). At
least plugins are arch dependent, and the FHS would thus suggest lib for
them. But I guess this probably isn't an issue in practice.

On the other hand, .local/lib was added to python after xdg-base-dir
spec was created. I think the argument was along the lines that .local 
is like /usr or /usr/local, just under ~, and so they copied what python
looked for in /usr.

That said, I'd be happy with either option.

  Tom