aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.github/workflows/test.yml6
-rw-r--r--ci/compile-tests/cct-lib.el9
-rw-r--r--coq/coq-par-compile.el1
3 files changed, 15 insertions, 1 deletions
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
index b6b5d226..15c8d3c7 100644
--- a/.github/workflows/test.yml
+++ b/.github/workflows/test.yml
@@ -133,6 +133,12 @@ jobs:
sudo apt-get update -y -q
sudo DEBIAN_FRONTEND=noninteractive apt-get install -y -q --no-install-recommends emacs
endGroup
+ startGroup other relevant configuration
+ getconf _NPROCESSORS_ONLN
+ emacs --version
+ coqc --version
+ ocaml --version
+ endGroup
startGroup Run tests
sudo chown -R coq:coq ./ci
make -C ci/compile-tests test
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 4b25956f..2685d9ae 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -223,6 +223,13 @@ or changed since recording the time in the association."
proof-auto-action-when-deactivating-scripting 'retract
proof-three-window-enable nil
coq-compile-auto-save 'save-coq
- coq--debug-auto-compilation nil))
+ coq--debug-auto-compilation nil
+ )
+ (custom-set-variables '(coq-compile-quick 'ensure-vo))
+ (when (< coq--internal-max-jobs 4)
+ (custom-set-variables '(coq-max-background-compilation-jobs 4)))
+ (message "config coq-max-background-compilation-jobs: %s (means %d)"
+ coq-max-background-compilation-jobs
+ coq--internal-max-jobs))
(provide 'cct-lib)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index c4e45af8..7d15537b 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -42,6 +42,7 @@
;; - coq-par-create-file-job detects a dependency cycle
;; - coq-par-create-file-job finds a job in every possible state
;; - coq-par-create-file-job finds a failed job
+;; - all tests in all quick and all vos variants
;;; Code: