Skip to content

Commit

Permalink
redesign of parallel background compilation without clones
Browse files Browse the repository at this point in the history
- no clones any more, existing jobs are directly linked
- the whole require command is processed by coqdep to determine
  the required files, this fixes ProofGeneral#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
  • Loading branch information
hendriktews committed Oct 31, 2020
1 parent 0fdb1ae commit 9745afc
Show file tree
Hide file tree
Showing 2 changed files with 647 additions and 599 deletions.
1 change: 1 addition & 0 deletions coq/coq-compile-common.el
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading

0 comments on commit 9745afc

Please sign in to comment.