Unable to run coqtop/rocq when using opam switches

[RangHo]

I'm on Arch Linux, running Emacs 30.2 as a systemd user service and connecting via emacsclient.

Since I have to juggle multiple versions of Coq/Rocq, I use opam switches extensively. For Emacs integration, I use the opam-switch-mode also hosted in the Proof General organization.

When I try to run Coq proofs from a buffer using C-c C-RET, Proof General fails to start coqtop with the following message: make-process@with-editor-process-filter: Searching for program: No such file or directory, coqtop.

Inspecting the value of exec-path and coq-prog-name, the buffer-local exec-path does have the correct binary path (i.e., /path/to/project/_opam/bin) and coq-autodetect-progname function seems to be able to detect the existence of coqtop binary in exec-path.

However, when actually trying to start the process in scomint.el, suddenly Emacs can't find the file. The code below is the last code in Proof General that I can trace back to.

PG/lib/scomint.el

Lines 186 to 189 in 75c13f9

	(setq proc (apply (if (fboundp 'start-file-process)
	;; da: start-file-process is Emacs23 only
	'start-file-process 'start-process)
	name buffer command switches)))

For now, I can workaround the issue by evaluating the coq-prog-name with the following script:

#!/bin/sh

# Script to start Proof General with the right Coq version.

make -q ${1}o || {
  make -n ${1}o | grep -v "\\b${1}\\b" | \
  (while read cmd; do
    sh -c "$cmd" || exit 2
   done)
}

COQPROGNAME="${COQBIN}coqtop"

emacs --eval "(setq coq-prog-name \"$COQPROGNAME\")" $1 && make ${1}o

...but I'd rather have more elegant solution that I can run from my central Emacs daemon.

Thanks in advance!

---

Edit: I tried adding the following content to .dir-locals.el to see if it can force using the correct version of coqtop but to no avail:

((coq-mode . ((coq-prog-name . "/path/to/_opam/bin/coqtop")))

In this case, the initial value of coq-prog-name is set as intended, but as soon as I try to spawn a proof shell using C-c C-RET it gets reverted to rocq and complains that Rocq is not installed. (I don't have rocq installed in my default switch, by the way.)

[Matafou]

This seems related to #869 .