diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-11-23 21:08:26 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-11-29 23:47:23 +0100 |
| commit | 1466839c2182b76853380a7c91e86af30fd9778f (patch) | |
| tree | 34ecbbb95902747a389674cbc8acfe30814645fc /coq/coq-par-test.el | |
| parent | d33897df4d6a2af94d0d315707111528a3c4a403 (diff) | |
support vio2vo background processing
Selecting quick-and-vio2vo will start vio2vo conversion in the
background on a subset of the available cores, see
`coq-max-background-vio2vo-percentage'. The vio2vo conversion
starts after all compilation for the require command has been
finished and the require has been processed. Because of a certain
incompatibility between .vio and .vo files (see coq issue 5223)
slowly single stepping through require commands does not
work (but processing them as a batch does).
Diffstat (limited to 'coq/coq-par-test.el')
| -rw-r--r-- | coq/coq-par-test.el | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index 4d28dc79..d22102c8 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -791,6 +791,7 @@ test the result and side effects wth `assert'." (different-not-ok t) (same-not-ok t) (last-different-time-stamp '(0 0)) + (file-descr-flattened (coq-par-test-flatten-files file-descr)) same-time-stamp file-list obj-mod-result result) (message "test case %s/576: %s %s%s" counter (car variant) file-descr @@ -862,7 +863,7 @@ test the result and side effects wth `assert'." (test-coq-par-sym-to-file dir delete-result)))) nil (concat id " delete file")) ;; check no other file is deleted - (dolist (f (coq-par-test-flatten-files file-descr)) + (dolist (f file-descr-flattened) (unless (eq f delete-result) (assert (file-attributes (test-coq-par-sym-to-file dir f)) nil (format "%s non del file %s: %s" @@ -886,6 +887,14 @@ test the result and side effects wth `assert'." (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) (get job 'use-quick)) nil (concat id " use-quick")) + ;; check vio2vo-needed property + (assert (eq + (and (eq quick-mode 'quick-and-vio2vo) + (eq req-obj-result 'vio) + (or (eq delete-result 'vo) + (not (member 'vo file-descr-flattened)))) + (get job 'vio2vo-needed)) + nil (concat id " vio2vo-needed wrong")) (ignore-errors (delete-directory dir t)))) |