From ef1887364870cd72724c97a7dd9d65f04475294f Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Sat, 31 Oct 2020 13:10:28 +0100 Subject: [PATCH] redesign of parallel background compilation without clones - no clones any more, existing jobs are directly linked - the whole require command is processed by coqdep to determine the required files, this fixes #352 - the require commands are a separate kind of jobs, because they do not need to get compiled - queue items are only stored in require jobs and file jobs can not have a queue dependency, this simplifies the logic --- coq/coq-compile-common.el | 1 + coq/coq-par-compile.el | 1245 +++++++++++++++++++------------------ 2 files changed, 647 insertions(+), 599 deletions(-) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 938f706e6..ed927409e 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -626,6 +626,7 @@ Changes the suffix from .vo to .vok. VO-OBJ-FILE must have a .vo suffix." ;;; manage coq--compile-response-buffer +;; XXX apparently nobody calls this with display equal to nil (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 diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 0a2bc11a6..92b58ec04 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -29,6 +29,14 @@ ;; Note that all argument computations inherit `coq-autodetected-version': when ;; changing compilers, all compilation jobs must be terminated. This is ;; consistent with the fact that the _CoqProject file is not reparsed. +;; +;; tests wanted: +;; - a require command with no dependencies or all deps ignored +;; - unlock checks for ancestors of failed jobs in different cases +;; - two require jobs, where the first finishes, while the second is +;; in a state before waiting-dep +;; - a coqdep error on a require command +;; - some dependency cycles ;;; Code: @@ -57,16 +65,30 @@ ;; are established when the coqdep output is processed. A job with ;; dependencies waits for the dependencies to finish before it ;; continues with coqc. -;; +;; +;; There are two differend kinds of compilation jobs. First, ordinary +;; files, whose dependencies must be determined with coqdep and which +;; might need to be compiled after all their dependencies are ready. +;; These compilation jobs are called 'file jobs here. Apart from 'file +;; jobs there are the Require commands in the asserted region. For +;; each Require command one must determine the modules/files (its +;; dependencies) that must be compiled before the Require command can +;; be processed. Require commands are tracked with 'require jobs here. +;; Typically, a 'require job has a number of 'file jobs as +;; dependencies. coqdep must be run on both, 'require and 'file jobs +;; to determine their dependencies. For 'require jobs this is done in +;; a temporary file. coqc must only be run on 'file jobs. +;; ;; It is pretty clear how to process these compilation jobs. The ;; problems are: ;; -;; 1- where to put the Require command and the items that follow it +;; 1- where to put the Require command itself and the items that follow it ;; 2- make sure ancestors are properly locked ;; 3- error reporting ;; 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11 ;; 5- using -vos for Coq >= 8.11 ;; +;; ;; For 1- where to put the Require command and the items that follow it: ;; ;; The Require command and the items that follow cannot stay in @@ -74,52 +96,38 @@ ;; long before the compilation finishes. I therefore cut ;; proof-action-list into pieces and leave only the items before the ;; first Require on proof-action-list. The others are put into the -;; 'queueitems property of the top level compilation job. When this -;; job finishes, it puts the items back into proof-action-list and -;; lets Proof General process them as usual. +;; 'queueitems property of the 'require command that is created for +;; the Require. When such a 'require job gets ready, it puts the items +;; back into proof-action-list and lets Proof General process them as +;; usual. ;; -;; When one Require command lists several modules or if there are -;; several Require commands, every required module gets its own -;; top-level compilation job and the queue items are stored with the -;; last module from each Require command. All these top-level -;; compilation jobs have so-called queue-depencency links between -;; them. These links ensure that a top-level module puts its items -;; back into proof-action-list only if all top-level jobs of those -;; modules that are required before it are finished. +;; All 'require commands are linked with so-called 'queue-dependent +;; links, such that later 'require jobs can be delayed until earlier +;; ones are ready. The later 'require job is said to be a queue +;; dependant of the earlier one. ;; -;; A problem occurs with "Require a. Require a.", where two different -;; action list pieces must be stored with the job for a. The solution -;; here is to clone the original job when it is needed more than one -;; time. This cloning is done in general and not only for top-level -;; jobs. So also when a.v and b.v both depend on c.v, the second -;; dependency link is managed by a clone of the job for c.v. Every -;; real job has dependency links to all its clones. All clones wait -;; until the original job has finished. (In retrospect it seems a -;; design without clone jobs might have been cleaner.) ;; ;; For 2- make sure ancestors are properly locked: ;; -;; The problem is "Require b. Require a.", where b depends on a. Here, -;; file a.v will be locked when the dependency b -> a is not known yet -;; to Proof General. Nevertheless, a.v must be associated with the -;; first Require command. Otherwise, a.v would be wrongly unlocked, -;; when only "Require a." is retracted. +;; Consider "Require a. Require b." where a and b depend on c. Locking +;; must be done such that c is only unlocked, when "Require a" is +;; undone and not when "Require b" is undone alone. During compilation +;; files are locked just before coqdep is started on them (after they +;; have been identified as a dependency). At that time the 'lock-state +;; property of the job is set to 'locked. Ancestors are then +;; propagated upwards in the dependency tree and stored in the +;; 'ancestors property of jobs. When a require job is retired all +;; direct and indirect ancestors with 'lock-state 'locked are stored +;; in the 'coq-locked-ancestors property of the span belonging to that +;; require command (in the 'require-span property). The 'lock-state is +;; then set to 'asserted, such that any other require job will ignore +;; these jobs. A span delete action will unlock all uncestors in the +;; 'coq-locked-ancestors property. ;; -;; The problem is solved with the 'coq-locked-ancestors property of -;; spans that contain Require commands. 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. +;; The 'ancestors property holds a hash that is used as a set, to +;; avoid exponential duplication of ancestors, see Proof General +;; issue 499. ;; -;; Ancestors accumulate in compilation jobs when the compilation walks -;; upwards the dependency tree. In the end, every top-level job -;; contains the set of all its direct and indirect ancestors in the -;; hash in its 'ancestors property. Because of eager locking, all its -;; ancestors are already locked, when a top-level job is about to be -;; retired. Every job records in his 'lock-state propery whether the -;; file corresponding to this job has been registered in some -;; 'coq-locked-ancestors property already. ;; ;; For 3- error reporting: ;; @@ -129,21 +137,33 @@ ;; `coq-par-emergency-cleanup', which kills all compilation jobs, ;; retracts the queue region and resets all internal data. ;; -;; For `coq-compile-keep-going', the failing job and all dependants -;; are marked as 'failed. Queue dependants are marked with -;; 'queue-failed. These marked jobs continue with their normal state -;; transition, but omit certain steps (eg., running coqc). The first -;; tricky part is how to unlock ancestors. When marking jobs as -;; failed, their ancestors (and thereby also the files for the jobs -;; themselves) are unlocked, unless they are still participating in an -;; ongoing compilation. If a coqc compilation finishes and all -;; dependants are marked as failed, ancestors are also unlocked in the -;; same way. If a top-level job is marked as 'queue-failed, its -;; ancestors are unlocked when this job finishes coqc compilation. +;; For `coq-compile-keep-going', the failing job, all ordinary +;; dependants and all queue dependants are marked with 'failed. All +;; ancestors that have already been registered in such a failed job +;; are treated in the following way: If the ancestor is (via a +;; different dependency path) an ancestor of a job that is still being +;; compiled, then the ancestor is kept locked. Otherwise the ancestor +;; is unlocked. Failed jobs continue with their normal state +;; transition, but omit certain steps (eg., running coqc). If a coqc +;; compilation finishes and all dependants are marked as failed, the +;; ancestors are also treated in the way described before. If a failed +;; require job is retired, nothing is done (especially its span is not +;; asserted), unless it is the last compilation job. If the last +;; compilation job is marked as failed when it is retired, then the +;; whole queue region is retracted. +;; +;; When a failing require command follows a bunch of commands that +;; take a while to process, it may happen, that the last failing +;; require command is ready to be retired before the preceeding +;; commands have been processed. In this case the retirement (in +;; particular, unlocking the queue region) must be delayed until proof +;; action list is empty. This is done by adding an empty action into +;; `proof-action-list' that calls the retirement function +;; `coq-par-kickoff-queue-maybe' again. Further +;; `coq--par-delayed-last-job' must be set to disable the cycle +;; detection that is otherwise automatically started if no background +;; job is active and the last require job has not been retired yet. ;; -;; The second tricky part is how to delete the queue region. For that -;; the last top-level job is delayed until proof-action-list is empty. -;; Then the whole queue is deleted. ;; ;; For 4- using -quick and the handling of .vo/.vio prerequisites for Coq < 8.11 ;; @@ -170,6 +190,7 @@ ;; .vo file and if already present .vo or .vio files must be deleted. ;; Only at that point the relevant property 'required-obj-file is set. ;; +;; ;; For 5- using -vos for Coq >= 8.11 ;; ;; When Coq >= 8.11 is detected, -vos is used and coq-compile-vos is @@ -195,95 +216,74 @@ ;; ;; 'name - some unique string, only used for debugging ;; 'queueitems - holds items from proof-action-list on -;; top-level jobs +;; require jobs ;; 'vo-file - the .vo file for the module that this job has ;; to make up-to-date. This slot is filled when the ;; job is created and independent of whether a .vio -;; or .vo file must be made up-to-date. +;; or .vo file must be made up-to-date. Only present +;; in file jobs. ;; 'required-obj-file - contains the .vio or .vo to be produced or nil -;; if that has not yet been decided. Does also contain -;; nil if no file needs to be rebuild at all. +;; if that has not yet been decided. May contain +;; nil if no file needs to be rebuild at all. Nil +;; on require jobs. ;; 'obj-mod-time - modification time of 'required-obj-file, stored -;; here, to avoid double stat calls; -;; contains 'obj-does-not-exist in case that file is absent +;; here in case compilation is not needed for file +;; jobs, to avoid double stat calls; ;; 'use-quick - 'vio if `coq-par-job-needs-compilation' decided to use ;; -quick for Coq older than 8.11; 'vos if it decided to ;; to use -vos for Coq 8.11 or newer, nil if it decided -;; to use .vo compilation or no compilation is necessary. -;; 'type - the type of the job, either 'clone or 'file -;; for real compilation jobs +;; to use .vo compilation, no compilation is necessary or +;; for require jobs. +;; 'type - the type of the job, either 'require or 'file ;; 'state - the state of the job, see below -;; 'coqc-dependants - list of parent jobs that depend on this job +;; 'coqc-dependants - list of parent jobs that depend on this job, ;; when this job finishes it propagates the ;; necessary information to it's parent jobs and ;; decreases their 'coqc-dependency-count ;; 'coqc-dependency-count - number of unfinished child jobs ;; increased for every subjob spawned ;; during coqdep output processing -;; This job waits with coqc until this -;; count reaches 0 again +;; File job waits with coqc until this +;; count reaches 0 again. Require jobs wait with +;; their transition to 'ready. ;; 'youngest-coqc-dependency - slot to accumulate the most recent ;; modification time of some ancestor -;; value might be an Emacs time or -;; 'just-compiled -;; 'queue-dependant - next top-level job, only present in top-level jobs -;; 'queue-dependant-waiting - t if this is a top-level job that has -;; to wait until previous top-level jobs -;; finish. In this waiting time, modules +;; value; might be an Emacs time or +;; 'just-compiled; not really needed in require +;; jobs but present there to simplify the code +;; 'queue-dependant - next top-level job, only present in require jobs +;; 'queue-dependant-waiting - t if this is a require job that has +;; to wait until previous require jobs +;; finish. In this waiting time, dependencies ;; are compiled, but queue items are only ;; put back into proof-action-list when ;; this property becomes nil -;; 'src-file - the .v file name +;; 'src-file - the .v file name, only in file jobs ;; 'load-path - value of coq-load-path, propagated to all ;; dependencies ;; 'ancestors - set of ancestor jobs, implemented as hash -;; mapping jobs to t; for real compilation jobs +;; mapping jobs to t; for file jobs ;; this set includes the job itself; the hash is ;; necessary to avoid an exponentially growing ;; number of duplicates -;; 'lock-state - nil for clone jobs, 'unlocked if the file +;; 'lock-state - nil for require jobs, 'unlocked if the file ;; corresponding to job is not locked, 'locked if that ;; file has been locked, 'asserted if it has been ;; registered in some span in the 'coq-locked-ancestors ;; property already -;; 'require-span - present precisely for top-level jobs only, there it -;; contains the span that must finally store the -;; ancestors +;; 'require-span - holds the span with the require command for require jobs ;; 'vio2vo-needed - t if a subsequent vio2vo process is required to ;; build the .vo file. Otherwiese nil. ;; 'failed - t if coqdep or coqc for the job or one dependee failed. -;; 'queue-failed - t if some direct or indirect queue dependee is -;; marked 'failed ;; 'visited - used in the dependency cycle detection to mark ;; visited jobs -;; -;; -;; State transition of real compilation jobs -;; -;; 'enqueued-coqdep -> 'waiting-dep -> 'enqueued-coqc -;; -> 'waiting-queue -> 'ready -;; -;; 'enqueued-coqdep - coqdep is running or the job enqueued, waiting -;; for a slot to start coqdep -;; 'waiting-dep - the job is waiting for all Coq dependencies to -;; finish -;; 'enqueued-coqc - coqc is running, or the job is enqueued, -;; waiting for a slot to start coqc -;; 'waiting-queue - coqc is finished and the job is waiting until -;; all top-level queue dependencies finish (if -;; there are any) -;; 'ready - ready, the .vo file might be missing though -;; -;; -;; State transition for clone jobs -;; -;; 'waiting-dep -> 'waiting-queue -> 'ready -;; -;; 'waiting-dep - the clone is waiting until the real job finishes -;; 'waiting-queue - the job is waiting until all top-level queue -;; dependencies finish -;; 'ready - ready -;; +;; 'current-dir - current directory or default-directory of the buffer +;; that contained the require command. Only present in +;; require jobs. Only needed for 8.4 compatibility. +;; 'temp-require-file - temporary file name just containing the require +;; command of a require job for determining the files +;; needed for that require. Must be deleted after +;; coqdep finished. ;; ;; ;; Properties of processes @@ -297,38 +297,69 @@ ;; 'coq-process-continuation - the continuation to be called when ;; the process finishes. Either ;; coq-par-process-coqdep-result or -;; coq-par-coqc-continuation +;; coq-par-coqc-continuation or +;; coq-par-vio2vo-continuation ;; 'coq-process-output - the output of the process ;; 'coq-process-command - the command for error reporting ;; (as string list) -;; 'coq-par-process-killed - t if this process has been killed +;; 'coq-par-process-killed - t if this process has been killed from PG ;; 'coq-process-rm - if not nil, a file to be deleted when -;; the process is killed +;; the process does not finish successfully, +;; i.e., when the continuation is not called. +;; +;; +;; State transition of file jobs +;; +;; 'enqueued-coqdep -> 'waiting-dep -> 'enqueued-coqc -> 'ready +;; +;; State transition for require jobs +;; +;; 'enqueued-coqdep -> 'waiting-dep -> 'waiting-queue -> 'ready +;; +;; State explanation +;; +;; 'enqueued-coqdep - coqdep is running or the job enqueued, waiting +;; for a slot to start coqdep +;; 'waiting-dep - coqdep finished, dependencies determined, waiting for +;; the dependencies +;; 'enqueued-coqc - dependencies ready, coqc is running, or the job is +;; enqueued, waiting for a slot to start coqc +;; 'waiting-queue - XXX +;; 'ready - ready, the result might be missing when 'failed ;; ;; ;; Over its live time, a compilation job might get passed through the ;; following functions. Some of them might be skipped or executed more ;; then once. ;; -;; | function | state | comment | +;; | functions for file jobs | state | comment | ;; |----------------------------------+------------------+--------------------------------------| -;; | coq-par-create-library-job | 'enqueued-coqdep | job creation | -;; | coq-par-start-coqdep | | | +;; | coq-par-create-file-job | 'enqueued-coqdep | job creation | +;; | coq-par-start-coqdep-on-file | | lock files | ;; | coq-par-process-coqdep-result | 'waiting-dep | create dependee/child jobs | ;; | coq-par-decrease-coqc-dependency | | dependee/child finished coqc | ;; | coq-par-compile-job-maybe | 'enqueued-coqc | | ;; | -- start coqc | | | ;; | coq-par-coqc-continuation | | | -;; | coq-par-kickoff-coqc-dependants | 'waiting-queue | | -;; | coq-par-kickoff-queue-maybe | ready | | +;; | coq-par-kickoff-coqc-dependants | 'ready | | +;; | coq-par-start-vio2vo | | | +;; | coq-par-vio2vo-continuation | | | +;; +;; +;; | function for require jobs | state | comment | +;; |----------------------------------+------------------+--------------------------------------| +;; | coq-par-create-require-job | 'enqueued-coqdep | job creation | +;; | coq-par-start-coqdep-on-require | | lock files | +;; | coq-par-process-coqdep-result | 'waiting-dep | create dependee/child jobs | +;; | coq-par-decrease-coqc-dependency | | dependee/child finished coqc | +;; | coq-par-kickoff-queue-maybe | 'waiting-queue | | ;; | coq-par-retire-top-level-job | | | +;; | coq-par-kickoff-queue-maybe cont | 'ready | | ;; | coq-par-require-processed | | in dummy action in proof-action-list | ;; | coq-par-run-vio2vo-queue | | called via timer | -;; | coq-par-start-vio2vo | | | -;; | coq-par-vio2vo-continuation | | | ;; ;; -;; The following is maybe outdated. +;; The following _is_ outdated. ;; To print the states of the compilation jobs for debugging, eval ;; ;; (let ((clones)) @@ -364,7 +395,7 @@ (defvar coq--compilation-object-hash nil "Hash for storing the compilation jobs. -This hash only stores real compilation jobs and no clones. They +This hash only stores file jobs and no require jobs. They are stored in order to avoid double compilation. The jobs stored in here are uninterned symbols that carry all important information in their property list. See the documentation in the @@ -372,7 +403,7 @@ 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 - "Pointer to the last top-level compilation job. + "Pointer to the last require compilation job. Used to link top-level jobs with queue dependencies.") (defvar coq--compile-vio2vo-in-progress nil @@ -398,7 +429,14 @@ The names are only used for debugging.") (defvar coq--par-delayed-last-job nil "Inform the cycle detection that there is a delayed top-level job. -If t, there is a delayed top-level job (for which the compilation failed).") +The retirement of failing require jobs must be delayed until +`proof-action-list' is empty, to avoid retracting commands before +the first failing require. This is done by adding the call to +`coq-par-kickoff-queue-maybe' to the end of `proof-action-list'. +This variable is t during this time to disable cycle detection, +which is otherwise started when `coq--last-compilation-job' has +not been retired but no compilation process is running in the +background.") ;;; utility functions @@ -429,9 +467,9 @@ the result." (defun coq-par-time-less (time-1 time-2) "Compare extended times. -The arguments can be an emacs time (a list of 2 or 3 integers, -see `file-attributes') or the symbol 'just-compiled, where the -latter greater then everything else." +The arguments can be an emacs time (a list of 2 to 4 integers, +see `current-time') or the symbol 'just-compiled, where the +latter is greater then everything else." (cond ((eq time-2 'just-compiled) t) ((eq time-1 'just-compiled) nil) @@ -442,7 +480,9 @@ latter greater then everything else." (setq coq--compilation-object-hash (make-hash-table :test 'equal))) (defun merge-hash-content (target source) - "Add all elements of hash SOURCE to hash TARGET." + "Add all elements of hash SOURCE to hash TARGET. +Keys present in TARGET and in SOURCE are replaced in TARGET with +their SOURCE binding." (maphash (lambda (key val) (puthash key val target)) source)) @@ -470,6 +510,7 @@ latter greater then everything else." ;;; job queue +;; XXX local variable -- check all defvars for local variables (defvar coq-par-compilation-queue (coq-par-new-queue) "Queue of compilation jobs that wait for a free core to get started. Use `coq-par-job-enqueue' and `coq-par-job-dequeue' to access the @@ -576,8 +617,36 @@ access the queue.") (defun coq-par-find-dependency-circle-for-job (job path) "Find a dependency cycle in the dependency subtree of JOB. -Do a depth-first-search to find the cycle. JOB is the current -node and PATH the stack of visited nodes." +Do a depth-first-search to find the cycle. JOB is the current +node and PATH the stack of visited nodes. Jobs in state +'enqueue-coqc can be ignored, because they can never participate +in a cycle." + ;; CORRECTNESS ARGUMENT FOR THIS FUNCTION + ;; + ;; An outside-cycle job is a job for which the whole upward segment + ;; of the dependency graph does not contain any cycle (and therefore + ;; neither job itself belongs to any cycle nor is there a path + ;; starting in job and leading to a cycle). Any job is either + ;; outside-cycle or there exists an upward path containing the job + ;; and a cycle above it. + ;; The visited-condition is that all jobs marked visited are + ;; outside-cycle jobs. + ;; + ;; The precondition of this function is that + ;; - PATH does not contain any job twice, + ;; - PATH is an reversed upward path where JOB is a dependant of the + ;; head of PATH, and + ;; - the visited-condition holds. + ;; + ;; This function returns nil and the visited condition holds at + ;; return, if the precondition holds and JOB is outside-cycle. + ;; Proved by induction on the length of the maximal upward path. + ;; + ;; This function returns a cycle (and not nil) if the precondition + ;; holds and JOB is not outside-cycle. Proved by induction on the + ;; distance to the first repeated job on the right-most upward path + ;; containing a cycle. Here, right is the direction of the head of + ;; the 'coqc-dependants list. (let (cycle (p path)) ;; path is reversed. A potential cycle goes from the beginning of ;; path to the first occurence of job. @@ -591,7 +660,11 @@ node and PATH the stack of visited nodes." (setq path (cons job path)) (setq p (get job 'coqc-dependants)) (while (and p (not cycle)) + ;; XXX when clause does not make sense: job is a dependee or + ;; dependency of (car p), therefore (car p) can only be in + ;; state 'waiting-dep (when (eq (get (car p) 'state) 'waiting-dep) + ;; XXX should not be called on visited ancestors? (setq cycle (coq-par-find-dependency-circle-for-job (car p) path))) (setq p (cdr p))) (put job 'visited t) @@ -600,8 +673,9 @@ node and PATH the stack of visited nodes." (defun coq-par-find-dependency-circle () "Find a dependency cycle in compilation jobs of state 'waiting-dep. If no circle is found return nil, otherwise the list of files -belonging to the circle." - (let (cycle result) +belonging to the circle. Jobs in state 'enqueue-coqc can be +ignored, because they can never participate in a cycle." + (let (cycle) (maphash (lambda (key job) (put job 'visited nil)) coq--compilation-object-hash) (maphash @@ -610,10 +684,7 @@ belonging to the circle." (eq (get job 'state) 'waiting-dep)) (setq cycle (coq-par-find-dependency-circle-for-job job nil)))) coq--compilation-object-hash) - (dolist (j cycle) - (when (eq (get j 'type) 'file) - (push (get j 'src-file) result))) - (nreverse result))) + (mapcar (lambda (j) (get j 'src-file)) cycle))) ;;; map coq module names to files, using synchronously running coqdep @@ -623,7 +694,9 @@ belonging to the circle." Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer that triggered the compilation, in order to provide correct load-path options to coqdep." - (nconc (coq-coqdep-prog-args coq-load-path (file-name-directory lib-src-file) (coq--pre-v85)) + (nconc (coq-coqdep-prog-args coq-load-path + (file-name-directory lib-src-file) + (coq--pre-v85)) (list lib-src-file))) (defun coq-par-coqc-arguments (lib-src-file coq-load-path) @@ -642,7 +715,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." +or .vos files must be done elsewhere." ;; (when coq--debug-auto-compilation ;; (message "analyse coqdep output \"%s\"" output)) (if (or @@ -651,7 +724,9 @@ files must be done elsewhere." (progn ;; display the error (coq-compile-display-error (mapconcat 'identity command " ") output t) - "unsatisfied dependencies") + (if (eq status 0) + "unsatisfied dependencies" + (format "coqdep exist status %d" status))) ;; In 8.5, coqdep produces two lines. Match with .* here to ;; extract only a part of the first line. ;; We could match against (concat "^[^:]*" obj-file "[^:]*: \\(.*\\)") @@ -664,118 +739,6 @@ files must be done elsewhere." (lambda (f) (string-match-p "\\.vo\\'" f)) (split-string (match-string 1 output)))))) -(defun coq-par-get-library-dependencies (lib-src-file coq-load-path - &optional command-intro) - "Compute dependencies of LIB-SRC-FILE. -Invoke \"coqdep\" on LIB-SRC-FILE and parse the output to -compute the compiled coq library object files on which -LIB-SRC-FILE depends. The return value is either a string or a -list. If it is a string then an error occurred and the string is -the core of the error message. If the return value is a list no -error occurred and the returned list is the (possibly empty) list -of file names LIB-SRC-FILE depends on. - -Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer -that triggered the compilation, in order to provide correct -load-path options to coqdep. - -If an error occurs this funtion displays -`coq-compile-response-buffer' with the complete command and its -output. The optional argument COMMAND-INTRO is only used in the -error case. It is prepended to the displayed command. - -LIB-SRC-FILE should be an absolute file name. If it is, the -dependencies are absolute too and the simplified treatment of -`coq-load-path-include-current' in `coq-include-options' won't -break. - -This function always computes the .vo file names. Conversion into .vio, -depending on `coq-compile-quick', must be done elsewhere." - (let* ((coqdep-arguments - (coq-par-coqdep-arguments lib-src-file coq-load-path)) - (this-command (cons coq-dependency-analyzer coqdep-arguments)) - (full-command (if command-intro - (cons command-intro this-command) - this-command)) - coqdep-status coqdep-output) - (when coq--debug-auto-compilation - (message "Run synchronously: %s" - (mapconcat 'identity full-command " "))) - ;; (when coq--debug-auto-compilation - ;; (message "CPGLD: call coqdep arg list: %s" coqdep-arguments)) - (with-temp-buffer - (setq coqdep-status - (apply 'call-process - coq-dependency-analyzer nil (current-buffer) nil - coqdep-arguments)) - (setq coqdep-output (buffer-string))) - ;; (when 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))) - -(defun coq-par-map-module-id-to-vo-file (module-id coq-load-path &optional from) - "Map MODULE-ID to the appropriate coq object (.vo) file. -The mapping depends of course on `coq-load-path'. The current -implementation invokes coqdep with a one-line require command. -This is probably slower but much simpler than modelling coq file -loading inside ProofGeneral. Argument SPAN is only used for error -handling. It provides the location information of MODULE-ID for a -decent error message. Argument COQ-LOAD-PATH must be -`coq-load-path' from the buffer that triggered the compilation, -in order to provide correct load-path options to coqdep. - -This function always computes the .vo file name. Conversion into .vio, -depending on `coq-compile-quick', must be done elsewhere. - -A peculiar consequence of the current implementation is that this -function returns () if MODULE-ID comes from the standard library." - (let ((coq-load-path - (if (and coq-load-path-include-current (coq--pre-v85)) - (cons default-directory coq-load-path) - coq-load-path)) - (coq-load-path-include-current nil) - (temp-require-file (make-temp-file "ProofGeneral-coq" nil ".v")) - (coq-string (concat (if from (concat "From " from " ") "") - "Require " module-id ".")) - result) - (unwind-protect - (progn - (with-temp-file temp-require-file - (insert coq-string)) - (setq result - (coq-par-get-library-dependencies - temp-require-file - coq-load-path - (concat "echo \"" coq-string "\" > " temp-require-file ";")))) - (delete-file temp-require-file)) - (when 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 - ;; translate module-id into a file name. We insert now a faked error - ;; message into coq-compile-response-buffer to make next-error happy. - (let ((error-message - (format "Cannot find library %s in loadpath" module-id)) - (inhibit-read-only t)) - ;; Writing a message into coq-compile-response-buffer for next-error - ;; does currently not work. We do have exact position information - ;; about the span, but we don't know how much white space there is - ;; between the start of the span and the start of the command string. - ;; Check that coq-compile-response-buffer is a valid buffer! - ;; (with-current-buffer coq-compile-response-buffer - ;; (insert - ;; (format "File \"%s\", line %d\n%s.\n" - ;; (buffer-file-name (span-buffer span)) - ;; (with-current-buffer (span-buffer span) - ;; (line-number-at-pos (span-start span))) - ;; error-message))) - ;; (coq-seq-display-compile-response-buffer) - (error error-message))) - (cl-assert (<= (length result) 1) - nil "Internal error in coq-seq-map-module-id-to-obj-file") - (car-safe result))) - ;;; manage background jobs @@ -845,7 +808,7 @@ background job that was killed." This is the function that cleans everything up when some background compilation process detected a severe error. When `coq-compile-keep-going' is nil, all errors are severe. When -`coq-compile-keep-going' is t, coqc and some coqdep errors are +`coq-compile-keep-going' is t, coqc and coqdep errors are not severe. This function is also used for the user action to kill all background compilation. @@ -903,11 +866,12 @@ interrupt signal to the prover." This function starts COMMAND with arguments ARGUMENTS for compilation job JOB, making sure that CONTINUATION runs when the process finishes successfully. FILE-RM, if non-nil, denotes a -file to be deleted when the process is killed." - ;; (message "CPSP %s %s %s %s %s" command arguments continuation job file-rm) +file to be deleted when the process does not finish successfully." + ;;(message "CPSP %s %s %s %s %s" command arguments continuation job file-rm) (let ((process-connection-type nil) ; use pipes (process-name (format "pro-%s" coq--par-next-id)) process) + (setq coq--par-next-id (1+ coq--par-next-id)) (with-current-buffer (or proof-script-buffer (current-buffer)) (when coq--debug-auto-compilation (message "%s %s: start %s %s in %s" @@ -923,12 +887,19 @@ file to be deleted when the process is killed." nil ; no process buffer command arguments)) (error + (when coq--debug-auto-compilation + (message "%s %s: error in start process, %s" + (get job 'name) process-name + (if file-rm + (format "rm %s" file-rm) + "no file removal"))) + (when file-rm + (ignore-errors (delete-file file-rm))) (signal 'coq-compile-error-command-start (list (cons command arguments) (nth 2 err))))) (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)) (process-put process 'coq-compilation-job job) (process-put process 'coq-process-continuation continuation) @@ -938,10 +909,17 @@ file to be deleted when the process is killed." (defun coq-par-process-sentinel (process event) "Sentinel for all background processes. -Runs when process PROCESS terminated because of EVENT. It +Runs when process PROCESS terminated because of EVENT. It determines the exit status and calls the continuation function -that has been registered with that process. Normal compilation -errors are reported with an error message." +that has been registered with that process. Normal compilation +errors are reported with an error message inside the callback. +Starts as many queued jobs as possible. If, at the end, no job is +running in the background but compilation has not been finished, +then there must be a cycle in the dependencies, which is found +and reported here. The cycle detection is skipped, if the +retirement of the last compilation job has been delayed per +`coq--par-delayed-last-job'. All signals are caught inside this +function and reported appropriately." (condition-case err (if (process-get process 'coq-par-process-killed) (progn @@ -953,9 +931,9 @@ errors are reported with an error message." (format "rm %s" (process-get process 'coq-process-rm)) "no file removal"))) - (if (process-get process 'coq-process-rm) - (ignore-errors - (delete-file (process-get process 'coq-process-rm)))) + (when (process-get process 'coq-process-rm) + (ignore-errors + (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 @@ -988,9 +966,14 @@ errors are reported with an error message." coq--last-compilation-job) (let ((cycle (coq-par-find-dependency-circle))) (if cycle + ;; XXX cycle may contain a file job -> check code and adapt + ;; cycle printing (signal 'coq-compile-error-circular-dep (mapconcat 'identity cycle " -> ")) (error "Deadlock in parallel compilation")))))) + ;; coq-compile-error-start can be signaled inside the continuation + ;; function, if that tries to start new jobs + ;; XXX catch this error also in coq-par-preprocess-require-commands (coq-compile-error-command-start (coq-par-emergency-cleanup) (message "%s \"%s\" in \"%s\"" @@ -1010,6 +993,8 @@ errors are reported with an error message." (defun coq-par-run-vio2vo-queue () "Start delayed vio2vo compilation." + ;; XXX this assert can be triggered - just start a compilation + ;; shortly before the timer triggers (cl-assert (not coq--last-compilation-job) nil "normal compilation and vio2vo in parallel 3") (setq coq--compile-vio2vo-in-progress t) @@ -1038,6 +1023,11 @@ somewhere after the last require command." 'coq-par-run-vio2vo-queue)))) (defun coq-par-callback-queue-item (callback) + "Create queue item containing just CALLBACK. +Create a queue item for `proof-action-list' containing just +CALLBACK. CALLBACK must be a function taking a span as argument. +The command list in the produced queue item is nil, therefore the +item will be processed as comment and only the callback will be called." ;; A proof-action-list item has the form of ;; (SPAN COMMANDS ACTION [DISPLAYFLAGS]) ;; If COMMANDS is nil, the item is processed as comment and not sent @@ -1048,15 +1038,6 @@ somewhere after the last require command." ;;; background job tasks -(defun coq-par-job-coqc-finished (job) - "Return t if JOB has state 'waiting-queue or 'ready." - (or (eq (get job 'state) 'waiting-queue) - (eq (get job 'state) 'ready))) - -(defun coq-par-job-is-ready (job) - "Return t if compilation job JOB is ready." - (eq (get job 'state) 'ready)) - (defun coq-par-dependencies-ready (job) "Return t if all dependencies of compilation job JOB are ready." (eq (get job 'coqc-dependency-count) 0)) @@ -1071,9 +1052,11 @@ somewhere after the last require command." (get dependee 'name) (get dependant 'name)))) (defun coq-par-add-queue-dependency (dependee dependant) - "Add queue dependency from child job DEPENDEE to parent job DEPENDANT." + "Add queue dependency from require job DEPENDEE to require job DEPENDANT. +The require item of DEPENDANT comes after those of DEPENDEE. +Therefore DEPENDANT must wait for DEPENDEE to finish. " (cl-assert (and (not (get dependant 'queue-dependant-waiting)) - (not (get dependee 'queue-dependant))) + (not (get dependee 'queue-dependant))) nil "queue dependency cannot be added") (put dependant 'queue-dependant-waiting t) (put dependee 'queue-dependant dependant) @@ -1096,7 +1079,7 @@ that are in the way are deleted. Note that the coq documentation does not contain a statement, about what file is loaded, if both a .vo and a .vio file are present. To be on the safe side, I therefore delete a file if it might be in the way. Sets the -'vio2vo property on job if necessary." +'vio2vo-needed property on job if necessary." (let* ((vo-file (get job 'vo-file)) (vio-file (coq-library-vio-of-vo-file vo-file)) (vo-obj-time (nth 5 (file-attributes vo-file))) @@ -1256,10 +1239,11 @@ This function decides whether JOB needs to get compiled for coq latter, `coq-compile-vos' is consulted and, if that is `nil', coq-compile-quick, see `coq-compile-prefer-vos'. This function assumes that coq is used consistently and that a .vo file cannot -be present without a .vos file that has the same time stamp of +be present without a .vos file that has the same time stamp or has been created more recently. As result, this function sets the property 'use-quick to `vos' if JOB should be compiled with -vos. -If no compilation is needed, 'obj-mod-time to the time stamp of +If compilation is needed, 'required-obj-file is set. +If no compilation is needed, 'obj-mod-time is set to the time stamp of the .vos or .vo file, depending on `coq-compile-prefer-vos'." (let* ((vo-file (get job 'vo-file)) (vos-file (coq-library-vos-of-vo-file vo-file)) @@ -1311,12 +1295,14 @@ the .vos or .vo file, depending on `coq-compile-prefer-vos'." (put job 'obj-mod-time vo-obj-time))))) result)) + (defun coq-par-job-needs-compilation (job) "Determine if JOB nees to get compiled and possibly do some side effects. This function calls `coq-par-job-needs-compilation-vos for coq >= 8.11 and `coq-par-job-needs-compilation-quick' otherwise. Returns t if a compilation is required and sets the 'use-quick property -depending on wheter -quick/-vio or -vos should be used. Property +depending on wheter -quick/-vio or -vos should be used. +If compilation is needed, 'required-obj-file is set. Property 'obj-mod-time is set when no compilation is needed." (if (coq--post-v811) (coq-par-job-needs-compilation-vos job) @@ -1324,23 +1310,22 @@ depending on wheter -quick/-vio or -vos should be used. Property (defun coq-par-retire-top-level-job (job) "Register ancestors and start queue items. -This function performs the essential tasks for top-level jobs -when they transition from 'waiting-queue to 'ready: +JOB must be a successful require job. + +This function performs the essential tasks for successful require +jobs when they transition from 'waiting-queue to 'ready: - Registering ancestors in the span and recording this fact in the 'lock-state property. - Moving queue items back to `proof-action-list' and start their execution. - Insert `coq-par-require-processed' as callback if this is the last top-level job, such that vio2vo compilation will start - eventually. - -This function can safely be called for non-top-level jobs. This -function must not be called for failed jobs." - (cl-assert (not (get job 'failed)) + eventually." + (cl-assert (and (not (get job 'failed)) (eq (get job 'type) 'require)) nil "coq-par-retire-top-level-job precondition failed") (let ((span (get job 'require-span)) (items (get job 'queueitems))) - (when (and span coq-lock-ancestors) + (when coq-lock-ancestors (maphash (lambda (anc-job not-used) (cl-assert (not (eq (get anc-job 'lock-state) 'unlocked)) @@ -1350,6 +1335,7 @@ function must not be called for failed jobs." (push (get anc-job 'src-file) (span-property span 'coq-locked-ancestors)))) (get job 'ancestors))) + ;; XXX each require job must have items, right? (when items (when (and (not (coq--post-v811)) (eq coq-compile-quick 'quick-and-vio2vo) @@ -1370,16 +1356,29 @@ function must not be called for failed jobs." (when coq--debug-auto-compilation (message "%s: add %s items to action list" (get job 'name) (length items))) + ;; this function should only be called once for each require job + ;; resetting queueitems is on the save side in any case (put job 'queueitems nil)))) (defun coq-par-kickoff-queue-maybe (job) - "Try transition 'waiting-queue -> 'ready for job JOB. -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 successful top-level jobs (non-nil 'require-span property), ancestors - are registered in the 'queue-span and marked as 'asserted in their - 'lock-state property + "Transition require job JOB to 'waiting-queue and maybe to 'ready. +This function can only be called for require jobs. It further +must not be called if JOB is in state 'enqueued-coqdep or in +state 'waiting-dep with some not yet finished dependencies. This +function is called when all dependencies of JOB are ready to put +JOB into state 'waiting-dep. When in state 'waiting-dep, this +function is also called, when the queue dependency of JOB has +transitioned to 'ready (inside this function). + +First JOB is put into state 'waiting-dep. If there is still a +queue dependency, nothing else happens and JOB waits until the +queue dependee calls this function again when it is ready. + +If there is no queue dependency, then require job JOB must be +retired and transition to 'ready. This means: +- for successful require jobs, ancestors are registered in the + 'queue-span and marked as 'asserted in their 'lock-state + property - processing of items in 'queueitems is started (if JOB is successful) - a possible queue dependant gets it's dependency cleared, and, if possible the 'waiting-queue -> 'ready transition @@ -1394,20 +1393,25 @@ case, the following actions are taken: proof-action-list item. When proof-action-list is empty, the queue span is deleted, remaining spans are cleared and the `proof-shell-busy' lock is freed." - (if (or (not (eq (get job 'state) 'waiting-queue)) - (get job 'queue-dependant-waiting)) + (cl-assert (and (eq (get job 'type) 'require) + (or (eq (get job 'state) 'waiting-queue) + (and (eq (get job 'state) 'waiting-dep) + (coq-par-dependencies-ready job)))) + nil "coq-par-kickoff-queue-maybe precondition failed") + (put job 'state 'waiting-queue) + (if (get job 'queue-dependant-waiting) (when 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)))) + (message "%s: no queue kickoff because waiting for queue dependency" + (get job 'name))) + ;; first require job in the queue of require jobs (when coq--debug-auto-compilation (message "%s: has itself no queue dependency" (get job 'name))) (unless (get job 'failed) (coq-par-retire-top-level-job job)) - (when (and (get job 'failed) (get job 'require-span)) + (when (get job 'failed) + ;; Reset coq--par-delayed-last-job for the case that this + ;; function was called from a callback in proof-action-list. If + ;; called from elsewhere, this does not harm. (setq coq--par-delayed-last-job nil)) (if (and (get job 'failed) (eq coq--last-compilation-job job) @@ -1430,14 +1434,25 @@ case, the following actions are taken: (cl-assert (not (eq coq--last-compilation-job job)) nil "coq--last-compilation-job invariant error") (put dependant 'queue-dependant-waiting nil) - (when 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) - (when coq--debug-auto-compilation - (message "%s: queue kickoff finished" - (get job 'name)))) + ;; dependant might still wait for dependencies or even + ;; for coqdep to finish + (if (eq (get dependant 'state) 'waiting-queue) + (progn + (when 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) + (when coq--debug-auto-compilation + (message "%s: queue kickoff finished" + (get job 'name)))) + (when coq--debug-auto-compilation + (message + "%s -> %s: clear queue dependency, no queue kickoff for %s" + (get job 'name) (get dependant 'name) + (get dependant 'name))))) + ;; XXX no dependant - this must be the last require job (when (eq coq--last-compilation-job job) (when (get job 'failed) ;; proof-action-list is empty, see above @@ -1445,7 +1460,7 @@ case, the following actions are taken: (with-current-buffer (or proof-script-buffer (current-buffer)) (proof-script-clear-queue-spans-on-error nil)) (proof-release-lock) - (when (and (coq--post-v811) + (when (and (not (coq--post-v811)) (eq coq-compile-quick 'quick-and-vio2vo)) (cl-assert (not coq--compile-vio2vo-delay-timer) nil "vio2vo timer set before last compilation job") @@ -1463,19 +1478,24 @@ case, the following actions are taken: (get job 'name)))))))) (defun coq-par-compile-job-maybe (job) - "Choose next action for JOB after dependencies are ready. + "Compile JOB after dependencies are ready or start next transitions. +This function can only be called for 'file jobs. It must also be +called for failed jobs to finish all necessary transitions. First JOB is put into state 'enqueued-coqc. Then it is determined if JOB needs compilation, what file must be produced (depending on `coq-compile-quick') and if a .vio or .vo file must be deleted. If necessary, deletion happens immediately. If JOB needs compilation, compilation is started or the JOB is enqueued and JOB stays in 'enqueued-coqc for the time being. Otherwise, the -transition 'enqueued-coqc -> 'waiting-queue is done and, if -possible, also 'waiting-queue -> 'ready." +transition 'enqueued-coqc -> 'ready is triggered." + (cl-assert (eq (get job 'type) 'file) + nil "wrong job type in coq-par-compile-job-maybe") (put job 'state 'enqueued-coqc) ;; Note that coq-par-job-needs-compilation sets 'required-obj-file - ;; as a side effect and deletes .vo or .vio files that are in the way. - ;; It also sets the 'vio2vo-needed property if needed. + ;; if compilation is needed (but it might also get set if no + ;; compilation is needed). For Coq < 8.11 .vo or .vio files that are + ;; in the way are deleted. It also sets the 'vio2vo-needed property + ;; if needed. (if (and (not (get job 'failed)) (coq-par-job-needs-compilation job)) (coq-par-start-or-enqueue job) (when coq--debug-auto-compilation @@ -1484,22 +1504,26 @@ possible, also 'waiting-queue -> 'ready." (if (get job 'failed) "failed" "up-to-date"))) (when (get job 'vio2vo-needed) (coq-par-vio2vo-enqueue job)) - (coq-par-kickoff-coqc-dependants job (get job 'youngest-coqc-dependency)))) + (coq-par-kickoff-coqc-dependants job nil))) (defun coq-par-decrease-coqc-dependency (dependant dependee-time dependee-anc-hash) "Clear Coq dependency and update dependee information in DEPENDANT. This function handles a Coq dependency from child dependee to parent dependant when the dependee has finished compilation (ie. -is in state 'waiting-queue). DEPENDANT must be in state +is in state 'ready). DEPENDANT must be in state 'waiting-dep. The time of the most recent ancestor is updated, if necessary using DEPENDEE-TIME. DEPENDEE-TIME must be an Emacs time or 'just-compiled. The ancestors of dependee in hash DEPENDEE-ANC-HASH are propagated to DEPENDANT. The dependency count of DEPENDANT is decreased and, if it reaches 0, the next transition is triggered for DEPENDANT. For 'file jobs this is -'waiting-dep -> 'enqueued-coqc and for 'clone jobs this -'waiting-dep -> 'waiting-queue." +'waiting-dep -> 'enqueued-coqc and for 'require jobs this is +'waiting-dep -> 'waiting-queue. + +This function must be called for failed jobs to complete all +necessary transitions." + ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time) (cl-assert (eq (get dependant 'state) 'waiting-dep) nil "wrong state of parent dependant job") @@ -1516,51 +1540,45 @@ transition is triggered for DEPENDANT. For 'file jobs this is (get dependant 'name) (get dependant 'coqc-dependency-count))) (when (coq-par-dependencies-ready dependant) (cond + ;;; XXX rewrite with if ((eq (get dependant 'type) 'file) (coq-par-compile-job-maybe dependant)) - ((eq (get dependant 'type) 'clone) - (coq-par-kickoff-coqc-dependants - dependant - (get dependant 'youngest-coqc-dependency)))))) - -(defun coq-par-kickoff-coqc-dependants (job dep-time) - "Handle transition to state 'waiting-queue for JOB. -For 'file jobs, this function is called when compilation finished -or was not necessary to make the transition 'enqueued-coqc -> -'waiting-queue. For 'clone jobs, this function is called when its -real 'file job has completed compilation and is in state -'waiting-queue to make the transition 'waiting-dep -> -waiting-queue for JOB. - -DEP-TIME is either 'just-compiled, when JOB has just finished -compilation, or the most recent modification time of all -dependencies of JOB. (If compilation for JOB failed, DEP-TIME is -meaningless but should nevertheless be a non-nil valid argument.) - -This function makes the following actions. -- Clear the dependency from JOB to all its dependants, thereby - propagating the ancestors of JOB and the maximum of DEP-TIME - and the modification time of the .vo of JOB. -- save the maximum of DEP-TIME and .vo modification time in - 'youngest-coqc-dependency, in case we later create a clone of this job -- put JOB into state 'waiting-queue -- try to trigger the transition 'waiting-queue -> ready for JOB -- If JOB is successful but all dependants have failed, unlock all - ancestors in case they are not participating in a still ongoing - compilation." + ((eq (get dependant 'type) 'require) + (coq-par-kickoff-queue-maybe dependant))))) + +(defun coq-par-kickoff-coqc-dependants (job just-compiled) + "Handle transition to state 'ready for file job JOB. +This function can only be called for file jobs and it must also +be called for failed jobs to complete all necessary transitions. +This function is called after compilation has been finished (with +JUST-COMPILED being t) or after determining that compilation was +not necessary or failed (with JUST-COMPILED being nil). This +function sets 'youngest-coqc-dependency to the maximal (youngest) +time stamp of the vo file for this job and all its ancestors. +This function also decreases the dependency counter on all +dependants, propagates 'youngest-coqc-dependency and the +ancestors and starts any necessary state transitions on the +dependants. Finally, if this job has not failed, but all +dependants are marked as failed already, then the ancestors are +unlocked as necessary. + +For the case that JUST-COMPILED is nil and that JOB has not +failed, this function relies on 'obj-mod-time has been set +before." + (cl-assert (not (eq (get job 'type) 'require)) + nil "kickoff-coqc-dependants called for require job") + ;; most actions are not relevant for failed jobs, but do not harm (let ((ancestor-hash (get job 'ancestors)) - (dependant-alive nil)) - (put job 'state 'waiting-queue) - ;; take max of dep-time and obj-mod-time - ;; - ;; dep-time is either 'just-compiled or 'youngest-coqc-dependency of - ;; the dependee, in the latter case obj-mod-time is greater than - ;; dep-time, because otherwise we would have compiled the file. For - ;; a clone job the max has already been taken when processing the - ;; original file. If coqdep failed, 'obj-mod-time is not set. - (unless (or (eq dep-time 'just-compiled) (eq (get job 'type) 'clone) - (get job 'failed)) - (setq dep-time (get job 'obj-mod-time))) + (dependant-alive nil) + ;; take max (youngest) time of this job and all ancestors + ;; + ;; If this job has just been compiled then it is clearly + ;; 'just-compiled. Otherwise it must be 'obj-mod-time, because + ;; if some ancestore were newer, this just would have been + ;; compiled. For failed jobs obj-mod-time might be nil, but + ;; this does not matter. + (dep-time (if just-compiled 'just-compiled + (get job 'obj-mod-time)))) (put job 'youngest-coqc-dependency dep-time) (when coq--debug-auto-compilation (message "%s: kickoff %d coqc dependencies with time %s" @@ -1568,35 +1586,67 @@ This function makes the following actions. (if (eq dep-time 'just-compiled) 'just-compiled (current-time-string dep-time)))) + ;; In the recursion coq-par-kickoff-coqc-dependants -> + ;; coq-par-decrease-coqc-dependency -> coq-par-compile-job-maybe + ;; -> coq-par-kickoff-coqc-dependants jobs on the path upwards + ;; must be in state 'ready, otherwise coq-par-ongoing-compilation + ;; might take one of those as witness for an ongoing compilation. + (put job 'state 'ready) (dolist (dependant (get job 'coqc-dependants)) (coq-par-decrease-coqc-dependency dependant dep-time ancestor-hash) (unless (get dependant 'failed) (setq dependant-alive t))) (when coq--debug-auto-compilation - (message (concat "%s: coqc kickoff finished, %s dependant alive, " - "maybe kickoff queue") + (message (concat "%s: coqc kickoff finished, %s dependant alive") (get job 'name) (if dependant-alive "some" "no"))) - (cl-assert (or (not (get job 'failed)) (not dependant-alive)) - nil "failed job with non-failing dependant") - (when (or (and (not dependant-alive) - (not (get job 'require-span)) - (not (get job 'failed))) - (and (get job 'queue-failed) (not (get job 'failed)))) - ;; job has not failed, but all dependants have 'failed set, or - ;; top-level job marked with 'queue-failed changes to 'failed - (when (get job 'queue-failed) - (when coq--debug-auto-compilation - (message "%s: queue-failed -> failed, unlock ancestors" - (get job 'name))) - (put job 'failed t)) - (coq-par-unlock-job-ancestors-on-error job)) - (coq-par-kickoff-queue-maybe job))) - -(defun coq-par-start-coqdep (job) - "Start coqdep for JOB. -Lock the source file and start the coqdep background process" + (when (and (not dependant-alive) + (not (get job 'failed))) + ;; job has not failed (see first assert), but all dependants + ;; have 'failed set + (coq-par-unlock-job-ancestors-on-error job)))) + +(defun coq-par-start-coqdep-on-require (job) + "Start coqdep for require job JOB. +Write the require statement in JOB into a temporary file and +start coqdep on it. + +This function may be called asynchronously, if the require job +was queued." + ;; get coq-load-path from job + ;; check that this really includes the current dir in the arguments + (let ((load-path + ;; For coq < 8.5 coqdep needs the current working directory + ;; in the load path. This differs from the directory containing + ;; 'temp-require-file. Therefore we add it here and tweek + ;; coq-load-path-include-current such that coq-coqdep-prog-args + ;; does not add the directory containing 'temp-require-file to + ;; load-path. + (if (and coq-load-path-include-current (coq--pre-v85)) + (cons (get job 'current-dir) (get job 'load-path)) + (get job 'load-path))) + (coq-load-path-include-current nil) + (require-command + (mapconcat 'identity (nth 1 (car (get job 'queueitems))) " "))) + (put job 'temp-require-file + (make-temp-file "ProofGeneral-coq" nil ".v" require-command)) + (when coq--debug-auto-compilation + (message "%s: start coqdep for require job for file %s" + (get job 'name) + (get job 'temp-require-file))) + (coq-par-start-process + coq-dependency-analyzer + (coq-par-coqdep-arguments (get job 'temp-require-file) load-path) + 'coq-par-process-coqdep-result + job + (get job 'temp-require-file)))) + +(defun coq-par-start-coqdep-on-file (job) + "Start coqdep for file job JOB. +Lock the source file and start the coqdep background process." (when (and coq-lock-ancestors + ;; the lock state property is initialized from all as + ;; locked registered files in `proof-included-files-list' (eq (get job 'lock-state) 'unlocked)) (proof-register-possibly-new-processed-file (get job 'src-file)) (puthash job t (get job 'ancestors)) @@ -1608,6 +1658,29 @@ Lock the source file and start the coqdep background process" job nil)) +(defun coq-par-start-coqc (job) + "Start coqc background compilation for JOB. +Depending on property 'use-quick, vos or quick compilation may be +used." + (message "Recompile %s%s" + (cond + ((eq (get job 'use-quick) 'vos) "-vos ") + ((eq (get job 'use-quick) 'vio) "-quick ") + (t "")) + (get job 'src-file)) + (let ((arguments + (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path)))) + (cond + ((eq (get job 'use-quick) 'vos) (push "-vos" arguments)) + ((eq (get job 'use-quick) 'vio) (push "-quick" arguments)) + (t t)) + (coq-par-start-process + coq-compiler + arguments + 'coq-par-coqc-continuation + job + (get job 'required-obj-file)))) + (defun coq-par-start-vio2vo (job) "Start vio2vo background job." (let ((arguments (coq-include-options (get job 'load-path))) @@ -1631,36 +1704,23 @@ Lock the source file and start the coqdep background process" (defun coq-par-start-task (job) "Start the background job for which JOB is waiting. JOB was at the head of the compilation queue and now either -coqdep or coqc are started for it." +coqdep, coqc or vio2vo is started for it. This function may be called +synchronously or asynchronously." (let ((job-state (get job 'state))) (cond + ((and (eq job-state 'enqueued-coqdep) (eq (get job 'type) 'require)) + (coq-par-start-coqdep-on-require job)) ((eq job-state 'enqueued-coqdep) - (coq-par-start-coqdep job)) + (coq-par-start-coqdep-on-file job)) ((eq job-state 'enqueued-coqc) - (message "Recompile %s%s" - (cond - ((eq (get job 'use-quick) 'vos) "-vos ") - ((eq (get job 'use-quick) 'vio) "-quick ") - (t "")) - (get job 'src-file)) - (let ((arguments - (coq-par-coqc-arguments (get job 'src-file) (get job 'load-path)))) - (cond - ((eq (get job 'use-quick) 'vos) (push "-vos" arguments)) - ((eq (get job 'use-quick) 'vio) (push "-quick" arguments)) - (t t)) - (coq-par-start-process - coq-compiler - arguments - 'coq-par-coqc-continuation - job - (get job 'required-obj-file)))) + (coq-par-start-coqc job)) ((eq job-state 'ready) (coq-par-start-vio2vo job)) (t (cl-assert nil nil "coq-par-start-task with invalid job"))))) (defun coq-par-start-jobs-until-full () - "Start background jobs until the limit is reached." + "Start background jobs until the limit is reached. +This function may be called synchronously or asynchronously." (let ((max-jobs (if coq--compile-vio2vo-in-progress coq--internal-max-vio2vo-jobs coq--internal-max-jobs)) @@ -1675,100 +1735,118 @@ coqdep or coqc are started for it." "Start NEW-JOB or put it into the queue of waiting jobs. 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." +room for Proof General. This function might be called +synchronously or asynchronously." (if (< (1+ coq--current-background-jobs) coq--internal-max-jobs) (coq-par-start-task new-job) (coq-par-job-enqueue new-job))) -(defun coq-par-create-library-job (module-vo-file coq-load-path queue-dep - require-span dependant) - "Create a new compilation job for MODULE-OBJ-FILE. -If there is already a job for MODULE-OBJ-FILE a new clone job is -created. This function initializes all necessary properties of -the new job. - -COQ-LOAD-PATH must be the load path from the source file that -originally initiated the compilation. QUEUE-DEP must be a -compilation job or nil. If non-nil, this function makes a queue -dependency from QUEUE-DEP to the new compilation job. If nil, a -newly created clone job will proceed to state ready if the -original job is ready. Argument REQUIRE-SPAN should be present -when the new job should update the ancestor list in some span. -Argument DEPENDANT tells who required MODULE-OBJ-FILE, this is -used only for the error message, in case MODULE-OBJ-FILE refers -to the current scriping buffer. - -If the new job is a clone job, its state is -- 'waiting-dep if the original file job is not 'ready yet -- 'waiting-queue if the original file job is ready, but there is - a queue dependency QUEUE-DEP (which cannot be ready yet) -- 'ready otherwise - -If the new job is a 'file job its state is 'enqueued-coqdep. If -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)) - (new-job (make-symbol "coq-compile-job-symbol"))) +(defun coq-par-job-init-common (coq-load-path type) + "Common initialization for 'require and 'file jobs. +Create a new job of type TYPE and initialize all common fields of +require and file jobs that need an initialization different from +nil." + (let ((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 'vo-file module-vo-file) (put new-job 'coqc-dependency-count 0) - (put new-job 'require-span require-span) + (put new-job 'type type) + (put new-job 'state 'enqueued-coqdep) + ;; The ancestor modification time is not really needed in require + ;; jobs, however, if the field is present, we can treat require + ;; and file jobs more uniformely. + (put new-job 'youngest-coqc-dependency '(0 0)) (put new-job 'ancestors (make-hash-table :size 7 :rehash-size 2.1)) - ;; fields 'required-obj-file and obj-mod-time are implicitely set to nil - (if orig-job - ;; there is already a compilation job for module-vo-file - (progn - (put new-job 'type 'clone) - (when 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 - (coq-par-add-queue-dependency queue-dep new-job)) - (if (coq-par-job-coqc-finished orig-job) - (progn - (if queue-dep - (put new-job 'state 'waiting-queue) - (put new-job 'state 'ready)) - (put new-job 'youngest-coqc-dependency - (get orig-job 'youngest-coqc-dependency)) - (merge-hash-content (get new-job 'ancestors) - (get orig-job 'ancestors))) - (coq-par-add-coqc-dependency orig-job new-job) - (put new-job 'state 'waiting-dep) - (put new-job 'youngest-coqc-dependency '(0 0)))) - ;; there is no compilation job for this file yet - (put new-job 'type 'file) - (put new-job 'state 'enqueued-coqdep) + (put new-job 'load-path coq-load-path) + new-job)) + +(defun coq-par-create-require-job (coq-load-path require-items require-span) + "Create a new require job for REQUIRE-SPAN. +Create a new require job and initialize its fields. COQ-LOAD-PATH +is the load path configured for the current scripting buffer, +that is passed down to all dependencies and used in all +compilations. REQUIRE-ITEMS are the non-require commands +following the REQUIRE-SPAN, they are temporarily stored in the +new require job outside of `proof-action-list'. + +The current directory (from `default-directory') is stored in +property 'current-dir for <8.5 compatibility, where coqdep did +not search the current directory. + +This function is called synchronously when asserting. The new +require job is neither started nor enqueued here - the caller +must do this." + (let ((new-job (coq-par-job-init-common coq-load-path 'require))) + (put new-job 'require-span require-span) + (put new-job 'queueitems require-items) + (put new-job 'current-dir default-directory) + (when coq--debug-auto-compilation + (let* ((require-item (car require-items)) + (require-command (mapconcat 'identity (nth 1 require-item) " "))) + (message "%s: create require job for %s" + (get new-job 'name) require-command))) + new-job)) + +;; XXX what happens when job exists but has been unlocked because +;; there was some error and it was not used anywhere back then, but +;; job is now needed as a dependency of some other file? +;; XXX what happens if the job exists and is failed? +(defun coq-par-create-file-job (module-vo-file coq-load-path dep-src-file) + "Create a new file job for MODULE-VO-FILE. +DEP-SRC-FILE is the source file whose coqdep output we are just +processing and which depends on MODULE-VO-FILE. This argument is +only used in the error message, when MODULE-VO-FILE happens to +coincide with the current scripting buffer (which means we +detected a dependency cycle). + +If there is a file job for MODULE-VO-FILE, just return this. +Otherwise, create a new file job and initialize its fields. In +particular, initialize its 'lock-state property from the set of +as locked registered files in `proof-included-files-list'. + +If a new job is created it is started or enqueued right away." + (cond + ((gethash module-vo-file coq--compilation-object-hash)) + (t + (let ((new-job (coq-par-job-init-common coq-load-path 'file))) + ;; fields 'required-obj-file and obj-mod-time are implicitely set to nil + (put new-job 'vo-file module-vo-file) (put new-job 'src-file (coq-library-src-of-vo-file module-vo-file)) (when (equal (get new-job 'src-file) (buffer-file-name proof-script-buffer)) + ;; test this error case - maybe need more files participating + ;; in the circle? (signal 'coq-compile-error-circular-dep - (concat dependant " -> scripting buffer"))) - (put new-job 'load-path coq-load-path) - (put new-job 'youngest-coqc-dependency '(0 0)) + (concat dep-src-file " -> scripting buffer"))) (puthash module-vo-file new-job coq--compilation-object-hash) (when coq--debug-auto-compilation (message "%s: create %s compilation for %s" (get new-job 'name) (get new-job 'type) module-vo-file)) + ;; if the user single-steps through multiple requires, then the + ;; compilation for the previous require might have been finished + ;; and cleared, then we might have visited and locked this file + ;; already (if (member (file-truename (get new-job 'src-file)) proof-included-files-list) (put new-job 'lock-state 'asserted) (put new-job 'lock-state 'unlocked)) - (when queue-dep - (coq-par-add-queue-dependency queue-dep new-job)) (message "Check %s" (get new-job 'src-file)) - (coq-par-start-or-enqueue new-job)) - new-job)) + (coq-par-start-or-enqueue new-job) + new-job)))) (defun coq-par-ongoing-compilation (job) "Determine if the source file for JOB needs to stay looked. Return t if job has a direct or indirect dependant that has not -failed yet and that is in a state before 'waiting-queue. Also, +failed yet and that is in a state before 'ready. Also, return t if JOB has a dependant that is a top-level job which has not yet failed." + ;; This function is called on jobs with 'lock-state 'locked. A job + ;; that is 'asserted has all its ancestors 'asserted as well. + ;; Therefore all direct and indirect dependants of job (i.e., + ;; everything above) cannot be 'asserted. In a stable state all + ;; dependants must be 'locked. But when this function is called, + ;; ancestors from some failing job are unlocked in no particular + ;; order, therefore some dependant might already be 'unlocked. (cl-assert (not (eq (get job 'lock-state) 'asserted)) nil "coq-par-ongoing-compilation precondition failed") (cond @@ -1777,21 +1855,24 @@ not yet failed." ((or (eq (get job 'state) 'waiting-dep) (eq (get job 'state) 'enqueued-coqc) ;; top-level job that has compilation finished but has not - ;; been asserted yet - (and (eq (get job 'state) 'waiting-queue) (get job 'require-span)) + ;; been asserted yet and has not been set to 'failed (see + ;; first cond check) + (eq (get job 'state) 'waiting-queue) ;; Note that job cannot be a top-level in state 'ready, ;; because we started from job with 'lock-state property equal ;; to 'locked. Top-level job in state 'ready have all ;; dependees with 'lock-state equal to 'asserted. ) t) - ;; Note that non-top-level jobs switch to 'waiting-queue as soon as - ;; all dependencies are ready, before they start to deal with the - ;; ancestors. We might therefore see here non-top-level jobs in - ;; state 'waiting-queue: they have successfully finished their - ;; compilation and are about to go to state 'ready. - ((or (eq (get job 'state) 'ready) - (eq (get job 'state) 'waiting-queue)) + ;; The following recursive clause needs to match file and require + ;; jobs that were ready, before the current mark-failing or + ;; unlocking-ancestors procedure started. Additionally, it also + ;; needs to match dependants that are right now inside + ;; coq-par-kickoff-coqc-dependants in the loop to propagate their + ;; ancestors to their dependants. Therefore it is important that + ;; coq-par-kickoff-coqc-dependants sets the state to 'ready quite + ;; early. + ((eq (get job 'state) 'ready) ;; internal ready job (let ((dependants (get job 'coqc-dependants)) (res nil) @@ -1804,9 +1885,12 @@ not yet failed." "impossible ancestor state %s on job %s" (get job 'state) (get job 'name))))) +;; XXX check whether this needs to be called only when job is set to 'failed +;; - when job was set to failed earlier, then the ancestors should have been +;; unlocked earlier too (defun coq-par-unlock-job-ancestors-on-error (job) "Unlock those ancestors of JOB that need to be unlocked. -For a failing job JOB, an ancestor need to stay looked if there +For a failing job JOB, an ancestor needs to stay looked if there is still some compilation going on for which this ancestor is a dependee or if a top level job with JOB as ancestor has finished it's compilation successfully. In all other cases the ancestor @@ -1823,23 +1907,20 @@ must be unlocked." (get job 'ancestors))) (defun coq-par-mark-queue-failing (job) - "Mark JOB with 'queue-failed. -Mark JOB with 'queue-failed, and, if JOB is in state -'waiting-queue, transition to 'failed and unlock ancestors as -appropriate." - (unless (or (get job 'failed) (get job 'queue-failed)) - (put job 'queue-failed t) + "Mark require JOB and its queue dependants with 'failed. +Mark JOB with 'failed and unlock ancestors as appropriate. +Recurse for queue dependants." + (unless (get job 'failed) + (put job 'failed t) (cl-assert (not (eq (get job 'state) 'ready)) nil "coq-par-mark-queue-failing impossible state") (when coq--debug-auto-compilation - (message "%s: mark as queue-failed, %s" + (message "%s: mark as failed, %s" (get job 'name) (if (eq (get job 'state) 'waiting-queue) - "failed, and unlock ancestors" + "and unlock ancestors" "wait"))) - (when (eq (get job 'state) 'waiting-queue) - (put job 'failed t) - (coq-par-unlock-job-ancestors-on-error job)) + (coq-par-unlock-job-ancestors-on-error job) (when (get job 'queue-dependant) (coq-par-mark-queue-failing (get job 'queue-dependant))))) @@ -1847,8 +1928,7 @@ appropriate." "Mark all dependants of JOB as failing and unlock ancestors as appropriate. Set the 'failed property on all direct and indirect dependants of JOB. Along the way, unlock ancestors as determined by -`coq-par-ongoing-compilation'. Mark queue dependants with -'queue-failed." +`coq-par-ongoing-compilation'." (unless (get job 'failed) (put job 'failed t) (when coq--debug-auto-compilation @@ -1865,17 +1945,19 @@ This function analyses the coqdep output of PROCESS. In case of error, the job is marked as failed or compilation is aborted via a signal (depending on `coq-compile-keep-going'). If there was no coqdep error, the following actions are taken. +- temp-require-file for require jobs is deleted - the job that started PROCESS is put into sate 'waiting-dep - a new job is created for every dependency. If this new job is - not immediately ready, a Coq dependency is registered from the + not immediately ready, a dependency is registered from the new job to the current job. For dependencies that are 'ready already, the most recent ancestor modification time is propagated. - if there are no dependencies (especially if coqdep failed) or - all dependencies are ready already, the next transition to - 'enqueued-coqc is triggered for the current job + all dependencies are ready already, the next transition is + triggered. For file jobs the next transition goes to + 'enqueued-coqc, for require jobs it goes to 'waiting-queue. - otherwise the current job is left alone until somebody - decreases its dependency count to 0 + decreases its dependency count to 0. The argument EXIT-STATUS must be the exit status of PROCESS, it is directly passed to `coq-par-analyse-coq-dep-exit'." @@ -1887,25 +1969,37 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (process-get process 'coq-process-command))) job-max-time) (if (stringp dependencies-or-error) - (if coq-compile-keep-going - (coq-par-mark-job-failing job) - (signal 'coq-compile-error-coqdep (get job 'src-file))) + (progn + (when coq--debug-auto-compilation + (message "%s coqdep error %s" (get job 'name) dependencies-or-error)) + (if coq-compile-keep-going + (coq-par-mark-job-failing job) + (signal 'coq-compile-error-coqdep (get job 'src-file)))) ;; no coqdep error -- work on dependencies (when coq--debug-auto-compilation (message "%s: dependencies of %s are %s" - (get job 'name) (get job 'src-file) dependencies-or-error)) + (get job 'name) + (if (eq (get job 'type) 'file) + (get job 'src-file) + (get job 'temp-require-file)) + dependencies-or-error)) + (when (get job 'temp-require-file) + (ignore-errors (delete-file (get job 'temp-require-file)))) (setq job-max-time (get job 'youngest-coqc-dependency)) (dolist (dep-vo-file dependencies-or-error) (unless (coq-compile-ignore-file dep-vo-file) - (let* ((dep-job (coq-par-create-library-job dep-vo-file - (get job 'load-path) - nil nil - (get job 'src-file))) + (let* ((dep-job (coq-par-create-file-job dep-vo-file + (get job 'load-path) + (get job 'src-file))) (dep-time (get dep-job 'youngest-coqc-dependency))) - (when (coq-par-time-less job-max-time dep-time) - (setq job-max-time dep-time)) - (unless (coq-par-job-coqc-finished dep-job) + ;; XXX what happens when dep-job failed? + (unless (eq (get dep-job 'state) 'ready) + ;; the following clause is not needed for require jobs, + ;; but it doesn't harm either, so keep the code a little + ;; bit more simple + (when (coq-par-time-less job-max-time dep-time) + (setq job-max-time dep-time)) (coq-par-add-coqc-dependency dep-job job))))) (put job 'youngest-coqc-dependency job-max-time)) ;; common part for job where coqdep was successful and where @@ -1915,7 +2009,10 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." (progn (when coq--debug-auto-compilation (message "%s: coqc dependencies finished" (get job 'name))) - (coq-par-compile-job-maybe job)) + (if (eq (get job 'type) 'file) + (coq-par-compile-job-maybe job) + ;; require jobs + (coq-par-kickoff-queue-maybe job))) (when coq--debug-auto-compilation (message "%s: wait for %d dependencies" (get job 'name) (get job 'coqc-dependency-count)))))) @@ -1924,7 +2021,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'." "Coqc continuation function. If coqc failed, signal an error or mark the job as 'failed, and unlock ancestors as appropriate. If coqc was successful, trigger -the transition 'enqueued-coqc -> 'waiting-queue for the job +the transition 'enqueued-coqc -> 'ready for the job behind PROCESS." (let ((job (process-get process 'coq-compilation-job))) (if (eq exit-status 0) @@ -1932,7 +2029,7 @@ behind PROCESS." ;; coqc success (when (get job 'vio2vo-needed) (coq-par-vio2vo-enqueue job)) - (coq-par-kickoff-coqc-dependants job 'just-compiled)) + (coq-par-kickoff-coqc-dependants job t)) ;; coqc error (coq-compile-display-error (mapconcat 'identity (process-get process 'coq-process-command) " ") @@ -1941,14 +2038,13 @@ behind PROCESS." (if coq-compile-keep-going (progn (coq-par-mark-job-failing job) - (coq-par-kickoff-coqc-dependants - job - (get job 'youngest-coqc-dependency))) + (coq-par-kickoff-coqc-dependants job nil)) (signal 'coq-compile-error-coqc (get (process-get process 'coq-compilation-job) 'src-file)))))) (defun coq-par-vio2vo-continuation (process exit-status) - "Vio2vo continuation function." + "Vio2vo continuation function. +Nothing to do in case of success. Otherwise display the errors." (let ((job (process-get process 'coq-compilation-job))) (if (eq exit-status 0) ;; success - nothing to do @@ -1970,96 +2066,44 @@ behind PROCESS." ;;; handle Require commands when queue is extended -(defun coq-par-handle-module (module-id span &optional from) - "Handle compilation of module MODULE-ID. -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'. - -This function must be evaluated with the buffer that triggered -the compilation as current, otherwise a wrong `coq-load-path' -might be used." - (when coq--debug-auto-compilation - (if from - (message "handle required module \"%s\" from \"%s\"" module-id from) - (message "handle required module \"%s\" without from clause" module-id))) - (let ((module-vo-file - (coq-par-map-module-id-to-vo-file module-id coq-load-path from)) - module-job) - (when coq--debug-auto-compilation - (if module-vo-file - (message "check compilation for module %s from object file %s" - module-id module-vo-file) - (message "nothing to check for module %s" module-id))) - ;; coq-par-map-module-id-to-vo-file currently returns () for - ;; standard library modules! - (when (and module-vo-file - (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 - "scripting buffer")) - (setq coq--last-compilation-job module-job) - (when coq--debug-auto-compilation - (message "%s: this job is the last compilation job now" - (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. REQUIRE-ITEMS is a list of queue items, eventually to be added to `proof-action-list', that contains just one require command in the first element. This function starts the compilation process -for all modules in this require command. - -This function parses the Require command, translates module names -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 -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) +for all modules and their dependencies in this require command. + +This function creates one require job for the require command, +maintains `coq--last-compilation-job' and adds the delete action +to delete all ancestors to the span of the require command. +Coqdep is directly started on the require job or the job is +enqueued. + +This function must be evaluated with the buffer that triggered +the compilation as current, otherwise a wrong `coq-load-path' +might be used. + +This function is called synchronously when asserting." + (let ((span (caar require-items)) + new-job) (when 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. - (string-match coq-require-command-regexp string) - (setq start (match-end 0)) - (setq prefix (match-string 1 string)) + (let* ((require-item (car require-items)) + (require-command (mapconcat 'identity (nth 1 require-item) " "))) + (message "handle require command \"%s\"" require-command))) (span-add-delete-action span `(lambda () (coq-unlock-all-ancestors-of-span ,span))) - ;; add a compilation job for all required modules - (while (string-match coq-require-id-regexp string start) - (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 - (progn - (cl-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) - require-items)) - (when coq--debug-auto-compilation - (message "%s: attach %s items (containing now %s items)" - (get coq--last-compilation-job 'name) - (length require-items) - (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)) - (when coq--debug-auto-compilation - (message "attach %s items to queueitems (containing now %s items)" - (length require-items) - (length queueitems)))))) - + ;; create a new require job and maintain coq--last-compilation-job + (setq new-job (coq-par-create-require-job coq-load-path require-items span)) + (when coq--last-compilation-job + (coq-par-add-queue-dependency coq--last-compilation-job new-job)) + (setq coq--last-compilation-job new-job) + (when coq--debug-auto-compilation + (message "%s: this job is the last compilation job now" + (get coq--last-compilation-job 'name))) + (coq-par-start-or-enqueue new-job))) + (defun coq-par-item-require-predicate (item) "Return t if ITEM contains a Require command. @@ -2080,24 +2124,26 @@ 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 already 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 -the ancestor hash are initialized. +the ancestor hash are reinitialized. As next action the new queue items are splitted at each Require command. The items before the first Require are appended to the last compilation job or put back into ‘proof-action-list’. The remaining batches of items that each start with a Require are then processed by `coq-par-handle-require-list', which creates -top-level compilation jobs as necessary. Before processing the +require jobs as necessary. Before processing the first of these batches, buffers are saved with -`coq-compile-save-some-buffers'. +`coq-compile-save-some-buffers' and an possibly ongoing vio2vo +compilation is stopped. 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." +the maximal number of background compilation jobs is started. +This function is called synchronously when asserting." (when coq--debug-auto-compilation (message "%d items were added to the queue, scan for require" (length queueitems))) @@ -2151,7 +2197,8 @@ If `coq-compile-before-require' is non-nil, this function starts the compilation (if necessary) of the dependencies ansynchronously in parallel in the background. This function only does the error checking/reporting for -`coq-par-preprocess-require-commands-internal', which does all the work." +`coq-par-preprocess-require-commands-internal', which does all +the work. This function is called synchronously when asserting." (when coq-compile-before-require (condition-case err (coq-par-preprocess-require-commands-internal)