add test for recompilation with changes

1 files changed, 71 insertions, 0 deletions

diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 42003d1c..532cd92a 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -29,6 +29,39 @@ says, programs should use this piece of code."
   (goto-char (point-min))
   (forward-line (1- line)))
 
+(defun cct-library-vo-of-v-file (v-src-file)
+  "Return .vo file name for V-SRC-FILE.
+Changes the suffix from .v to .vo.  V-SRC-FILE must have a .v suffix."
+  (concat v-src-file "o"))
+
+(defun cct-record-change-time (file)
+  "Return cons of FILE and its modification time.
+The modification time is an emacs time value, it's nil if file
+cannot be accessed."
+  (cons file (nth 5 (file-attributes file))))
+
+(defun cct-record-change-times (files)
+  "Return an assoc list of FILES with their modification times.
+The modification time is an emacs time value, it's nil if file
+cannot be accessed."
+  (mapcar 'cct-record-change-time files))
+
+(defun cct-split-change-times (file-change-times files)
+  "Split assoc list FILE-CHANGE-TIMES.
+FILE-CHANGE-TIMES must be an assoc list and FILES must be a
+subset (i.e., each key occoring at most once) of the keys of
+FILE-CHANGE-TIMES as list. This function returns two associations
+lists (as cons cell). The car contains those associations in
+FILE-CHANGE-TIMES with keys not in FILES, the cdr contains those
+with keys in FILES."
+  (seq-reduce
+   (lambda (acc file)
+     (push (assoc file (car acc)) (cdr acc))
+     (setcar acc (assoc-delete-all file (car acc)))
+     acc)
+   files
+   (cons (copy-alist file-change-times) nil)))
+
 (defun cct-process-to-line (line)
   "Assert/retract to line LINE and wait until processing completed."
   (cct-goto-line line)
@@ -108,11 +141,49 @@ documentation of coq/coq-par-compile.el."
     (should
      (seq-set-equal-p locked-ancestors ancestors))))
 
+(defun cct-file-unchanged (file time)
+  "Check that modification time of FILE equals TIME.
+Used to check that FILE has not been changed since TIME was
+recorded before."
+  (let ((file-time (nth 5 (file-attributes file))))
+    ;; (message "TFU on %s: rec: %s now: %s\n"
+    ;;          file
+    ;;          (format-time-string "%H:%M:%S.%3N" time)
+    ;;          (format-time-string "%H:%M:%S.%3N" file-time))
+    (should
+     (and file-time (equal time file-time)))))
+
+(defun cct-unmodified-change-times (file-time-assoc)
+  "Check that files in FILE-TIME-ASSOC have not been changed.
+FILE-TIME-ASSOC must be an association list of files and emacs
+times as returned by `cct-record-change-times' or
+`cct-split-change-times'. This function checks that the
+modification time of files in FILE-TIME-ASSOC equals the time
+recorded in FILE-TIME-ASSOC, i.e., that the file has not been
+changed since FILE-TIME-ASSOC has been recorded."
+  (mapc
+   (lambda (file-time-cons)
+     (cct-file-unchanged (car file-time-cons) (cdr file-time-cons)))
+   file-time-assoc))
+
 (defun cct-file-newer (file time)
   "Check that FILE exists and its modification time is more recent than TIME."
   (let ((file-time (nth 5 (file-attributes file))))
     (should (and file-time (time-less-p time file-time)))))
 
+(defun cct-older-change-times (file-time-assoc)
+  "Check that files exist and have been changed.
+FILE-TIME-ASSOC must be an association list of files and emacs
+times as returned by `cct-record-change-times' or
+`cct-split-change-times'. This function checks that the files in
+FILE-TIME-ASSOC do exist and that their modification time is more
+recent than in the association list, i.e., they have been updated
+or changed since recording the time in the association."
+  (mapc
+   (lambda (file-time-cons)
+     (cct-file-newer (car file-time-cons) (cdr file-time-cons)))
+   file-time-assoc))
+
 (defun cct-configure-proof-general ()
   "Configure Proof General for test execution."
   (setq delete-old-versions t