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

[zacque0]

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]

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]

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]

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]

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]

Agreed, this needs a proper and documented solution.