#233 closed defect (fixed)
Coq fails to start
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-3.7.1 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
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
Change History (6)
comment:1 Changed 16 years ago by
comment:2 Changed 16 years ago by
Milestone: | PG-Emacs-4.0 → PG-Emacs-3.7.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
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.
comment:3 Changed 16 years ago by
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.
comment:4 Changed 15 years ago by
comment:5 Changed 14 years ago by
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
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.