diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-compile-common.el | 4 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 8 |
2 files changed, 7 insertions, 5 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index ed927409..3e3b7023 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -600,8 +600,8 @@ Changes the suffix from .vo to .vio. VO-OBJ-FILE must have a .vo suffix." (concat (coq-library-src-of-vo-file vo-obj-file) "io")) (defun coq-library-vos-of-vo-file (vo-obj-file) - "Return .vok file name for VO-OBJ-FILE. -Changes the suffix from .vo to .vok. VO-OBJ-FILE must have a .vo suffix." + "Return .vos file name for VO-OBJ-FILE. +Changes the suffix from .vo to .vos. VO-OBJ-FILE must have a .vo suffix." (concat vo-obj-file "s")) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index a914ec74..7710a029 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -25,18 +25,19 @@ ;; ;; - fix -I current-dir argument for coqc invocations ;; - on error, try to put location info into the error message +;; - use file-attribute-modification-time and similar functions when +;; dropping support for emacs 25 (emacs 26.1 released on 05/2018) +;; - use define-error when dropping support for emacs 24 (25.1 +;; released on 09/2016) ;; ;; 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 ;; - a job depending on a failed dependee, where the dependee has been finished before ;;; Code: @@ -664,6 +665,7 @@ in a 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 + ;; XXX only recurse for dependants not visited yet (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))) |