Custom Query (361 matches)

The devlopment version (BZR trunk) of Emacs can hang when PG Coq is used together with Emacs' auto fill minor mode. You can, for instance, reproduce the error in the following way:

1. Start Emacs without any initialization; emacs -q -nsl
2. Load PG initialization: M-x load-file <path-to-PG>/generic/proof-site.el
3. Open a *.v file.
4. Activate auto fill mode: M-x auto-fill-mode
5. Place the cursor _afer_ a comment with more than `fill-column' many characters.
6. Press <enter> -> Emacs hangs, and must be killed.

Remark 1: You do not get an error if auto filling happens _inside_ a comment.

Remark 2: Emacs 24.2.1 does not have this problem at all.

I'm using the Proof General 4.2 with emacs 23.3.1 in ubunbu 12.04 to program with coq.While I was using it to step the coq script,I found that the window was splitted horizontally as which was shown in the attachment.I try to use the "M-x proof-three-window-toogle" and "M-x proof-layout-window" to change the layout so that the window will be splitted vertically. Unfortunately it's of no use.

In Proof General 4.1 with emacs 23.3.1 in ubuntu 12.04,I can split the window vertically by the above commands,while the contents in the "coq goals" was not cleaned. I'm not quite familiar with emacs.So I want to know how to solve these problems.

When I try to process the attached Coq file using ProofGeneral, it gets hung up on the Definition of IB6_IB7_QueryTags_First. In contrast, coqtop file works on this file. The file was generated by Why3's Coq driver, so maybe it's doing something that's syntactically unusual.

I'm running PG 4.1 on GNU Emacs 24.2.1. The Coq version is 8.3pl4.