From 70183fa234acec75f024c4821942771f1a1a3b6c Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 14 Nov 2012 11:38:50 +0000 Subject: all-cpus option for coq-max-background-compilation-jobs --- coq/coq-compile-common.el | 46 ++++++++++++++++++++++++++++++++++++++++++---- coq/coq-par-compile.el | 6 ++---- doc/ProofGeneral.texi | 28 ++++++++++++++++++---------- 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 -- cgit v1.2.3