proof-general/coq/ex/test-cases, branch master Emacs plugins for proof management systems - first version of parallel asynchronous compilation for coq in 2012-11-13T22:05:11+00:00 Hendrik Tews 2012-11-13T22:05:11+00:00 2243cc9d87d4993ca6b0281f7171b883dd9fd52d coq-par-compile.el (must be activated via coq-compile-parallel-in-background) - items in the queue region are not necessarily in proof-action-list any more! Require commands and the following items are stored elsewhere until the compilation finishes. Variable proof-second-action-list-active notifies the generic machinery if queue items are stored elsewhere. In this case, Proof General must neither release the proof shell lock nor delete the queue span when proof-action-list is empty. - to kill background processes as early as possible, the new hook proof-shell-signal-interrupt-hook is used 
  coq-par-compile.el (must be activated via
  coq-compile-parallel-in-background)
- items in the queue region are not necessarily in
  proof-action-list any more! Require commands and the following
  items are stored elsewhere until the compilation finishes.
  Variable proof-second-action-list-active notifies the generic
  machinery if queue items are stored elsewhere. In this case,
  Proof General must neither release the proof shell lock nor
  delete the queue span when proof-action-list is empty.
- to kill background processes as early as possible, the new hook
  proof-shell-signal-interrupt-hook is used
fix typo + add one missing cvsignore 2012-05-09T08:12:39+00:00 Hendrik Tews 2012-05-09T08:12:39+00:00 4634aede2ac4ad03007c0c66bdad8e85215789bd 






Typo
2011-12-27T13:15:11+00:00

David Aspinall

2011-12-27T13:15:11+00:00

5a754170ca3113295a1bd58f407a2e40e05cc3ff












- minor changes: clean personal todo list + adjust test case description
2011-05-20T06:38:04+00:00

Hendrik Tews

2011-05-20T06:38:04+00:00

d020f9c42ad658b05d669e10aef03f43e1605a98












- add test coq/ex/test-cases/change-ancestor for the
2011-05-12T11:59:15+00:00

Hendrik Tews

2011-05-12T11:59:15+00:00

df9f007644f89c6acd7104ea641876a868e10e89

  change-ancestor bug





  change-ancestor bug







- adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc
2011-02-28T10:10:37+00:00

Hendrik Tews

2011-02-28T10:10:37+00:00

6a9d3058e006dd826203262105adc604091326b8












- fix problem description
2011-01-26T10:43:52+00:00

Hendrik Tews

2011-01-26T10:43:52+00:00

e6fafcd7d4afc6e1d94a6db79d322499b2cb1b92












- use time-less-p
2011-01-21T09:59:35+00:00

Hendrik Tews

2011-01-21T09:59:35+00:00

e8e9187778549aa132b33321394345c99992b8b4

- delete previous-head, simplify loop
- coq 8.2 compatibility
- describe bug for killing completely asserted active buffers in
  coq/ex/test-cases/retract-completely-asserted





- delete previous-head, simplify loop
- coq 8.2 compatibility
- describe bug for killing completely asserted active buffers in
  coq/ex/test-cases/retract-completely-asserted







- fixed stale load path problem with killing the proof shell in
2011-01-18T21:46:18+00:00

Hendrik Tews

2011-01-18T21:46:18+00:00

358b338316430fe8707780985702b2a925a45abc

  the deactivation-hook





  the deactivation-hook







fix problems in test cases
2011-01-17T07:44:42+00:00

Hendrik Tews

2011-01-17T07:44:42+00:00

aa76421458123fc17a61f4b7218a175ece5e9404

coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir





coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir