search

ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
491 stars 89 forks source link

User-defined `coq-prog-args` gets reset to `("-emacs")` on every `proof-shell-start` #661

Open zacque0 opened 2 years ago

zacque0 commented 2 years ago

Hi,

Problem description: As per title.

Steps to reproduce:

  1. Simply set coq-prog-args to some values. E.g. (setq coq-prog-args '("-set" "Printing Parentheses")).
  2. In a Coq file, run M-x proof-shell-start, or C-c C-s bound to proof-toggle-active-scripting.
  3. Then, you can see that coq-prog-args is now set to ("-emacs").

Problem diagnosis:

  1. Function coq-prog-args is run right before every proof-shell-start. https://github.com/ProofGeneral/PG/blob/ec4f9bad18f6c8336e53910d3ea941d5ceb52f52/coq/coq-system.el#L659-L667

  2. In coq-prog-args, the function coq-load-project-file fails to detect coq-load-args from file-local-variables-alist. https://github.com/ProofGeneral/PG/blob/ec4f9bad18f6c8336e53910d3ea941d5ceb52f52/coq/coq-system.el#L626-L627

  3. Indeed, in any newly opened Coq file, the file-local-variables-alist is nil.

So, now, if I M-x eval-expression, then (push (cons 'coq-prog-args coq-prog-args) file-local-variables-alist) and starts the proof-shell. Everything works as expected.

But then now the variable coq-prog-args is modified to custom value specified for the current file and Coq project. And if I stop and start the proof-shell again, the same file-specific arguments will be appended to coq-prog-args again and again.

I haven't found out which function does that. But maybe it should work on the file-local coq-prog-args value and not the user-defined one...

Summary: There are two things gone wrong here:

  1. PG needs a way to detect whether a user has defined a custom coq-prog-args, but it fails.
  2. PG needs a way to compute a file-/project-specific arguments to Coq, but it modifies the custom variable coq-prog-args instead. This is surprising to the user, because custom variable should only be modifiable by the user. Perhaps storing the computed arguments as coq-computed-args into the file-local-variables-alist would solve the problem(?).

Thanks!

Environment: Using Coq v8.15.1 Melpa version: proof-general-20220610.705. Variable value of proof-general-version: "Proof General Version 4.5-git."

Matafou commented 2 years ago

Good point. IMHO the idea is either you have a _CoqProject file either you set coq-prog-args because implicitly coq-prog-args is mainly for setting the load-path. For user options you should probably use coq-user-init-cmd for user preferences like this. If we stick to this policy we should probably document it.

zacque0 commented 2 years ago

Hmmm, but coq-user-init-cmd is defined as a constant, not a custom variable... That's why I'm not aware of it in the M-x customize-group options.

Matafou commented 2 years ago

Indeed it is a bit rough at the edges. We need to make this easier to set up. Especially because dune is also coming in the game and we probably will have more use case like yours.

zacque0 commented 2 years ago

Okay, not sure how is that relevant to my issue.

Anyways, my workaround solution is to place user-wide configuration into ~/.coqrc.

As for this issue, I'll leave it open since it's unsolved. Thanks!

Matafou commented 2 years ago

Agreed, this needs a proper and documented solution.