Timeline



Nov 9, 2010:

1:12 PM Ticket #379 (Syntax error in ProofGeneral.desktop file) closed by David Aspinall
fixed: Thanks for noticing this. It seems to be complaining because the …
9:55 AM Ticket #379 (Syntax error in ProofGeneral.desktop file) created by Robin Green
I receive the following message from KDE on my terminal periodically: …
9:34 AM Ticket #378 (Makefile "make" should detect wrong bytecode file version and rebuild) created by Robin Green
I am using emacs 23.2 exclusively - no other versions of emacs. …

Oct 11, 2010:

9:34 AM Ticket #336 (Toolbar images on Mac Emacsen are super-ugly) reopened by David Aspinall
Note: background is better, but the scaling of png icons still …
1:01 AM Ticket #336 (Toolbar images on Mac Emacsen are super-ugly) closed by David Aspinall
fixed: pngs were given white background instead of transparency.
12:34 AM WikiStart edited by David Aspinall
(diff)
12:23 AM Ticket #377 (Electric-terminator mode next line movement changed) created by megacz
When electric-terminator mode is enabled, after I type a period the …

Oct 10, 2010:

11:39 PM Ticket #376 (Enable and complete testing of parser cache, add to user options menu) created by David Aspinall
PG has a cache available to reduce the amount of parsing that takes …
11:36 PM Milestone PG-Emacs-4.0 completed
Proof General 4.0 will only support GNU Emacs, version 23.
11:35 PM Ticket #366 (Fix documentation for mouse button commands) closed by David Aspinall
fixed
3:25 PM Ticket #371 (electric terminator mode broken) closed by David Aspinall
fixed: I reconsidered. The behaviour should now be pretty close to PG 3.7, …
1:20 PM Ticket #375 (PG goes into infinite loop with 100% CPU usage) closed by David Aspinall
invalid: This is indeed ugly, but it isn't PG's fault. Instead of testing …
1:02 PM Ticket #370 (Proof General immediately starts processing the file as soon as I open it) closed by David Aspinall
invalid: Yes, I can repeat the effect with your .emacs, but it is buggy. In …
6:49 AM Ticket #370 (Proof General immediately starts processing the file as soon as I open it) reopened by megacz
Nope, the bug is definitely there. It occurs even if these are the …

Oct 8, 2010:

10:14 AM Ticket #370 (Proof General immediately starts processing the file as soon as I open it) closed by David Aspinall
worksforme: I can't reproduce this, even adding your key binding. It sounds like …
9:54 AM Ticket #373 (PG 4.0 forgets things.) closed by David Aspinall
needmoreinfo: Thanks for the report. It doesn't look good, but the screenshot …
9:51 AM Ticket #372 (funny => sign all over my scripts) closed by David Aspinall
invalid: This is the "overlay arrow", you are seeing the crude tty equivalent …
7:51 AM Ticket #375 (PG goes into infinite loop with 100% CPU usage) created by megacz
To reproduce: download the attachment. Then type: emacs -nw pg_bug3.v …
7:40 AM Ticket #374 (cannot turn on electric-terminator interactively) closed by megacz
invalid: Er, nevermind, I didn't know the keystroke depended on which proof …
7:31 AM Ticket #374 (cannot turn on electric-terminator interactively) created by megacz
I seem to be able to enable the electric-terminator using a hook in my …

Oct 7, 2010:

7:13 AM Ticket #373 (PG 4.0 forgets things.) created by megacz
Something is going very, very wrong with the proof state... see screenshot.
7:13 AM Ticket #372 (funny => sign all over my scripts) created by megacz
for some reason proof general 4.0 is putting this funny "=>" symbol …
7:12 AM Ticket #371 (electric terminator mode broken) created by megacz
Electric terminator mode isn't working anymore with PG 4.0. When I …
7:11 AM Ticket #370 (Proof General immediately starts processing the file as soon as I open it) created by megacz
Proof General immediately starts processing my script as soon as I …

Oct 6, 2010:

11:05 AM Ticket #369 (PG will not compile under non-windowing Emacs) closed by David Aspinall
fixed: Thanks for the report. You were trying to compile using Mac OS X's …
5:37 AM Ticket #369 (PG will not compile under non-windowing Emacs) created by megacz
emacs --batch --no-site-file -q -eval '(setq load-path (append …

Oct 4, 2010:

8:40 PM Ticket #339 (Infinite loop on module print with coq-8.3) closed by David Aspinall
fixed: Pierre says this is the same as #140.
6:12 PM Ticket #368 (coq, already defined values) closed by David Aspinall
needmoreinfo: Thanks for the report. Unfortunately I can't reproduce this, using …
5:57 PM Ticket #339 (Infinite loop on module print with coq-8.3) reopened by David Aspinall
Could someone check whether this is fixed by same fix as #140?
5:48 PM Ticket #368 (coq, already defined values) created by Damien Pous
Hi, The following code is rejected by Coq, since [x] is already …
3:39 PM Ticket #367 (Fix web pages and update screenshots) created by David Aspinall
Some links on web pages have rusted, and screenshots need updating.
2:45 PM Ticket #357 (Feature suggestion: function + binding to insert Coq closing tactics) closed by David Aspinall
fixed: Patch applied, many thanks!
2:39 PM Ticket #365 (Fix three mouse bindings in proof-menu.el, pg-goals.el, and pg-vars.el) closed by David Aspinall
fixed: Patch applied, many thanks!
2:34 PM Ticket #366 (Fix documentation for mouse button commands) created by David Aspinall
The manual has an incomplete list and bindings which are old.
2:27 PM Ticket #362 (Proof Completed message for Coq is lost) closed by David Aspinall
fixed: Fixed already

