Recent MR to support rocq binary broke "hacks" that allow changing coq-prog-name

[gmalecha]

It appears that a967f22#diff-100fc6940be2711fc43c067e3ede790de91765c7d18b33e5fc459d9b5c2faa89R801-R804

            (if (and proof-prog-name-ask proof-prog-name)
                 ;; let us find other executables in the exact same
                 ;; place. TODO: go back to default exec-path if not found?
                 (let ((exec-path (list (file-name-directory proof-prog-name))))
                   (setq coq-compiler (executable-find (coq-detect-coqc)))
                   (setq coq-dependency-analyzer (executable-find (coq-detect-coqdep))))
               ;; default: detect everything from the current exec-path
               (setq proof-prog-name (coq-autodetect-progname))
               (setq coq-compiler (coq-detect-coqc))
               (setq coq-dependency-analyzer (coq-detect-coqdep)))

may have broken the configuration that is used when Rocq is not installed. Specifically, this code from coqdev.el (https://github.com/rocq-prover/rocq/blob/master/dev/tools/coqdev.el#L86-L93)

(defun coqdev-setup-proofgeneral ()
  "Setup Proofgeneral variables for Rocq development.

Note that this function is executed before _Coqproject is read if it exists."
  (let ((dir (coqdev-default-directory)))
    (when dir
      (setq-local coq-prog-name (concat dir "_build/install/default/bin/coqtop")))))
(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral)

I don't know a lot about e-lisp, but after a few hours of debugging it seems that I can restore the desired functionality by commenting out the (setq proof-prog-name (coq-autodetect-progname)).

[Blaisorblade]

Sadly, link to diffs almost never work — but one can find the quoted code in

PG/coq/coq-system.el

Lines 795 to 804 in a967f22

	(if (and proof-prog-name-ask proof-prog-name)
	;; let us find other executables in the exact same
	;; place. TODO: go back to default exec-path if not found?
	(let ((exec-path (list (file-name-directory proof-prog-name))))
	(setq coq-compiler (executable-find (coq-detect-coqc)))
	(setq coq-dependency-analyzer (executable-find (coq-detect-coqdep))))
	;; default: detect everything from the current exec-path
	(setq proof-prog-name (coq-autodetect-progname))
	(setq coq-compiler (coq-detect-coqc))
	(setq coq-dependency-analyzer (coq-detect-coqdep)))

.

[SkySkimmer]

It's also possible that the coqdev-setup-proofgeneral is wrong and should be setting proof-prog-name instead

[gmalecha]

@SkySkimmer I experimented with this as well, but even updating our hook (similar to the Rocq hook) to update both variables did not seem to work. I could get it to work by setting coq-prog-name-ask but I don't want to type the path every time (it is prompted before this logic).