PG takes a long time printing module types in Coq

[Evgeny Makarov]

Dear Proof General developers,

I found a curious behavior: it seems that the time it takes PG to print the module type in Coq grows exponentially (or faster?) depending on the number of parameters in this module type.

For example, I started with

Module Type T.

Parameter p1 : nat.

End T.

and started adding lines "Parameter p2 : nat.", "Parameter p3 : nat.", etc. Each time I issued the command

Time Print Module Type T.

after the closing of the module type T. Up to 4 parameters were printed practically instantaneously. When T had 5 parameters, the printing command took about 5 seconds, and when it had 6 parameters, it took about 60 seconds.

In all cases the time requires by Coq as printed by the "Time" command was negligible (~ 0.001 s.). Also, I tried entering all these commands directly in coqtop, and again, printing was instantaneous.

[David Aspinall]

I can't reproduce this. I tried this file called T.v:

Module Type T.

Parameter p1 : nat.
Parameter p2 : nat.
Parameter p3 : nat.
Parameter p4 : nat.
Parameter p5 : nat.
Parameter p6 : nat.
Parameter p7 : nat.
Parameter p8 : nat.
Parameter p9 : nat.

End T. 

Time Print Module Type T. 

If you are using the latest CVS of PG, please could you advise the Emacs/XEmacs version you are using? If my test file is incorrect could you upload a correct one and re-open, please? Thanks.

PS I do notice a processing difference behaviour between XEmacs and GNU Emacs in this example: GNU Emacs processes this file step-by-step, whereas XEmacs processes the module type in a single step, possibly due to regexp behaviour differences. We should harmonise this.

[courtieu]

Could you also give the coq version please?

[Evgeny Makarov]

I am sorry I did not respond to your requests for more information. I still have this issue even though I am using a different computer and a different Linux version (Ubuntu 10.04 instead of Fedora). I used the file you provided above: 5 parameters still take about 5 seconds while 6 parameters take a minute and a half with 100% CPU load. Moreover, during the waiting time Emacs is unresponsive and I can't close it by clicking on the red cross window frame button; I have to use the "kill" command.

I am using the minimal .emacs file with one line:

(load-file "~/software/ProofGeneral/generic/proof-site.el")

I have the latest CVS version (I had to copy contrib subdirectory from ProofGeneral-4.0pre100909.tgz because "make compile" complained about the absence of mmm-auto). I include the info about my Emacs in the end.

Printing module types is important for me because I am studying the new Coq library Numbers, which relies heavily on modules. Often it is not clear, for example, whether a given module type has parameters.

Thanks

In GNU Emacs 23.1.50.1 (i486-pc-linux-gnu, GTK+ Version 2.18.0)
 of 2009-09-27 on palmer, modified by Debian
 (emacs-snapshot package, version 1:20090909-1)
Windowing system distributor `The X.Org Foundation', version 11.0.10706000
configured using `configure  '--build' 'i486-linux-gnu' '--host' 'i486-linux-gnu'
'--prefix=/usr' '--sharedstatedir=/var/lib'
'--libexecdir=/usr/lib' '--localstatedir=/var' 
'--infodir=/usr/share/info' '--mandir=/usr/share/man' '--with-pop=yes'
'--enable-locallisppath=/etc/emacs-snapshot:/etc/emacs:/usr/local/share/emacs/23.1.50/site-lisp:
/usr/local/share/emacs/site-lisp:
/usr/share/emacs/23.1.50/site-lisp:/usr/share/emacs/site-lisp'
'--with-x=yes' '--with-x-toolkit=gtk' 'build_alias=i486-linux-gnu' 'host_alias=i486-linux-gnu'
'CFLAGS=-DDEBIAN -DSITELOAD_PURESIZE_EXTRA=5000 -g -O2'
'LDFLAGS=-g -Wl,--as-needed' 'CPPFLAGS=''

Important settings:
  value of $LC_ALL: nil
  value of $LC_COLLATE: nil
  value of $LC_CTYPE: nil
  value of $LC_MESSAGES: nil
  value of $LC_MONETARY: nil
  value of $LC_NUMERIC: nil
  value of $LC_TIME: nil
  value of $LANG: fr_FR.utf8
  value of $XMODIFIERS: nil
  locale-coding-system: utf-8-unix
  default enable-multibyte-characters: t

Major mode: Coq

Minor modes in effect:
  holes-mode: t
  tooltip-mode: t
  mouse-wheel-mode: t
  menu-bar-mode: t
  file-name-shadow-mode: t
  global-font-lock-mode: t
  font-lock-mode: t
  blink-cursor-mode: t
  global-auto-composition-mode: t
  auto-composition-mode: t
  auto-encryption-mode: t
  auto-compression-mode: t
  line-number-mode: t
  transient-mark-mode: t

Load-path shadows:
/usr/share/emacs/23.1.50/site-lisp/debian-startup hides /usr/share/emacs/site-lisp/debian-startup

[Evgeny Makarov]

Yes, and my Coq version is trunk 13419.

[David Aspinall]

Thanks for the (very belated!) follow up. I can now reproduce this (with an older Coq and different Emacs).

The problem is surely with some horrendous looking regular expressions being used to decorate the output.

I set debug-on-signal and interrupted the Emacs process to get a backtrace, attached.

Hoping Pierre will take a look as those regexps are scary!

[David Aspinall]

PS: can you elaborate on the MMM problem? From the CVS version "make compile" works cleanly for me.

[courtieu]

This should be fixed now in cvs. Please let me know if there is still a problem.