Oct 2, 2010:

1:47 AM Ticket #365 (Fix three mouse bindings in proof-menu.el, pg-goals.el, and pg-vars.el) created by Erik Martin-Dorel
The "mouse bindings" associated with proof-mouse-goto-point, …

Oct 1, 2010:

5:32 PM Ticket #168 (Reorganise TODO files in distribution) closed by David Aspinall
fixed: This stuff is lost in the mists of time, really…
5:32 PM Ticket #316 (UI glitch: point still jumps about when follow-mode=never move) closed by David Aspinall
fixed: Can't reproduce this now, should be fixed with other cleanups.
5:20 PM Ticket #261 (Finish support for proof-query-identifier) closed by David Aspinall
fixed: Documentation added now, and a few cleanups.
5:12 PM Ticket #364 (Unify proof-query-identifier and pg-identifier-near-point-query (cleanup)) created by David Aspinall
These functions are almost the same, except that the latter adds a …
4:04 PM Ticket #356 (Coq identifiers are unexpectedly colorized) closed by courtieu
fixed: Hello, Thanks! This is (re)fixed in cvs. I hope there are no other …
3:56 PM Ticket #363 (Multiple file handling for Coq needs sensible treatment) created by David Aspinall
We need to find a way to make Proof General development across …
3:53 PM Ticket #362 (Proof Completed message for Coq is lost) created by courtieu
This is misleading because people think the proof is not finished. …
3:02 PM Ticket #361 (Generic adjustment of prover's pretty-printing width) created by David Aspinall
See pg-user.el version 10.52 for commented out code.
1:00 PM Ticket #359 (Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & ...) closed by David Aspinall
fixed: Applied patch, many thanks!
12:34 PM Ticket #360 (link to proof general is broken and lacks helpful message) closed by David Aspinall
fixed: OK, reformatted just for you. You only needed to read one line higher …

Sep 29, 2010:

10:33 AM Ticket #356 (Coq identifiers are unexpectedly colorized) reopened by Erik Martin-Dorel
Thanks for the fix. But I reopen the ticket since it seems to me …

Sep 28, 2010:

8:29 PM Ticket #360 (link to proof general is broken and lacks helpful message) created by megacz
The link to Proof General 4.0 on …
5:34 PM Ticket #356 (Coq identifiers are unexpectedly colorized) closed by courtieu
fixed: This should be fixed in cvs now. Thanks a lot for reporting.

Sep 27, 2010:

1:53 AM Ticket #359 (Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & ...) created by Erik Martin-Dorel
I suggest to fix 3 key bindings issues in coq/coq.el: The correct …
1:24 AM Ticket #358 (link to proof general is broken) closed by David Aspinall
invalid: Not a bug, 4.0 not yet released. Sorry for confusion.

Sep 25, 2010:

7:47 PM Ticket #358 (link to proof general is broken) created by megacz
The link to Proof General 4.0 on …

Sep 22, 2010:

9:06 PM Ticket #357 (Feature suggestion: function + binding to insert Coq closing tactics) created by Erik Martin-Dorel
I have noticed that Coq closing tactics are defined in …
8:34 PM Ticket #356 (Coq identifiers are unexpectedly colorized) created by Erik Martin-Dorel
I have just done a cvs update, and the Coq font lock seems to be …
4:11 PM Ticket #140 (PG takes a long time printing module types in Coq) closed by courtieu
fixed: This should be fixed now in cvs. Please let me know if there is still …
1:39 AM Ticket #352 (Unexpected shift in toolbar buttons) closed by David Aspinall
fixed: Confirmed, thanks for the recipe to reproduce this. Now fixed. It …
1:06 AM Ticket #355 (Autosend should be re-engaged after C-c C-n) created by David Aspinall
In case autosending is interrupted but the user hits C-c C-n, …

Sep 21, 2010:

6:09 PM Ticket #140 (PG takes a long time printing module types in Coq) reopened by Evgeny Makarov
I am sorry I did not respond to your requests for more information. I …

Sep 17, 2010:

11:30 AM Ticket #352 (Unexpected shift in toolbar buttons) reopened by Erik Martin-Dorel
The problem is actually reproducible when I use …

Sep 16, 2010:

3:29 PM Ticket #352 (Unexpected shift in toolbar buttons) closed by David Aspinall
needmoreinfo

Sep 14, 2010:

1:30 PM Ticket #354 (synchronisation lost with "process rest" and "undo") created by nils
this error is not really reproducible, but nevertheless occurs quite …
11:03 AM Ticket #353 ("undo last proof command" does not work at the end of theory) created by nils
there are only ML commands in this theory, and when it is processed …

Sep 12, 2010:

6:05 PM Ticket #352 (Unexpected shift in toolbar buttons) created by Erik Martin-Dorel
In the current ProofGeneral toolbar, the tooltip and underlying …
Note: See TracTimeline for information about the timeline view.