diff options
| author | Hendrik Tews | 2020-12-05 22:27:47 +0100 |
|---|---|---|
| committer | hendriktews | 2020-12-19 16:43:49 +0100 |
| commit | 16e784a63f2a38ce3f03e36b6fa9a7db2da211b9 (patch) | |
| tree | 40c0e559f5f0bab2729fb30f1536d43e6b63a064 /coq | |
| parent | 163ff8d20276be0e932474cdd6cb2c3086c5be9c (diff) | |
add test for recompilation with changes
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))) |