File mode specification error: (void-variable coq-cmd-force-next-proof-kept)

[DaKnig]

Steps to reproduce:

• package-install RET proof-general
• package-install RET company-coq
• open a coq file ending with .v
• get the error in the title

this error is reported again when re-enabling coq-mode

[DaKnig]

I did restart emacs a few times hoping the thing will solve itself , didnt help

[erikmd]

Hi @DaKnig, thanks for your report!

Could you give more details on your configuration? (OS and (if applicable) Linux distribution, emacs --version)

@hendriktews could you take a look? the reported error mentions the custom you had introduced in: https://github.com/ProofGeneral/PG/commit/0a793dbbe55c58348e581f828e77e651e195ed5d

[erikmd]

@DaKnig can you also run the following code and paste its output?

$ ls -dl ~/.emacs.d/elpa/proof-general-*

[hendriktews]

Can you retry without company-coq? I only see two occurrences of coq-cmd-force-next-proof-kept, one in coq.el and the declaration in coq-syntax.el. And coq.el loads coq-syntax.el. Therefore my suspicion is that the problem comes from copany-coq.

[hendriktews]

If you need a workaround, put

(setq coq-cmd-force-next-proof-kept "Let")

in your .emacs

[Matafou]

What is the status of this issue pls?

[DaKnig]

here are some warnings I get while native-compiling lisp: https://paste.centos.org/view/d527b5df

edit: nope, after restarting emacs, it still doesnt work. symbol's function definition is void : proof-segment-up-to edit2: File mode specification error: (void-variable coq-cmd-force-next-proof-kept) feels like I am in a loop of weird random glitches now

[Matafou]

Does it disappear if company-coq is unstalled.

[DaKnig]

no

[Matafou]

Sorry my question was badly spelled so your answer is now ambiguous :-). Are you saying that when you remove company-coq the bug was still there?

[DaKnig]

the bug is still there without company-coq yes.

if you want to do faster back-and-forth I am available on libera and matrix so just tell what room to join.

[hendriktews]

I cannot reproduce this. I did:

• created a fresh user account for testing, logged in there
• started emacs (28.2)
• M-x package-install proof-general
• opened ~/a.v

[hendriktews]

Additionally, I tried:

• adding melpa as described on the company-coq page
• installing proof-general and company-coq from melpa Again, the error does not appear.

[hendriktews]

@DaKnig : There are still questions that you have not answered yet. Could you answer them? I suspect now that the problem is raised by your personal configuration (.emacs, .emacs.d/init.el, other installed packages, ...) Therefore, can you try to reproduce in a freshly created user account? Or on a different machine, where you have not yet copied your personal emacs configuration to?

[hendriktews]

@DaKnig : I am closing this issue now on the assumption that it was a problem in your personal emacs configuration. Feel free to reopen to continue the investigation if this is incorrect.