proof-prog-name-ask interacts poorly with tab-completion (especially on Windows)

[JasonGross]

When I set proof-prog-name-ask to "non-nil", I get asked about the prover name. If I change it, and tab-complete to d:/Documents/GitHub/coq-8.5-ltacprof/bin/coqtop.exe (note the trailing space that Emacs automatically inserts), then I get:

Starting: d:/Documents/GitHub/coq-8.5-ltacprof/bin/coqtop.exe  -emacs
apply: Spawning child process: invalid argument

It seems that PG thinks that the trailing whitespace is part of the filename. I propose that trailing whitespace should be stripped from the executable name when it ends in .sh, .exe, .byte, or .opt (or, more generally, when the executable does not exist, but stripping trailing whitespace results in an existing executable).

By a happy accident, this only occurs frequently on Windows, where coqtop.exe is unique, and not on linux, where coqtop exists but is not unique, because coqtop.byte and coqtop.opt also exist.

[cpitclaudel]

It seems that PG thinks that the trailing whitespace is part of the filename. I propose that trailing whitespace should be stripped from the executable name when it ends in .sh, .exe, .byte, or .opt (or, more generally, when the executable does not exist, but stripping trailing whitespace results in an existing executable).

Wouldn't stripping final spaces work? Currently we use read-shell-command; we could either complete to a file name instead of trying to read a command, or we could strip final spaces, right?

I think the original intent was that you could pass arguments to the prover using proof-prog-name-ask. Since this has been broken for a while, I think we can just assume that this option should do as its name indicate, i.e. ask for the name of the prover.

[Matafou]

Indeed arguments should be passed via proof-prog-args now. If we allow only
file names then things like aliases will not work, and also "coqtop" alone
will not work anymore. I guess stripping trailing spaces is ok.

P.

2016-07-05 17:58 GMT+02:00 Clément Pit--Claudel notifications@github.com:

It seems that PG thinks that the trailing whitespace is part of the
filename. I propose that trailing whitespace should be stripped from the
executable name when it ends in .sh, .exe, .byte, or .opt (or, more
generally, when the executable does not exist, but stripping trailing
whitespace results in an existing executable).

Wouldn't stripping final spaces work? Currently we use read-shell-command;
we could either complete to a file name instead of trying to read a
command, or we could strip final spaces, right?

I think the original intent was that you could pass arguments to the
prover using proof-prog-name-ask. Since this has been broken for a while,
I think we can just assume that this option should do as its name indicate,
i.e. ask for the name of the prover.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
#86 (comment), or mute
the thread
https://github.com/notifications/unsubscribe/AEsl6ryvMfFSlofQ_8nedEkAXnl5SYpBks5qSn85gaJpZM4JD7I3
.

[JasonGross]

Stripping trailing spaces should be fine, unless want to support the use case of having trailing spaces in the executable name.

[cpitclaudel]

unless want to support the use case of having trailing spaces in the executable name.

I don't :)