Opened 14 years ago

Closed 13 years ago

Last modified 13 years ago

#339 closed defect (fixed)

Infinite loop on module print with coq-8.3

Reported by: Paolo Herms Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:
Cc: paolo.herms@…

Description

When I try to process the following with coq 8.3 beta, emacs freezes with 100% cpu. This doesn't happen with coq 8.2.

Require Import MSets.
Module NatSet := MSetList.Make Nat_as_DT.
Print NatSet.

Change History (5)

comment:1 Changed 14 years ago by David Aspinall

Resolution: needmoreinfo
Status: newclosed

Strange! Thanks for the report and small example. Unfortunately haven't got access to this version at the moment. Are you able to interrupt and inspect the contents of the *coq* buffer? If you do

M-x set-variable RET debug-on-quit RET t RET

you should be able to get a backtrace from Emacs as well.

comment:2 Changed 14 years ago by Paolo Herms

Cc: paolo.herms@… added

I'm not able to interrupt (you mean with proof-interrupt-process, right?) neither did I understand where debug-on-quit would put this backtrace. Notice that I really have to kill the emacs window, it just stops reacting!

Now, I found out that sometimes it doesn't happen and it kind of depends on the size of the window... But you should try it yourself. Compiling coq is as easy as doing:

svn co svn://scm.gforge.inria.fr/svn/coq/branches/v8.3 coq-8.3-svn
cd coq-8.3-svn
./configure -prefix "$HOME/usr" -mandir "$HOME/usr/share/man" -opt -with-doc no
make world install

This takes some time (20min) and then installs coq in your home directory. (you need ocaml with camlp5-transitional)

comment:3 Changed 13 years ago by David Aspinall

Resolution: needmoreinfo
Status: closedreopened

Could someone check whether this is fixed by same fix as #140?

comment:4 Changed 13 years ago by David Aspinall

Resolution: fixed
Status: reopenedclosed

Pierre says this is the same as #140.

comment:5 Changed 13 years ago by Paolo Herms

In fact, it seems to be fixed in the snapshot. I was using the cvs access, kind of weird it's less up to date than the snapshot...

Note: See TracTickets for help on using tickets.