The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

This sounds reasonable; you should make a bug report/feature request.

-Jason

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