The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 09/28/2014 08:19 PM, Jason Gross wrote:
> This sounds reasonable; you should make a bug report/feature request.
>
> -Jason

OK - I'll do that.  I just noticed the "enhancement" item on the 
Severity pulldown menu in the bug reporter...

> On Sep 28, 2014 1:06 PM, "Jonathan" 
> <jonikelee AT gmail.com>
>  wrote:
>
> > Suppose one has a Coq script "pwd.v" that just contains the single line:
> >
> >   Pwd.
> >
> > When this script is loaded in Proof General, the result printed for the
> > Pwd command is the path of the directory containing the script, regardless
> > of the location of emacs or where it was started from.
> >
> > When this script is loaded in CoqIDE, the result printed for the Pwd
> > command is the path of the directory where CoqIDE was started from,
> > regardless of the location of the script.
> >
> > This makes it difficult to use relative paths within Coq scripts
> > effectively so that the script has the same behavior whether run in PG or
> > CoqIDE.  For example, a command such as [Add LoadPath "." as Foo.] would
> > work for development using PG, but usually not for CoqIDE, unless one
> > somehow arranges for CoqIDE to always be started in the home directory of
> > the script it is running.
> >
> > I think it would make sense for CoqIDE to have some way to behave like PG
> > for such cases.  Consider that, quite often, an IDE such as PG or CoqIDE is
> > started by clicking an icon on the desktop or toolbar, or from a global
> > application menu.  In such cases, the current directory of the IDE at
> > startup is almost never a good place to use as the current working
> > directory of a file loaded into that IDE after startup.  Certainly it is
> > possible to arrange for some other single current directory to be
> > associated with that icon - but that only solves the problem when loading
> > scripts in that specific directory, not in others.
> >
> > Would it be possible to add a "-scriptwd" option to CoqIDE to get PG's
> > behavior?
> >
> > Or would it make more sense to just change CoqIDE's behavior to mirror
> > that of PG?
> >
> > -- Jonathan