diff options
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 108 |
1 files changed, 54 insertions, 54 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index c94cd8b7..936ad923 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -78,7 +78,7 @@ Must be used together with `coq-par-enable'." (defun coq-switch-compilation-method () - "Set function for coq-compile-parallel-in-background." + "Set function for function ‘coq-compile-parallel-in-background’." (if coq-compile-parallel-in-background (progn (coq-par-enable) @@ -91,7 +91,7 @@ Must be used together with `coq-par-enable'." (condition-case nil (with-temp-buffer (setq status - (call-process "getconf" nil (current-buffer) t + (call-process "getconf" nil (current-buffer) t "_NPROCESSORS_ONLN")) (setq ncpus (string-to-number (buffer-string)))) (error @@ -103,7 +103,7 @@ Must be used together with `coq-par-enable'." (defvar coq--max-background-vio2vo-percentage-shadow 40 "Internal shadow value of `coq-max-background-vio2vo-percentage'. This variable does always contain the same value as -`coq-max-background-vio2vo-percentage'. It is used only to break +`coq-max-background-vio2vo-percentage'. It is used only to break the dependency cycle between `coq-set-max-vio2vo-jobs' and `coq-max-background-vio2vo-percentage'.") @@ -167,7 +167,7 @@ Ignore any quick setting for Coq versions before 8.5." (defcustom coq-compile-before-require nil "If non-nil, check dependencies of required modules and compile if necessary. If non-nil ProofGeneral intercepts \"Require\" commands and checks if the -required library module and its dependencies are up-to-date. If not, they +required library module and its dependencies are up-to-date. If not, they are compiled from the sources before the \"Require\" command is processed. This option can be set/reset via menu @@ -181,12 +181,12 @@ This option can be set/reset via menu (defcustom coq-compile-parallel-in-background nil "Choose the internal compilation method. When Proof General compiles itself, you have the choice between -two implementations. If this setting is nil, then Proof General +two implementations. If this setting is nil, then Proof General uses the old implementation and compiles everything sequentially -with synchronous job. With this old method Proof General is -locked during compilation. If this setting is t, then the new +with synchronous job. With this old method Proof General is +locked during compilation. If this setting is t, then the new method is used and compilation jobs are dispatched in parallel in -the background. The maximal number of parallel compilation jobs +the background. The maximal number of parallel compilation jobs is set with `coq-max-background-compilation-jobs'. This option can be set/reset via menu @@ -207,58 +207,58 @@ This option can be set/reset via menu "Control quick compilation, vio2vo and vio/vo files auto compilation. This option controls whether ``-quick'' is used for parallel background compilation and whether up-date .vo or .vio files are -used or deleted. Please use the customization system to change +used or deleted. Please use the customization system to change this option to ensure that any ``-quick'' setting is ignored for Coq before 8.5. Note that ``-quick'' can be noticebly slower when your sources do -not declare section variables with ``Proof using''. Note that +not declare section variables with ``Proof using''. Note that even if you do declare section variables, ``-quick'' is typically slower on small files. Use the default `no-quick', if you have not yet switched to -``Proof using''. Use `quick-no-vio2vo', if you want quick -recompilation without producing .vo files. Value +``Proof using''. Use `quick-no-vio2vo', if you want quick +recompilation without producing .vo files. Value `quick-and-vio2vo' updates missing prerequisites with ``-quick'' and starts vio2vo conversion on a subset of the availables cores (see `coq-compile-vio2vo-percentage') when the quick recompilation finished (but see below for a .vio .vo -incompatibility caveat). Note that all the previously described +incompatibility caveat). Note that all the previously described modes might load .vio files and that you therefore might not -notice certain universe inconsistencies. Finally, use `ensure-vo' +notice certain universe inconsistencies. Finally, use `ensure-vo' for only importing .vo files with complete universe checks. Detailed description of the 4 modes: no-quick Compile outdated prerequisites without ``-quick'', producing .vo files, but don't compile prerequisites - for which an up-to-date .vio file exists. Delete + for which an up-to-date .vio file exists. Delete or overwrite outdated .vo files. quick-no-vio2vo Compile outdated prerequisites with ``-quick'', producing .vio files, but don't compile prerequisites - for which an up-to-date .vo file exists. Delete + for which an up-to-date .vo file exists. Delete or overwrite outdated .vio files. quick-and-vio2vo Same as `quick-no-vio2vo', but start vio2vo processes after the last ``Require'' command has been processed - to convert the vio dependencies into vo files. With this + to convert the vio dependencies into vo files. With this mode you might see asynchronous errors from vio2vo compilation while you are processing stuff far below the - last require. vio2vo compilation is done on a subset of + last require. vio2vo compilation is done on a subset of the available cores, see `coq-compile-vio2vo-percentage'. When `coq-compile-keep-going' is set, vio2vo compilation is scheduled for those files for which coqc compilation was successful. Warning: This mode does only work when you process require - commands in batches. Slowly single-stepping through require's + commands in batches. Slowly single-stepping through require's might lead to inconsistency errors when loading some libraries, see Coq issue #5223. ensure-vo Ensure that all library dependencies are present as .vo files and delete outdated .vio files or .vio files that - are more recent than the corresponding .vo file. This + are more recent than the corresponding .vo file. This setting is the only one that ensures soundness. This option can be set via menu @@ -296,9 +296,9 @@ This option can be set/reset via menu (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 +'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) @@ -326,13 +326,13 @@ with 'quick-and-vio2vo, see Coq issue #5223." :group 'coq-auto-compile) (defcustom coq-compile-command "" - "External compilation command. If empty ProofGeneral compiles itself. + "External compilation command. If empty ProofGeneral compiles itself. If unset (the empty string) ProofGeneral computes the dependencies of -required modules with coqdep and compiles as necessary. This internal +required modules with coqdep and compiles as necessary. This internal dependency checking does currently not handle ML modules. If a non-empty string, the denoted command is called to do the -dependency checking and compilation. Before executing this +dependency checking and compilation. Before executing this command the following keys are substituted as follows: %p the (physical) directory containing the source of the required module @@ -363,8 +363,8 @@ minibuffer if `coq-confirm-external-compilation' is t." ("%r" requiring-file)) "Substitutions for `coq-compile-command'. Value must be a list of substitutions, where each substitution is -a 2-element list. The first element of a substitution is the -regexp to substitute, the second the replacement. The replacement +a 2-element list. The first element of a substitution is the +regexp to substitute, the second the replacement. The replacement is evaluated before passing it to `replace-regexp-in-string', so it might be a string, or one of the symbols 'physical-dir, 'module-object, 'module-source, 'qualified-id and @@ -380,7 +380,7 @@ that contains the \"Require\".") "Buffers to save before checking dependencies for compilation. There are two orthogonal choices: Firstly one can save all or only the coq buffers, where coq buffers means all buffers in coq mode except the current -buffer. Secondly, Emacs can ask about each such buffer or save all of them +buffer. Secondly, Emacs can ask about each such buffer or save all of them unconditionally. This makes four permitted values: 'ask-coq to confirm saving all @@ -407,7 +407,7 @@ This option can be set via menu (defcustom coq-lock-ancestors t "If non-nil, lock ancestor module files. If external compilation is used (via `coq-compile-command') then -only the direct ancestors are locked. Otherwise all ancestors are +only the direct ancestors are locked. Otherwise all ancestors are locked when the \"Require\" command is processed. This option can be set via menu @@ -433,12 +433,12 @@ This option can be set/reset via menu (defcustom coq-compile-ignored-directories nil "Directories in which ProofGeneral should not compile modules. List of regular expressions for directories in which ProofGeneral -should not compile modules. If a library file name matches one +should not compile modules. If a library file name matches one of the regular expressions in this list then ProofGeneral does neither compile this file nor check its dependencies for -compilation. It makes sense to include non-standard coq library +compilation. It makes sense to include non-standard coq library directories here if they are not changed and if they are so big -that dependency checking takes noticeable time. The regular +that dependency checking takes noticeable time. The regular expressions in here are always matched against the .vo file name, regardless whether ``-quick'' would be used to compile the file or not." @@ -451,12 +451,12 @@ or not." "and has not been found") "Regexp to match errors in the output of coqdep. coqdep indicates errors not always via a non-zero exit status, -but sometimes only via printing warnings. This regular expression +but sometimes only via printing warnings. This regular expression is used for recognizing error conditions in the output of -coqdep (when coqdep terminates with exit status 0). Its default +coqdep (when coqdep terminates with exit status 0). Its default value matches the warning that some required library cannot be found on the load path and ignores the warning for finding a -library at multiple places in the load path. If you want to turn +library at multiple places in the load path. If you want to turn the latter condition into an error, then set this variable to \"^\\*\\*\\* Warning\"." :type 'string @@ -468,7 +468,7 @@ the latter condition into an error, then set this variable to "[ \t\n]*\\([A-Za-z0-9_']+\\(\\.[A-Za-z0-9_']+\\)*\\)[ \t\n]*" "Regular expression matching one Coq module identifier. Should match precisely one complete module identifier and surrounding -white space. The module identifier must be matched with group number 1. +white space. The module identifier must be matched with group number 1. Note that the trailing dot in \"Require A.\" is not part of the module identifier and should therefore not be matched by this regexp.") @@ -488,25 +488,25 @@ modules are matched separately with `coq-require-id-regexp'") "Name of the buffer to display error messages from coqc and coqdep.") (defvar coq--debug-auto-compilation nil - "*Display more messages during compilation") + "*Display more messages during compilation.") ;;; basic utilities (defun time-less-or-equal (time-1 time-2) - "Return `t' if time value time-1 is earlier or equal to time-2. + "Return t if time value TIME-1 is earlier or equal to TIME-2. A time value is a list of two, three or four integers of the form (high low micro pico) as returned by `file-attributes' or -'current-time'. First element high contains the upper 16 bits and +'current-time'. First element high contains the upper 16 bits and the second low the lower 16 bits of the time." (not (time-less-p time-2 time-1))) (defun coq-max-dep-mod-time (dep-mod-times) "Return the maximum in DEP-MOD-TIMES. Argument DEP-MOD-TIMES is a list where each element is either a -time value (see `time-less-or-equal') or 'just-compiled. The +time value (see `time-less-or-equal') or 'just-compiled. The function returns the maximum of the elements in DEP-MOD-TIMES, -where 'just-compiled is considered the greatest time value. If +where 'just-compiled is considered the greatest time value. If DEP-MOD-TIMES is empty it returns nil." (let ((max nil)) (while dep-mod-times @@ -526,10 +526,10 @@ DEP-MOD-TIMES is empty it returns nil." (defun coq-compile-ignore-file (lib-obj-file) "Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE. -Return `t' if ProofGeneral should skip LIB-OBJ-FILE and `nil' if -ProofGeneral should handle the file. For normal users it does, +Return t if ProofGeneral should skip LIB-OBJ-FILE and nil if +ProofGeneral should handle the file. For normal users it does, for instance, not make sense to let ProofGeneral check if the coq -standard library is up-to-date. This function is always invoked +standard library is up-to-date. This function is always invoked on the .vo file name, regardless whether the file would be compiled with ``-quick'' or not." (if (some @@ -556,7 +556,7 @@ Chops off the last character of LIB-OBJ-FILE to convert \"x.vo\" to \"x.v\"." (defun coq-library-vio-of-vo-file (vo-obj-file) "Return .vio file name for VO-OBJ-FILE. -Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." +Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." (concat (coq-library-src-of-vo-file vo-obj-file) "io")) @@ -583,7 +583,7 @@ Changes the suffix from .vio to .vo. VO-OBJ-FILE must have a .vo suffix." (defun coq-compile-display-error (command error-message display) "Display COMMAND and ERROR-MESSAGE in `coq--compile-response-buffer'. -If needed, reinitialize `coq--compile-response-buffer'. Then +If needed, reinitialize `coq--compile-response-buffer'. Then display COMMAND and ERROR-MESSAGE." (unless (buffer-live-p (get-buffer coq--compile-response-buffer)) (coq-init-compile-response-buffer)) @@ -598,10 +598,10 @@ display COMMAND and ERROR-MESSAGE." (defun coq-init-compile-response-buffer (&optional command) "Initialize the buffer for the compilation output. -If `coq--compile-response-buffer' exists, empty it. Otherwise +If `coq--compile-response-buffer' exists, empty it. Otherwise create a buffer with name `coq--compile-response-buffer', put it into `compilation-mode' and store it in -`coq--compile-response-buffer' for later use. Argument COMMAND is +`coq--compile-response-buffer' for later use. Argument COMMAND is the command whose output will appear in the buffer." (let ((buffer-object (get-buffer coq--compile-response-buffer))) (if buffer-object @@ -675,10 +675,10 @@ from `coq-compile-save-some-buffers' to (defun coq-compile-save-buffer-filter () "Filter predicate for `coq-compile-save-some-buffers'. -See also `save-some-buffers'. Returns t for buffers with major +See also `save-some-buffers'. Return t for buffers with major mode 'coq-mode' different from `coq-compile-buffer-with-current-require' and nil for all other -buffers. The buffer to test must be current." +buffers. The buffer to test must be current." (and (eq major-mode 'coq-mode) (not (eq coq-compile-buffer-with-current-require @@ -686,7 +686,7 @@ buffers. The buffer to test must be current." (defun coq-compile-save-some-buffers () "Save buffers according to `coq-compile-auto-save'. -Uses the local variable coq-compile-buffer-with-current-require to pass the +Uses the local variable ‘coq-compile-buffer-with-current-require’ to pass the current buffer (which contains the Require command) to `coq-compile-save-buffer-filter'." (let ((coq-compile-buffer-with-current-require (current-buffer)) @@ -711,10 +711,10 @@ current buffer (which contains the Require command) to (defun coq-switch-buffer-kill-proof-shell () "Kill the proof shell without asking the user. -This function is for `proof-deactivate-scripting-hook'. It kills +This function is for `proof-deactivate-scripting-hook'. It kills the proof shell without asking the user for confirmation (assuming she agreed already on switching the active -scripting buffer). This is needed to ensure the load path is +scripting buffer). This is needed to ensure the load path is correct in the new scripting buffer." (unless proof-shell-exit-in-progress (proof-shell-exit t))) |