Coq fails to start

[coquser]

OS: Mac OS X 10.5.4

PG version: 3.7.1

Gnu Emacs version: 22.2.1 (via MacPorts?), 23.0.60.1 (via CVS)

Coq version: 8.1pl3

Test file: A single line consisting of "Definition x : nat := 3."

Problem: Coq fails to start when I try to process the line or buffer. The only error message that I see is "Wrong type argument: integerp, "-emacs-U"." (For the CVS version of emacs, it's characterp instead of integerp.) In the *Messages* buffer, I see "let*: Wrong type argument: integerp, "-emacs-U" [2 times]." I don't think I'm seeing this problem with PG 3.7.

My contact: brian.aydemir [ at ] gmail.com

Cheers, Brian Aydemir

[David Aspinall]

Thanks for the swift report. I can't reproduce this on Linux, nor on Mac using Carbon Emacs 1.6.0 or Emacs.app binary release 2007-11-25 (23.0.60.1).

Could you please upload a full backtrace? See PG/etc/debugging-tips.txt

Probably best to remove the compiled files (make clean) first.

[David Aspinall]

Looking at the code I have found the problem, which is triggered when there is a Makefile in the same directory as the .v file. The code has a type error and also ignores whether the make command succeeds or fails. We will make a swift patch of 3.7.1 to fix this bug. Thanks again for raising it swiftly.

[David Aspinall]

Followup note: the 3.7.1.1 release adds a new custom setting for Coq, coq-use-makefile, which causes the code to guess the Coq command line by running gmake -n -W foo.v foo.vo. If you have a Makefile in the same directory as your Coq files which doesn't give the correct response, you should not enable this flag. It is nil by default. This flag isn't documented in the manual.

[nikecitycn]

​Nike air force ones ​Air Jordan shoes ​Nike Dunks ​Nike Shox ​Nike Shoes

[Frome123]

Who does it seem that coq fails to start when I try to process the line or buffer. The only error message that I see is "Wrong type argument: integerp, "-emacs-U"." (For the CVS version of emacs, it's characterp ​zend php framework instead of integerp.) In the *Messages* buffer, I see "let*: Wrong type argument: integerp, "-emacs-U" [2 times]." I don't think I'm seeing this problem with PG 3.7.6

[deman]

​Effektive fettverbrennung ​Zahnaufhellung Tipps