Downloaded bytecode buggy?

[courtieu]

Hello, I am getting an error with bytecode of the 4.0 package and emacs-23.1.1.

I perform the following:

download pg at http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.0.tgz

untar, set path variable of emacs correctly. Start emacs, open a .v file. Here is the error message:

Loading coq... Coq default abbrevs loaded Loading coq...done File mode specification error: (wrong-number-of-arguments called-interactively-p 1)

Notice that if I make clean; make in pg directory everything goes well.

Regards, PC

[David Aspinall]

Thanks for the report, I have heard this before, I think the .elcs were accidently produced with a beta version of Emacs 23.2 whose bytecode has incompatibilities with 23.1.

The next version will officially (i.e. deliberately!) have 23.2 bytecode.

[David Aspinall]

See also #378