(Some) vok compilation seems to ignore coq-compiler

[LukeXuan]

I use directory local variables to configure different opam switches for different projects I'm working on. It seems like regardless the content of coq-compiler, the delayed compilation of vok files always calls coqc from exec-path/environment.

An updated observation: most of the dependencies are compiled using the correct binary except for a few files...

[hendriktews]

Thanks for the report!
The second stage compilation (i.e., vok compilation) is started via a timer. While I restore default-directory I don't change (current-buffer) when the timer hits. So the second stage processes run with whatever buffer your are visiting as current buffer when the timer hits. And then pick local variables from that buffer.
Could you verify the above theory by explicitly changing the buffer directly after you started some compilation and staying there until the second stage starts? And also by explicitly staying in the current buffer after you started some compilation? By default the timer to start the second stage triggers 2.5 seconds after the last item from the queue region that caused the compilation has been processed.

[hendriktews]

Before writing the above comment, I deduced a few things from your report. Can you please check the following deductions and tell me if they are right? You have different projects for which you set coq-compiler differently via the local variable mechanism. Apparently, after starting compilation you now and then switch buffers and then sometimes the second stage is triggered when you are visiting a buffer from a different project.

[hendriktews]

If my theory is right, the required change is a bit more invasive and will take some time. Until then I have the following suggestions:

• Disable vok compilation (menu coq->auto compilation->vos compilation-> vos no vok)
• Stay within the project until second stage starts, maybe reduce coq-compile-second-stage-delay
• Switch the opam switch explicitly when switching projects via opam-switch-mode

[LukeXuan]

Ah indeed. I didn't switch to a different buffer from a different project, but rather I switched to *coq-compile-resposnse* buffer because I saw an error message. coqc-compiler for that buffer is indeed unset and contains the default value coqc.

Maybe an easy fix (I don't know if it makes sense): is it possible to make *coq-compile-response* buffer (and other PG buffer without corresponding physical files) inherit the coqc-compiler (and other configurations as well) value from the buffer where proof-shell-start is invoked?

Stay within the project until second stage starts, maybe reduce coq-compile-second-stage-delay

I suspect one needs to stay within the buffer until second stage finishes, not just started. I can see from top TUI that the compiler changes from .opam/branch/coqc to coqc in the middle of vok jobs.

Switch the opam switch explicitly when switching projects via opam-switch-mode

I didn't know about opam-switch-mode. I definitely will give it a try!

[monnier]

Maybe an easy fix (I don't know if it makes sense): is it possible to make `*coq-compile-response*` buffer (and other PG buffer without corresponding physical files) inherit the `coqc-compiler` (and other configurations as well) value from the buffer where `proof-shell-start` is invoked?

Another approach used in some packages is to use a buffer local variable set in `*coq-compile-response*` which contains the "origin" buffer (e.g. `vc-parent-buffer`), so that we can go back to that buffer to know which context should be applied.

[hendriktews]

@LukeXuan Right, you would have to stay in some buffer in the right project until vok compilation finishes.

opam-switch-mode globally sets the opam switch for the emacs session by changing exec-path. It is meant for manually switching the opam switch, but it should work project-wise if you set an eval-field in your .dir-locals.el.

@monnier Yes, I need to record the original script buffer and set this in the sentinel and the timer function. I do this already for default-directory.