Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Broken (possibly outdated?) setup instructions regarding coq-prog-name #596

Closed
Janno opened this issue Sep 3, 2021 · 3 comments · Fixed by #598
Closed

Broken (possibly outdated?) setup instructions regarding coq-prog-name #596

Janno opened this issue Sep 3, 2021 · 3 comments · Fixed by #598

Comments

@Janno
Copy link

Janno commented Sep 3, 2021

The instructions in https://proofgeneral.github.io/doc/master/userman/Obtaining-and-Installing/ instruct users to add -emacs to their coq-prog-name variable:

(setq coq-prog-name "/usr/bin/coqtop -emacs")

It seems this actually breaks PG, leading to failures such as

proof-activate-scripting: Wrong type argument: stringp, nil

or

proof-activate-scripting: Starting process: coqtop -emacs -emacs <..more arguments..>...failed

on newer versions of PG.

@Janno
Copy link
Author

Janno commented Sep 3, 2021

Interestingly, starting coqtop with two -emacs arguments is actually fine. It seems the debug message printed on newer PG versions is missing some quotes around the program name that it actually tries to run. I assume the actual underlying failure is from trying to run "coqtop -emacs" -emacs, not "coqtop" -emacs -emacs as it is printed.

@hendriktews
Copy link
Collaborator

Thanks for the report! Above the only occurrence of -emacs I read "The default names for proof assistant binaries may work on your system. If not, ..." in Appendix A. Therefore, I would not say the manual instructs people to add -emacs... Did the default names of the binaries not work for you?
I agree that there seems to be a problem with the documentation. Setting coq-prog-name as documented should not raise such an error, even in case the default binaries do work.
Have you customized coq-compile-before-require or do you see this problem with the default setting of nil for this setting?
The latest changes in that part of the manual are from 2000. @Matafou: To me this looks like we forgot to update that part of the manual when we changed the code to add emacs as argument.

@Matafou
Copy link
Contributor

Matafou commented Sep 5, 2021

Indeed this part of the manual needs update.
AFAIK the good answer is: coq-prog-name should contain the executable name ONLY, with no option or argument, and options should go into the list coq-prog-args (and of course -emacs is useless because added by PG anyway but this is indeed innocuous).
That said even this, while correct, is a bit outdated since writing a _CoqProject is better almost in any circumstances and you don't need to care about these variables anymore.
I will try to fix this part of the documentation. Thanks for reporting.

Matafou added a commit to Matafou/PG that referenced this issue Sep 13, 2021
Matafou added a commit that referenced this issue Sep 13, 2021
fix #596 - outdated documentation for setup coq-prog-xxx.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants