From 1466839c2182b76853380a7c91e86af30fd9778f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 23 Nov 2016 21:08:26 +0100 Subject: 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). --- coq/coq-par-test.el | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'coq/coq-par-test.el') 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)))) -- cgit v1.2.3