From 60bf4ce887474116a152045296ff849e4fa00402 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 30 Nov 2016 12:22:37 +0100 Subject: use coq-- for internal compilation variables --- coq/coq-par-compile.el | 278 ++++++++++++++++++++++++------------------------- 1 file changed, 139 insertions(+), 139 deletions(-) (limited to 'coq/coq-par-compile.el') diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 00ddedbc..6dbfb109 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -102,7 +102,7 @@ ;; ;; The problem is solved with the 'coq-locked-ancestors property of ;; spans that contain Require commands and with the -;; coq-par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors +;; coq--par-ancestor-files hash. Ancestors in the 'coq-locked-ancestors ;; property are unlocked when this span is retracted. As locking is ;; done eagerly (as soon as coqdep runs first on the file), I only ;; have to make sure the right files appear in 'coq-locked-ancestors. @@ -111,7 +111,7 @@ ;; walks upwards the dependency tree. In the end, every top-level job ;; contains a list of all its direct and indirect ancestors. Because ;; of eager locking, all its ancestors are already locked, when a -;; top-level job is about to be retired. The coq-par-ancestor-files +;; top-level job is about to be retired. The coq--par-ancestor-files ;; hash therefore records whether some ancestor does already appear in ;; the 'coq-locked-ancestors property of some span before the current ;; one. If it doesn't, I store it in the current span. @@ -244,7 +244,7 @@ ;; the process is killed ;; ;; -;; Symbols in the coq-par-ancestor-files hash +;; Symbols in the coq--par-ancestor-files hash ;; ;; This hash maps file names to symbols. A file is present in the ;; hash, if it has been locked. @@ -269,7 +269,7 @@ ;; (mapc (lambda (p) (when (eq (get p 'type) 'clone) ;; (push p clones))) ;; (get v 'coqc-dependants))) -;; coq-compilation-object-hash) +;; coq--compilation-object-hash) ;; (mapc (lambda (v) ;; (message "%s type %s for %s state %s dep of %s queue dep of %s" ;; (get v 'name) @@ -283,7 +283,7 @@ ;;; Variables -(defvar coq-par-ancestor-files nil +(defvar coq--par-ancestor-files nil "Hash remembering the state of locked ancestor files. This hash maps true file names (in the sense of `file-truename') to either 'locked or 'asserted. @@ -299,10 +299,10 @@ asserted region. asserted required module (and is in some 'coq-locked-ancestors property).") -(defvar coq-current-background-jobs 0 +(defvar coq--current-background-jobs 0 "Number of currently running background jobs.") -(defvar coq-compilation-object-hash nil +(defvar coq--compilation-object-hash nil "Hash for storing the compilation jobs. This hash only stores real compilation jobs and no clones. They are stored in order to avoid double compilation. The jobs stored @@ -311,17 +311,17 @@ information in their property list. See the documentation in the source file \"coq-par-compile.el\". The hash always maps .vo file names to compilation jobs, regardless of ``-quick''.") -(defvar coq-last-compilation-job nil +(defvar coq--last-compilation-job nil "Pointer to the last top-level compilation job. Used to link top-level jobs with queue dependencies.") -(defvar coq-compile-vio2vo-in-progress nil +(defvar coq--compile-vio2vo-in-progress nil "Set to t iff vio2vo is running in background.") -(defvar coq-compile-vio2vo-delay-timer nil +(defvar coq--compile-vio2vo-delay-timer nil "Holds the timer for the vio2vo delay.") -(defvar coq-par-next-id 1 +(defvar coq--par-next-id 1 "Increased for every job and process, to get unique job names. The names are only used for debugging.") @@ -363,15 +363,15 @@ latter greater then everything else." (t (time-less-p time-1 time-2)))) (defun coq-par-init-compilation-hash () - "(Re-)Initialize `coq-compilation-object-hash'." - (setq coq-compilation-object-hash (make-hash-table :test 'equal))) + "(Re-)Initialize `coq--compilation-object-hash'." + (setq coq--compilation-object-hash (make-hash-table :test 'equal))) (defun coq-par-init-ancestor-hash () - "(Re-)Initialize `coq-par-ancestor-files'" - (setq coq-par-ancestor-files (make-hash-table :test 'equal)) + "(Re-)Initialize `coq--par-ancestor-files'" + (setq coq--par-ancestor-files (make-hash-table :test 'equal)) (mapc (lambda (locked-anc) - (puthash locked-anc 'asserted coq-par-ancestor-files)) + (puthash locked-anc 'asserted coq--par-ancestor-files)) proof-included-files-list)) ;;; generic queues @@ -405,13 +405,13 @@ queue.") (defun coq-par-job-enqueue (job) "Insert job in the queue of waiting compilation jobs." (coq-par-enqueue coq-par-compilation-queue job) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: enqueue job in waiting queue" (get job 'name)))) (defun coq-par-job-dequeue () "Dequeue the next job from the compilation queue." (let ((res (coq-par-dequeue coq-par-compilation-queue))) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (if res (message "%s: dequeue" (get res 'name)) (message "compilation queue empty"))) @@ -428,13 +428,13 @@ access the queue.") (defun coq-par-vio2vo-enqueue (job) "Insert JOB in the queue for vio2vo processing." (coq-par-enqueue coq-par-vio2vo-queue job) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: enqueue job in vio2vo queue" (get job 'name)))) (defun coq-par-vio2vo-dequeue () "Dequeue the next job from the vio2vo queue." (let ((res (coq-par-dequeue coq-par-vio2vo-queue))) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (if res (message "%s: vio2vo dequeue" (get res 'name)) (message "vio2vo queue empty"))) @@ -530,13 +530,13 @@ If no circle is found return nil, otherwise the list of files belonging to the circle." (let (cycle result) (maphash (lambda (key job) (put job 'visited nil)) - coq-compilation-object-hash) + coq--compilation-object-hash) (maphash (lambda (key job) (when (and (not cycle) (not (get job 'visited)) (eq (get job 'state) 'waiting-dep)) (setq cycle (coq-par-find-dependency-circle-for-job job nil)))) - coq-compilation-object-hash) + coq--compilation-object-hash) (dolist (j cycle) (when (eq (get j 'type) 'file) (push (get j 'src-file) result))) @@ -570,7 +570,7 @@ this buffer visible and returns a string. This function does always return .vo dependencies, regardless of the value of `coq-compile-quick'. If necessary, the conversion into .vio files must be done elsewhere." - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "analyse coqdep output \"%s\"" output)) (if (or (not (eq status 0)) @@ -625,10 +625,10 @@ depending on `coq-compile-quick', must be done elsewhere." (cons command-intro this-command) this-command)) coqdep-status coqdep-output) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "Run synchronously: %s" (mapconcat 'identity full-command " "))) - ;; (if coq-debug-auto-compilation + ;; (if coq--debug-auto-compilation ;; (message "CPGLD: call coqdep arg list: %s" coqdep-arguments)) (with-temp-buffer (setq coqdep-status @@ -636,7 +636,7 @@ depending on `coq-compile-quick', must be done elsewhere." coq-dependency-analyzer nil (current-buffer) nil coqdep-arguments)) (setq coqdep-output (buffer-string))) - ;; (if coq-debug-auto-compilation + ;; (if coq--debug-auto-compilation ;; (message "CPGLD: coqdep status %s, output on %s: %s" ;; coqdep-status lib-src-file coqdep-output)) (coq-par-analyse-coq-dep-exit coqdep-status coqdep-output full-command))) @@ -676,7 +676,7 @@ function returns () if MODULE-ID comes from the standard library." coq-load-path (concat "echo \"" coq-string "\" > " temp-require-file ";")))) (delete-file temp-require-file)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "coq-par-get-library-dependencies delivered \"%s\"" result)) (if (stringp result) ;; Error handling: coq-par-get-library-dependencies was not able to @@ -726,38 +726,38 @@ function returns () if MODULE-ID comes from the standard library." (when (process-get process 'coq-compilation-job) (process-put process 'coq-par-process-killed t) (delete-process process) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s %s: kill it" (get (process-get process 'coq-compilation-job) 'name) (process-name process))))) (process-list)) - (setq coq-current-background-jobs 0))) + (setq coq--current-background-jobs 0))) (defun coq-par-unlock-ancestors-on-error () "Unlock ancestors which are not in an asserted span. Used for unlocking ancestors on compilation errors." - (when coq-par-ancestor-files + (when coq--par-ancestor-files ;; nil e.g. when enabling on-the-fly compilation after processing imports. (maphash (lambda (ancestor state) (when (eq state 'locked) (coq-unlock-ancestor ancestor) - (puthash ancestor nil coq-par-ancestor-files))) - coq-par-ancestor-files))) + (puthash ancestor nil coq--par-ancestor-files))) + coq--par-ancestor-files))) (defun coq-par-emergency-cleanup () "Emergency cleanup for parallel background compilation. Kills all processes, unlocks ancestors, clears the queue region and resets the internal state." - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "emergency cleanup")) (coq-par-kill-all-processes) (setq coq-par-compilation-queue (coq-par-new-queue)) - (setq coq-last-compilation-job nil) + (setq coq--last-compilation-job nil) (setq coq-par-vio2vo-queue (coq-par-new-queue)) - (setq coq-compile-vio2vo-in-progress nil) - (when coq-compile-vio2vo-delay-timer - (cancel-timer coq-compile-vio2vo-delay-timer)) + (setq coq--compile-vio2vo-in-progress nil) + (when coq--compile-vio2vo-delay-timer + (cancel-timer coq--compile-vio2vo-delay-timer)) (when proof-action-list (setq proof-shell-interrupt-pending t)) (coq-par-unlock-ancestors-on-error) @@ -778,10 +778,10 @@ compilation job JOB, making sure that CONTINUATION runs when the process finishes successfully. FILE-RM, if not nil, denotes a file to be deleted when the process is killed." (let ((process-connection-type nil) ; use pipes - (process-name (format "pro-%s" coq-par-next-id)) + (process-name (format "pro-%s" coq--par-next-id)) process) (with-current-buffer (or proof-script-buffer (current-buffer)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s %s: start %s %s in %s" (get job 'name) process-name command (mapconcat 'identity arguments " ") @@ -800,8 +800,8 @@ file to be deleted when the process is killed." (set-process-filter process 'coq-par-process-filter) (set-process-sentinel process 'coq-par-process-sentinel) (set-process-query-on-exit-flag process nil) - (setq coq-par-next-id (1+ coq-par-next-id)) - (setq coq-current-background-jobs (1+ coq-current-background-jobs)) + (setq coq--par-next-id (1+ coq--par-next-id)) + (setq coq--current-background-jobs (1+ coq--current-background-jobs)) (process-put process 'coq-compilation-job job) (process-put process 'coq-process-continuation continuation) (process-put process 'coq-process-command (cons command arguments)) @@ -817,7 +817,7 @@ errors are reported with an error message." (condition-case err (if (process-get process 'coq-par-process-killed) (progn - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s %s: skip sentinel, process killed, %s" (get (process-get process 'coq-compilation-job) 'name) (process-name process) @@ -830,13 +830,13 @@ errors are reported with an error message." (delete-file (process-get process 'coq-process-rm)))) (when (eq (process-get process 'coq-process-continuation) 'coq-par-vio2vo-continuation) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: reenqueue for vio2vo" (get (process-get process 'coq-compilation-job) 'name))) (coq-par-vio2vo-enqueue (process-get process 'coq-compilation-job)))) (let (exit-status) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s %s: process status changed to %s" (get (process-get process 'coq-compilation-job) 'name) (process-name process) @@ -845,18 +845,18 @@ errors are reported with an error message." ((eq (process-status process) 'exit) (setq exit-status (process-exit-status process))) (t (setq exit-status "abnormal termination"))) - (setq coq-current-background-jobs - (max 0 (1- coq-current-background-jobs))) + (setq coq--current-background-jobs + (max 0 (1- coq--current-background-jobs))) (funcall (process-get process 'coq-process-continuation) process exit-status) (coq-par-start-jobs-until-full) - (when (and coq-compile-vio2vo-in-progress - (eq coq-current-background-jobs 0)) - (setq coq-compile-vio2vo-in-progress nil) + (when (and coq--compile-vio2vo-in-progress + (eq coq--current-background-jobs 0)) + (setq coq--compile-vio2vo-in-progress nil) (message "vio2vo compilation finished")) (when (and - (eq coq-current-background-jobs 0) - coq-last-compilation-job) + (eq coq--current-background-jobs 0) + coq--last-compilation-job) (let ((cycle (coq-par-find-dependency-circle))) (if cycle (signal 'coq-compile-error-circular-dep @@ -881,11 +881,11 @@ errors are reported with an error message." (defun coq-par-run-vio2vo-queue () "Start delayed vio2vo compilation." - (assert (not coq-last-compilation-job) + (assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 3") - (setq coq-compile-vio2vo-in-progress t) - (setq coq-compile-vio2vo-delay-timer nil) - (when coq-debug-auto-compilation + (setq coq--compile-vio2vo-in-progress t) + (setq coq--compile-vio2vo-delay-timer nil) + (when coq--debug-auto-compilation (message "Start vio2vo processing for %d jobs" (+ (length (car coq-par-vio2vo-queue)) (length (cdr coq-par-vio2vo-queue))))) @@ -896,9 +896,9 @@ errors are reported with an error message." This callback is inserted with a dummy item after the last require command to start vio2vo compilation after `coq-compile-vio2vo-delay' seconds." - (assert (not coq-last-compilation-job) + (assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 1") - (setq coq-compile-vio2vo-delay-timer + (setq coq--compile-vio2vo-delay-timer (run-at-time coq-compile-vio2vo-delay nil 'coq-par-run-vio2vo-queue))) @@ -922,7 +922,7 @@ require command to start vio2vo compilation after (put dependant 'coqc-dependency-count (1+ (get dependant 'coqc-dependency-count))) (push dependant (get dependee 'coqc-dependants)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s -> %s: add coqc dependency" (get dependee 'name) (get dependant 'name)))) @@ -933,7 +933,7 @@ require command to start vio2vo compilation after nil "queue dependency cannot be added") (put dependant 'queue-dependant-waiting t) (put dependee 'queue-dependant dependant) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s -> %s: add queue dependency" (get dependee 'name) (get dependant 'name)))) @@ -961,7 +961,7 @@ therefore delete a file if it might be in the way. Sets the (src-time (nth 5 (file-attributes (get job 'src-file)))) file-to-delete max-obj-time vio-is-newer other-file other-obj-time result) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message (concat "%s: compare mod times: vo mod %s, vio mod %s, src mod %s, " "youngest dep %s; vo < src : %s, vio < src : %s, " @@ -1012,7 +1012,7 @@ therefore delete a file if it might be in the way. Sets the (put job 'required-obj-file vo-file) (when vio-obj-time (setq file-to-delete vio-file))) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message (concat "%s: definitely need to compile to %s; delete %s") (get job 'name) @@ -1038,7 +1038,7 @@ therefore delete a file if it might be in the way. Sets the (time-less-or-equal vio-obj-time src-time) (time-less-or-equal vio-obj-time dep-time))) (setq file-to-delete vio-file)) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: vo up-to-date 1; delete %s" (get job 'name) (if file-to-delete file-to-delete "noting")))) @@ -1049,7 +1049,7 @@ therefore delete a file if it might be in the way. Sets the (or (time-less-or-equal vio-obj-time src-time) (time-less-or-equal vio-obj-time dep-time))) (setq file-to-delete vio-file)) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: need to compile to vo; delete %s" (get job 'name) (if file-to-delete file-to-delete "noting"))))) @@ -1073,7 +1073,7 @@ therefore delete a file if it might be in the way. Sets the (progn (put job 'required-obj-file other-file) (put job 'obj-mod-time other-obj-time) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message (concat "%s: .vio and .vo up-to-date, " "continue with the older %s") (get job 'name) @@ -1088,13 +1088,13 @@ therefore delete a file if it might be in the way. Sets the (put job 'obj-mod-time vio-obj-time) (when (eq coq-compile-quick 'quick-and-vio2vo) (put job 'vio2vo-needed t)) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: vio up-to-date; delete %s" (get job 'name) (if file-to-delete file-to-delete "noting")))) (put job 'required-obj-file vo-file) (put job 'obj-mod-time vo-obj-time) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: vo up-to-date 2; delete %s" (get job 'name) (if file-to-delete file-to-delete "noting"))))))) @@ -1111,37 +1111,37 @@ This transition is only possible if JOB is in state 'waiting-queue and if it has no queue dependee. If this is the case, the following actions are taken: - for top-level jobs (non-nil 'require-span property), ancestors - are registered in `coq-par-ancestor-files' and in the span in + are registered in `coq--par-ancestor-files' and in the span in 'queue-span - processing of items in 'queueitems is started - a possible queue dependant gets it's dependency cleared, and, if possible the 'waiting-queue -> 'ready transition is (recursively) done for the dependant - if this job is the last top-level compilation - job (`coq-last-compilation-job') then the last compilation job + job (`coq--last-compilation-job') then the last compilation job and `proof-second-action-list-active' are cleared." (if (or (not (eq (get job 'state) 'waiting-queue)) (get job 'queue-dependant-waiting)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (if (not (eq (get job 'state) 'waiting-queue)) (message "%s: no queue kickoff because in state %s" (get job 'name) (get job 'state)) (message "%s: no queue kickoff because waiting for queue dependency" (get job 'name)))) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: has itself no queue dependency" (get job 'name))) (when (and (get job 'require-span) coq-lock-ancestors) (let ((span (get job 'require-span))) (dolist (f (get job 'ancestor-files)) - (unless (eq (gethash f coq-par-ancestor-files) 'asserted) - (puthash f 'asserted coq-par-ancestor-files) + (unless (eq (gethash f coq--par-ancestor-files) 'asserted) + (puthash f 'asserted coq--par-ancestor-files) (span-set-property span 'coq-locked-ancestors (cons f (span-property span 'coq-locked-ancestors))))))) (when (get job 'queueitems) (let ((items (get job 'queueitems))) - (when (and (eq coq-last-compilation-job job) + (when (and (eq coq--last-compilation-job job) (eq coq-compile-quick 'quick-and-vio2vo)) ;; Insert the vio2vo start notification callback after the ;; require item. @@ -1157,34 +1157,34 @@ case, the following actions are taken: (list nil nil 'coq-par-require-processed) (cdr items))))) (proof-add-to-queue items 'advancing) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: add %s items to action list" (get job 'name) (length items))) (put job 'queueitems nil))) (put job 'state 'ready) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: ready" (get job 'name))) (let ((dependant (get job 'queue-dependant))) (if dependant (progn - (assert (not (eq coq-last-compilation-job job)) - nil "coq-last-compilation-job invariant error") + (assert (not (eq coq--last-compilation-job job)) + nil "coq--last-compilation-job invariant error") (put dependant 'queue-dependant-waiting nil) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s -> %s: clear queue dependency, kickoff queue at %s" (get job 'name) (get dependant 'name) (get dependant 'name))) (coq-par-kickoff-queue-maybe dependant) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: queue kickoff finished" (get job 'name)))) - (when (eq coq-last-compilation-job job) - (setq coq-last-compilation-job nil) + (when (eq coq--last-compilation-job job) + (setq coq--last-compilation-job nil) (setq proof-second-action-list-active nil) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "clear last compilation job")) (message "Library compilation finished")) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: no queue dependant, queue kickoff finished" (get job 'name))))))) @@ -1204,7 +1204,7 @@ possible, also 'waiting-queue -> 'ready." ;; It also puts job into the vio2vo queue, if necessary. (if (coq-par-job-needs-compilation job) (coq-par-start-or-enqueue job) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: up-to-date, no compilation" (get job 'name))) (when (get job 'vio2vo-needed) (coq-par-vio2vo-enqueue job)) @@ -1235,7 +1235,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for (1- (get dependant 'coqc-dependency-count))) (assert (<= 0 (get dependant 'coqc-dependency-count)) nil "dependency count below zero") - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: coqc dependency count down to %d" (get dependant 'name) (get dependant 'coqc-dependency-count))) (when (coq-par-dependencies-ready dependant) @@ -1279,7 +1279,7 @@ This function makes the following actions. (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone)) (setq dep-time (get job 'obj-mod-time))) (put job 'youngest-coqc-dependency dep-time) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: kickoff %d coqc dependencies with time %s" (get job 'name) (length (get job 'coqc-dependants)) (if (eq dep-time 'just-compiled) @@ -1290,7 +1290,7 @@ This function makes the following actions. (lambda (dependant) (coq-par-decrease-coqc-dependency dependant dep-time ancestor-files)) (get job 'coqc-dependants)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: coqc kickoff finished, maybe kickoff queue" (get job 'name))) (coq-par-kickoff-queue-maybe job))) @@ -1299,13 +1299,13 @@ This function makes the following actions. "Start coqdep for JOB. Besides starting the background process, the source file is locked, registered in the 'ancestor-files property of JOB and in -`coq-par-ancestor-files'" +`coq--par-ancestor-files'" (let ((true-src (file-truename (get job 'src-file)))) (when coq-lock-ancestors (proof-register-possibly-new-processed-file true-src) (put job 'ancestor-files (list true-src)) - (unless (gethash true-src coq-par-ancestor-files) - (puthash true-src 'locked coq-par-ancestor-files))) + (unless (gethash true-src coq--par-ancestor-files) + (puthash true-src 'locked coq--par-ancestor-files))) (coq-par-start-process coq-dependency-analyzer (coq-par-coqdep-arguments (get job 'src-file) (get job 'load-path)) @@ -1319,7 +1319,7 @@ locked, registered in the 'ancestor-files property of JOB and in (module (coq-module-of-src-file (get job 'src-file))) (default-directory (file-name-directory (file-truename (get job 'src-file))))) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: start vio2vo for %s" (get job 'name) (get job 'src-file))) @@ -1359,12 +1359,12 @@ coqdep or coqc are started for it." (defun coq-par-start-jobs-until-full () "Start background jobs until the limit is reached." - (let ((max-jobs (if coq-compile-vio2vo-in-progress + (let ((max-jobs (if coq--compile-vio2vo-in-progress coq--internal-max-vio2vo-jobs coq--internal-max-jobs)) next-job) - (while (and (< coq-current-background-jobs max-jobs) - (setq next-job (if coq-compile-vio2vo-in-progress + (while (and (< coq--current-background-jobs max-jobs) + (setq next-job (if coq--compile-vio2vo-in-progress (coq-par-vio2vo-dequeue) (coq-par-job-dequeue)))) (coq-par-start-task next-job)))) @@ -1374,7 +1374,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--internal-max-jobs) + (if (< (1+ coq--current-background-jobs) coq--internal-max-jobs) (coq-par-start-task new-job) (coq-par-job-enqueue new-job))) @@ -1407,10 +1407,10 @@ there is space, coqdep is started immediately, otherwise the new job is put into the compilation queue. This function returns the newly created job." - (let* ((orig-job (gethash module-vo-file coq-compilation-object-hash)) + (let* ((orig-job (gethash module-vo-file coq--compilation-object-hash)) (new-job (make-symbol "coq-compile-job-symbol"))) - (put new-job 'name (format "job-%d" coq-par-next-id)) - (setq coq-par-next-id (1+ coq-par-next-id)) + (put new-job 'name (format "job-%d" coq--par-next-id)) + (setq coq--par-next-id (1+ coq--par-next-id)) (put new-job 'vo-file module-vo-file) (put new-job 'coqc-dependency-count 0) (put new-job 'require-span require-span) @@ -1419,7 +1419,7 @@ This function returns the newly created job." ;; there is already a compilation job for module-vo-file (progn (put new-job 'type 'clone) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: create %s compilation job for %s" (get new-job 'name) (get new-job 'type) module-vo-file)) (when queue-dep @@ -1446,8 +1446,8 @@ This function returns the newly created job." (message "Check %s" (get new-job 'src-file)) (put new-job 'load-path coq-load-path) (put new-job 'youngest-coqc-dependency '(0 0)) - (puthash module-vo-file new-job coq-compilation-object-hash) - (if coq-debug-auto-compilation + (puthash module-vo-file new-job coq--compilation-object-hash) + (if coq--debug-auto-compilation (message "%s: create %s compilation for %s" (get new-job 'name) (get new-job 'type) module-vo-file)) (when queue-dep @@ -1485,7 +1485,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (signal 'coq-compile-error-coqdep (get job 'src-file)) ;; no coqdep error -- work on dependencies - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: dependencies of %s are %s" (get job 'name) (get job 'src-file) dependencies-or-error)) (put job 'state 'waiting-dep) @@ -1506,10 +1506,10 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (put job 'youngest-coqc-dependency job-max-time) (if (coq-par-dependencies-ready job) (progn - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: coqc dependencies finished" (get job 'name))) (coq-par-compile-job-maybe job)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: wait for %d dependencies" (get job 'name) (get job 'coqc-dependency-count))))))) @@ -1537,9 +1537,9 @@ PROCESS." (let ((job (process-get process 'coq-compilation-job))) (if (eq exit-status 0) ;; success - nothing to do - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: vio2vo finished successfully" (get job 'name))) - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%s: vio2vo failed" (get job 'name))) (coq-compile-display-error (concat @@ -1560,12 +1560,12 @@ PROCESS." This function translates MODULE-ID to a file name. If compilation for this file is not ignored, a new top-level compilation job is created. If there is a new top-level compilation job, it is saved -in `coq-last-compilation-job'. +in `coq--last-compilation-job'. This function must be evaluated with the buffer that triggered the compilation as current, otherwise a wrong `coq-load-path' might be used." - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (if from (message "handle required module \"%s\" from \"%s\"" module-id from) (message "handle required module \"%s\" without from clause" @@ -1573,7 +1573,7 @@ might be used." (let ((module-vo-file (coq-par-map-module-id-to-vo-file module-id coq-load-path from)) module-job) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (if module-vo-file (message "check compilation for module %s from object file %s" module-id module-vo-file) @@ -1584,12 +1584,12 @@ might be used." (not (coq-compile-ignore-file module-vo-file))) (setq module-job (coq-par-create-library-job module-vo-file coq-load-path - coq-last-compilation-job span + coq--last-compilation-job span "scripting buffer")) - (setq coq-last-compilation-job module-job) - (if coq-debug-auto-compilation + (setq coq--last-compilation-job module-job) + (if coq--debug-auto-compilation (message "%s: this job is the last compilation job now" - (get coq-last-compilation-job 'name)))))) + (get coq--last-compilation-job 'name)))))) (defun coq-par-handle-require-list (require-items) "Start compilation for the required modules in the car of REQUIRE-ITEMS. @@ -1603,14 +1603,14 @@ to file names and creates one top-level compilation job for each required module that is not ignored (eg via `coq-compile-ignored-directories'). Jobs are started immediately if possible. The last such created job is remembered in -`coq-last-compilation-job'. The REQUIRE-ITEMS are attached to +`coq--last-compilation-job'. The REQUIRE-ITEMS are attached to this last top-level job or directly to proof-action-list, if there is no last compilation job." (let* ((item (car require-items)) (string (mapconcat 'identity (nth 1 item) " ")) (span (car item)) prefix start) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "handle require command \"%s\"" string)) ;; We know there is a require in string. But we have to match it ;; again in order to get the end position. @@ -1626,22 +1626,22 @@ there is no last compilation job." (setq start (match-end 0)) (coq-par-handle-module (match-string 1 string) span prefix)) ;; add the asserted items to the last compilation job - (if coq-last-compilation-job + (if coq--last-compilation-job (progn - (assert (not (coq-par-job-is-ready coq-last-compilation-job)) + (assert (not (coq-par-job-is-ready coq--last-compilation-job)) nil "last compilation job from previous compilation ready") - (put coq-last-compilation-job 'queueitems - (nconc (get coq-last-compilation-job 'queueitems) + (put coq--last-compilation-job 'queueitems + (nconc (get coq--last-compilation-job 'queueitems) require-items)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "%s: attach %s items (containing now %s items)" - (get coq-last-compilation-job 'name) + (get coq--last-compilation-job 'name) (length require-items) - (length (get coq-last-compilation-job 'queueitems))))) + (length (get coq--last-compilation-job 'queueitems))))) ;; or add them directly to queueitems if there is no compilation job ;; (this happens if the modules are ignored for compilation) (setq queueitems (nconc queueitems require-items)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "attach %s items to queueitems (containing now %s items)" (length require-items) (length queueitems)))))) @@ -1666,7 +1666,7 @@ If `coq-compile-before-require' is non-nil, this function starts the compilation (if necessary) of the dependencies ansynchronously in parallel in the background. -If there is a last compilation job (`coq-last-compilation-job') +If there is a last compilation job (`coq--last-compilation-job') then the queue region is extended, while some background compilation is still running. In this case I have to preserve the internal state. Otherwise the hash of the compilation jobs and @@ -1684,51 +1684,51 @@ first of these batches, buffers are saved with Finally, `proof-second-action-list-active' is set if I keep some queue items because they have to wait for a compilation job. Then the maximal number of background compilation jobs is started." - (when coq-debug-auto-compilation + (when coq--debug-auto-compilation (message "%d items were added to the queue, scan for require" (length queueitems))) - (unless coq-last-compilation-job + (unless coq--last-compilation-job (coq-par-init-compilation-hash) (coq-par-init-ancestor-hash) (coq-init-compile-response-buffer)) (let ((splitted-items (split-list-at-predicate queueitems 'coq-par-item-require-predicate))) - (if coq-last-compilation-job + (if coq--last-compilation-job (progn - (put coq-last-compilation-job 'queueitems - (nconc (get coq-last-compilation-job 'queueitems) + (put coq--last-compilation-job 'queueitems + (nconc (get coq--last-compilation-job 'queueitems) (car splitted-items))) (setq queueitems nil) (message "attach first %s items to job %s" (length (car splitted-items)) - (get coq-last-compilation-job 'name))) + (get coq--last-compilation-job 'name))) (setq queueitems (car splitted-items)) - (if coq-debug-auto-compilation + (if coq--debug-auto-compilation (message "attach first %s items directly to queue" (length (car splitted-items))))) ;; XXX handle external compilation here, compile everything ;; with one command, use compilation-finish-functions to get ;; notification (when (cdr splitted-items) - (when coq-compile-vio2vo-delay-timer - (cancel-timer coq-compile-vio2vo-delay-timer)) - (when coq-compile-vio2vo-in-progress - (assert (not coq-last-compilation-job) + (when coq--compile-vio2vo-delay-timer + (cancel-timer coq--compile-vio2vo-delay-timer)) + (when coq--compile-vio2vo-in-progress + (assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 2") ;; there are only vio2vo background processes (coq-par-kill-all-processes) - (setq coq-compile-vio2vo-in-progress nil)) + (setq coq--compile-vio2vo-in-progress nil)) ;; save buffers before invoking the first coqdep (coq-compile-save-some-buffers) (mapc (lambda (require-items) (coq-par-handle-require-list require-items)) (cdr splitted-items))) - (when coq-last-compilation-job + (when coq--last-compilation-job (setq proof-second-action-list-active t)) (coq-par-start-jobs-until-full) - (if coq-debug-auto-compilation - (if coq-last-compilation-job + (if coq--debug-auto-compilation + (if coq--last-compilation-job (message "return control, waiting for background jobs") (message "return control, no background jobs"))))) -- cgit v1.2.3