proof-general/coq/ex/test-cases/README, 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
- 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 






- 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







- more coq test cases (some with surprising and embarrassing bugs)
2011-01-14T21:59:26+00:00

Hendrik Tews

2011-01-14T21:59:26+00:00

e1f5de972cbc0eb8d88675366c34ee66aca1b1b4












- move proof-no-fully-processed-buffer to generic/proof-config
2011-01-14T15:50:47+00:00

Hendrik Tews

2011-01-14T15:50:47+00:00

05f9272860f9f57e6adfa150734ea7aa29702ca7

- add documentation for it
- add a test case demonstrating it in
  coq/ex/test-cases/retract-completely-asserted





- add documentation for it
- add a test case demonstrating it in
  coq/ex/test-cases/retract-completely-asserted