all-cpus option for coq-max-background-compilation-jobs

3 files changed, 62 insertions, 18 deletions

diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index fea396f7..e24cc5b2 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -117,6 +117,36 @@ Must be used together with `coq-par-enable'."
     (coq-par-disable)
     (coq-seq-enable)))
 
+(defun number-of-cpus ()
+  (let (status ncpus)
+    (condition-case nil
+	(with-temp-buffer
+	  (setq status
+		(call-process "getconf" nil (current-buffer) nil 
+			      "_NPROCESSORS_ONLN"))
+	  (setq ncpus (string-to-number (buffer-string))))
+      (error
+       (setq status -1)))
+    (if (and (eq status 0) (> ncpus 0))
+	ncpus
+      nil)))
+
+(defvar coq-internal-max-jobs 1
+  "Value of `coq-max-background-compilation-jobs' translated to a number.")
+
+(defun coq-max-jobs-setter (symbol new-value)
+  ":set function for `coq-max-background-compilation-jobs.
+SYMBOL should be 'coq-max-background-compilation-jobs"
+  (set symbol new-value)
+  (cond
+   ((eq new-value 'all-cpus)
+    (setq new-value (number-of-cpus))
+    (unless new-value
+      (setq new-value 1)))
+   ((and (integerp new-value) (> new-value 0)) t)
+   (t (setq new-value 1)))
+  (setq coq-internal-max-jobs new-value))
+
 
 ;;; user options and variables
 
@@ -158,10 +188,18 @@ This option can be set/reset via menu
 ;; defpacustom fails to call :eval during inititialization, see trac #456
 (coq-switch-compilation-method)
 
-(defcustom coq-max-background-compilation-jobs 1
-  "Maximal number of parallel jobs, if parallel compilation is enabled."
-  :type 'integer
-  :safe (lambda (v) (and (integerp v) (> v 0)))
+(defcustom coq-max-background-compilation-jobs 'all-cpus
+  "Maximal number of parallel jobs, if parallel compilation is enabled.
+Use the number of available CPU cores if this is set to
+'all-cpus. This variable is the user setting. The value that is
+really used is `coq-internal-max-jobs'. Use `coq-max-jobs-setter'
+or the customization system to change this variable. Otherwise
+your change will have no effect, because `coq-internal-max-jobs'
+is not adapted."
+  :type '(choice (const :tag "use all CPU cores" all-cpus)
+		 (integer :tag "fixed number" :value 1))
+  :safe (lambda (v) (or (eq v 'all-cpus) (and (integerp v) (> v 0))))
+  :set 'coq-max-jobs-setter
   :group 'coq-auto-compile)
 
 (defcustom coq-compile-command ""
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index a04892b7..7bf83a4d 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -20,7 +20,6 @@
 ;; - check what happens if coq-par-coq-arguments gets a bad load path
 ;; - on error, try to location info into the error message
 ;; - handle missing coqdep/coqc gracefully
-;; - 'all-cores option for coq-max-background-compilation-jobs
 ;; 
 
 (eval-when-compile
@@ -851,8 +850,7 @@ coqdep or coqc are started for it."
   "Start background jobs until the limit is reached."
   (let ((next-job t))
     (while (and next-job
-		(< coq-current-background-jobs
-		   coq-max-background-compilation-jobs))
+		(< coq-current-background-jobs coq-internal-max-jobs))
       (setq next-job (coq-par-dequeue))
       (when next-job
 	(coq-par-start-task next-job)))))
@@ -862,7 +860,7 @@ coqdep or coqc are started for it."
 NEW-JOB goes already into the waiting queue, if the number of
 background jobs is one below the limit. This is in order to leave
 room for Proof General."
-  (if (< (1+ coq-current-background-jobs) coq-max-background-compilation-jobs)
+  (if (< (1+ coq-current-background-jobs) coq-internal-max-jobs)
       (coq-par-start-task new-job)
     (coq-par-enqueue new-job)))
 
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index f6e34827..f5149df8 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -4315,11 +4315,12 @@ compilation command. For standard dependency analysis with
 General calls @code{coqdep} and @code{coqc} as needed.
 @item
 The default compilation method is synchronous compilation. In
-order to experience parallel background compilation, 
+order to experience parallel background compilation on all your
+CPU cores, 
 enable `coq-compile-parallel-in-background' (menu @code{Coq ->
-Settings -> Compile Parallel In Background}) and set
-`coq-max-background-compilation-jobs' to the number of spare
-cores.
+Settings -> Compile Parallel In Background}). Configure 
+@code{coq-max-background-compilation-jobs} if you want to limit
+the number of parallel background jobs.
 @end itemize
 
 
@@ -4414,11 +4415,12 @@ locked until compilation finishes. Use @code{C-g} to interrupt
 compilation. 
 @item Parallel asynchronous compilation
 This is the new version added in Proof General version 4.3. It
-runs up to `coq-max-background-compilation-jobs' coqdep and coqc
-jobs in parallel in asynchronous subprocesses. Your Emacs
-will stay responsive during compilation. Use @code{C-c C-c} or
-the tool bar icons for interrupt or restart to interrupt
-compilation. 
+runs up to @code{coq-max-background-compilation-jobs} coqdep and
+coqc jobs in parallel in asynchronous subprocesses (or uses all
+your CPU cores if @code{coq-max-background-compilation-jobs}
+equals @code{'all-cpus}). Your Emacs will stay responsive during
+compilation. Use @code{C-c C-c} or the tool bar icons for
+interrupt or restart to interrupt compilation.
 
 For the usual case, you have at most
 `coq-max-background-compilation-jobs' parallel processes
@@ -4537,7 +4539,13 @@ This option can be set/reset via menu
 
 @c TEXI DOCSTRING MAGIC: coq-max-background-compilation-jobs
 @defvar coq-max-background-compilation-jobs 
-Maximal number of parallel jobs, if parallel compilation is enabled.
+Maximal number of parallel jobs, if parallel compilation is enabled.@*
+Use the number of available CPU cores if this is set to
+@code{'all-cpus}. This variable is the user setting. The value that is
+really used is @samp{@code{coq-internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}}
+or the customization system to change this variable. Otherwise
+your change will have no effect, because @samp{@code{coq-internal-max-jobs}}
+is not adapted.
 @end defvar