Custom Query (361 matches)

Dear Proof General developers,

When I issue the proof-assert-next-command-interactive (C-c C-n) command over a comment in a Coq file, the comment is joined to the locked region and the cursor is positioned at the end of the comment. After that, I cannot insert any text: whatever I type, I get a beep and a message "Region is read-only" in the minibuffer. As far as I noticed, this only happens when I type just after I have locked a comment; after I process other Coq commands, I am able to enter text.

This happens when I am using the CVS snapshot 3.7pre070704 even with no .emacs file.

By the way, when I was writing this, the link "bug tracker" on the PG home page http://proofgeneral.inf.ed.ac.uk/ was broken.

Prover does not start when run from a Product configuration, though it starts successfully as a plugin. Exception seems to be generated by the system path management which calls the prover and its tools.

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.