include compile tests in CI elisp compilation

1 files changed, 221 insertions, 0 deletions

diff --git a/ci/compile-tests/005-change-recompile/runtest.el b/ci/compile-tests/005-change-recompile/runtest.el
new file mode 100644
index 00000000..c5d7f9b3
--- /dev/null
+++ b/ci/compile-tests/005-change-recompile/runtest.el
@@ -0,0 +1,221 @@
+;; This file is part of Proof General.
+;;
+;; © Copyright 2020  Hendrik Tews
+;;
+;; Authors: Hendrik Tews
+;; Maintainer: Hendrik Tews <hendrik@askra.de>
+;;
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+;; Coq Compile Tests (cct) --
+;; ert tests for parallel background compilation for Coq
+;;
+;; Test that the right files are recompiled when changes are made in
+;; the dependency hierarchy and that unaffected ancestors are not
+;; touched.
+;;
+;; The following graph shows the file dependencies in this test:
+;;
+;;           a
+;;          / \
+;;         b   c
+;;        /   / \
+;;       d   e   f
+;;      / \  |  /
+;;     |   \ | /
+;;     |    \|/
+;;     g     h
+;;
+;;
+;;
+;;
+;;
+;;
+;;
+
+;; require cct-lib for the elisp compilation, otherwise this is present already
+(require 'cct-lib)
+
+;;; set configuration
+(cct-configure-proof-general)
+
+;;; Data and utility functions
+
+(defconst b-ancestors '("./b.v" "./d.v" "./g.v" "./h.v")
+  "Ancestors of b.v.")
+
+(defconst c-ancestors '("./c.v" "./e.v" "./f.v")
+  "Ancestors of c.v.")
+
+(defconst all-ancestors (append b-ancestors c-ancestors)
+  "All ancestors.")
+
+(defconst all-compiled-ancestors
+  (mapcar 'cct-library-vo-of-v-file all-ancestors)
+  "All vo ancestors files.")
+  
+
+(defun cct-replace-last-word (line word)
+  "Replace last word in line LINE with WORD.
+In current buffer, go to the end of line LINE and one word
+backward. Replace the word there with WORD."
+  (cct-goto-line line)
+  (end-of-line)
+  (backward-word)
+  (kill-word 1)
+  (insert word))
+
+(defun cct-check-main-buffer (vo-times new-sum recompiled-files
+                                       other-locked-files)
+  "Perform various checks for recompilation in buffer a.v.
+Combine all the following tests in this order:
+- line 21 in a.v is unlocked
+- after replacing the sum on line 28 with NEW-SUM, a.v can be
+  processed until line 38
+- files in VO-TIMES not listed in RECOMPILED-FILES have the same
+  last change time as in VO-TIMES
+- files in RECOMPILED-FILES have a newer change time
+- the spans in line 22 and 23 hold the ancestors of b and c, respectively.
+- all the buffers in OTHER-LOCKED-FILES are locked until line 18."
+  (let (splitted)
+    (set-buffer "a.v")
+    (cct-check-locked 21 'unlocked)
+    (cct-replace-last-word 28 new-sum)
+    (cct-process-to-line 38)
+    (cct-check-locked 37 'locked)
+    (setq splitted (cct-split-change-times vo-times recompiled-files))
+    (cct-unmodified-change-times (car splitted))
+    (cct-older-change-times (cdr splitted))
+    (cct-locked-ancestors 22 b-ancestors)
+    (cct-locked-ancestors 23 c-ancestors)
+    (mapc
+     (lambda (b)
+       (set-buffer b)
+       (cct-check-locked 18 'locked))
+     other-locked-files)))
+
+
+;;; The test itself
+
+(ert-deftest cct-change-recompile ()
+  "Test successful recompilation after changes and deletion."
+  (find-file "a.v")
+
+  ;; 1. process original content - compile everything
+  (message "\n1. process original content - compile everything\n")
+  (cct-process-to-line 38)
+  (cct-check-locked 37 'locked)
+  (cct-locked-ancestors 22 b-ancestors)
+  (cct-locked-ancestors 23 c-ancestors)
+
+  (let ((vo-times (cct-record-change-times all-compiled-ancestors))
+        other-locked-files)
+
+    ;; 2. retract and process again - nothing should be compiled
+    (message "\n2. retract and process again - nothing should be compiled\n")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer vo-times "35" nil nil)
+
+    ;; 3. change c and process again - only c should be compiled
+    (message "\n3. change c and process again - only c should be compiled\n")
+    (find-file "c.v")
+    (push "c.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "4")
+    (cct-check-main-buffer vo-times "36" '("./c.vo") other-locked-files)
+
+    ;; 4. change h and process again - everything except g should get compiled
+    (message (concat "\n4. change h and process again - "
+                         "everything except g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "h.v")
+    (push "h.v" other-locked-files)
+    (cct-check-locked 21 'locked)
+    (cct-replace-last-word 21 "10")
+    (cct-check-main-buffer
+     vo-times "38" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
+     other-locked-files)
+    
+    ;; 5. change d and f and process again -
+    ;; only b, c, d and f should get recompiled
+    (message (concat "\n5. change d and f and process again - "
+                         "only b, c, d and f should get recompiled"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "d.v")
+    (push "d.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "7")
+    (find-file "f.v")
+    (push "f.v" other-locked-files)
+    (cct-check-locked 23 'unlocked)
+    (cct-replace-last-word 23 "10")
+
+    (cct-check-main-buffer
+     vo-times "45" '("./b.vo" "./c.vo" "./d.vo" "./f.vo") other-locked-files)
+
+    ;; 6. change d and b and process again - only d and b should get compiled
+    (message (concat "\n6. change d and b and process again - "
+                         "only d and b should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (find-file "b.v")
+    (push "b.v" other-locked-files)
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "7")
+    (set-buffer "d.v")
+    (cct-check-locked 23 'unlocked)
+    (cct-replace-last-word 23 "13")    ; increase by 6
+
+    (cct-check-main-buffer vo-times "56" '("./b.vo" "./d.vo")
+                           other-locked-files)
+    
+    ;; 7. delete b and process again - only b should get compiled
+    (message (concat "\n7. delete b and process again - "
+                         "only b should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (delete-file "b.vo")
+    (set-buffer "a.v")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer vo-times "56" '("./b.vo") other-locked-files)
+    
+    ;; 8. delete h and process again - everything except g should get compiled
+    (message (concat "\n8. delete h and process again - "
+                         "everything except g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (delete-file "h.vo")
+    (set-buffer "a.v")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer
+     vo-times "56" '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./h.vo")
+     other-locked-files)
+    
+    ;; 9. change d, delete g and process again - only b, d and g should
+    ;; get compiled
+    (message (concat "\n9. change d, delete g and process again - "
+                         "only b, d and g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (set-buffer "d.v")
+    (cct-check-locked 23 'locked)
+    (cct-replace-last-word 23 "20")     ; increase by 7
+    (delete-file "g.vo")
+    (set-buffer "a.v")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer vo-times "63" '("./b.vo" "./d.vo" "./g.vo")
+                           other-locked-files)
+    
+    ;; 10. delete d, change g and process again - only b, d and g should
+    ;; get compiled
+    (message (concat "\n10. delete d, change g and process again - "
+                         "only b, d and g should get compiled\n"))
+    (setq vo-times (cct-record-change-times all-compiled-ancestors))
+    (delete-file "d.vo")
+    (find-file "g.v")
+    (push "g.v" other-locked-files)
+    (cct-check-locked 21 'locked)
+    (cct-replace-last-word 21 "15")     ; increase by 8
+    (set-buffer "a.v")
+    (cct-process-to-line 21)
+    (cct-check-main-buffer vo-times "71" '("./b.vo" "./d.vo" "./g.vo")
+                           other-locked-files)
+  ))