Stream: Proof General users

Topic: "File mode specification" error


view this post on Zulip Pierre-Yves Strub (Nov 10 2021 at 10:20):

Hi. With Coq 8.14 & PG 20211109.1442 (installed by elpa), I have this error when opening a Coq file:

File mode specification error: (coq-unclassifiable-version . 8.14.0 compiled)

view this post on Zulip Pierre-Yves Strub (Nov 10 2021 at 10:20):

Do you understand what is happening here?

view this post on Zulip Karl Palmskog (Nov 10 2021 at 10:21):

probably related to this previous closed issue: https://github.com/ProofGeneral/PG/issues/600

view this post on Zulip Karl Palmskog (Nov 10 2021 at 10:21):

ping @Erik Martin-Dorel

view this post on Zulip Pierre-Yves Strub (Nov 10 2021 at 10:24):

Hmm. In fact, I was loading a old version of PG... This now works since the ELPA version is loaded. Sorry for the noise.

view this post on Zulip Karl Palmskog (Nov 10 2021 at 10:26):

at least we find out that testing on Coq 8.14+rc1 paid off...


Last updated: Feb 06 2023 at 06:29 UTC