;; This file is part of Proof General. ;; ;; © Copyright 2020 Hendrik Tews ;; ;; Authors: Hendrik Tews ;; Maintainer: Hendrik Tews ;; ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;;; Commentary: ;; ;; Coq Compile Tests (cct) -- ;; ert tests for parallel background compilation for Coq ;; ;; This file contains common definitions for the automated tests of ;; parallel background compilation. ;; Require some libraries for the elisp compilation. When compiling, ;; nothing is loaded, but all Proof General directories are in the ;; load path. When this file is loaded as part of a test, proof-site ;; has been loaded but only the generic subdir is in the load path. ;; This file references variables from coq-compile-common and ;; functions from proof-shell, therefore coq-compile-common must be ;; required for compilation. When running a test, these files would be ;; loaded anyway when the test visits the first Coq file. For ;; executing tests, the coq subdir will only be added to the load path ;; when the first Coq file is visited. Therefore we have to add it ;; here via proof-ready-for-assistant. For compilation, we have to ;; require proof-site, otherwise proof-ready-for-assistant won't be ;; defined. (require 'proof-site) (proof-ready-for-assistant 'coq) (require 'coq-compile-common) (require 'ert) (defvar cct--debug-tests nil "Set to t to get more output during test runs.") (defmacro cct-implies (p q) "Short-circuit logical implication. Evaluate Q only if P is non-nil." `(or (not ,p) ,q)) (defun cct-list-subset (l1 l2) "Return t if all elements of L1 are in L2 (compared by `equal')" (let ((res t)) (while (and l1 res) (unless (member (pop l1) l2) (setq res nil))) res)) ;; Reimplementation of seq-set-equal-p for lists, because ;; seq-set-equal-p is not present before emacs 26. ;; XXX consider seq-set-equal-p when emacs 25 support is dropped. (defun cct-list-set-equal (l1 l2) "Return t if L1 and L2 contain the elements (compared by `equal')" (and (cct-list-subset l1 l2) (cct-list-subset l2 l1))) (defun cct-goto-line (line) "Put point on start of line LINE. Very similar to `goto-line', but the documentation of `goto-line' says, programs should use this piece of code." (goto-char (point-min)) (forward-line (1- line)) (cl-assert (eq (line-number-at-pos) line) nil "point not at required line in cct-goto-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 list of some of the keys of FILE-CHANGE-TIMES. 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." (let (out in) (dolist (file-time file-change-times (cons out in)) (if (member (car file-time) files) (push file-time in) (push file-time out))))) (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-process-to-line (line) "Assert/retract to line LINE and wait until processing completed." (when cct--debug-tests (message "assert/retrect to line %d in buffer %s" line (buffer-name))) (cct-goto-line line) (proof-goto-point) (while (or proof-second-action-list-active (consp proof-action-list)) ;; (message "wait for coq/compilation with %d items queued\n" ;; (length proof-action-list)) ;; ;; accept-process-output without timeout returns rather quickly, ;; apparently most times without process output or any other event ;; to process. (accept-process-output nil 0.1))) (defun cct-get-vanilla-span (line) "Get THE vanilla span for line LINE, report an error if there is none. PG uses a number of overlapping and non-overlapping spans (read overlays) in the asserted and queue region of the proof buffer, see the comments in generic/proof-script.el. Spans of type vanilla (stored at 'type in the span property list) are created for real commands (not for comments). They hold various information that is used, among others, for backtracking. This function returns the vanilla span that covers line LINE and reports a test failure if there is none or more than one vanilla spans." (let (spans) (cct-goto-line line) (setq spans (spans-filter (overlays-at (point)) 'type 'vanilla)) (should (eq (length spans) 1)) (car spans))) (defun cct-last-message-line () "Extract the last line from the *Messages* buffer. Useful if the message is not present in the echo area any more and `current-message' does not return anything." (with-current-buffer "*Messages*" (goto-char (point-max)) (forward-line -1) (buffer-substring (point) (- (point-max) 1)))) (defun cct-check-locked (line locked-state) "Check that line LINE has locked state LOCKED-STATE LOCKED-STATE must be 'locked or 'unlocked. This function checks whether line LINE is inside or outside the asserted (locked) region of the buffer and signals a test failure if not." (let ((locked (eq locked-state 'locked))) (when cct--debug-tests (message (concat "check lock state in buffer %s: line %d should be %s;\n" "\tlocked-span: %s ends at char %s in line %d") (buffer-name) line (if locked "locked" "unlocked") proof-locked-span (if (overlayp proof-locked-span) (span-end proof-locked-span) "") (if (overlayp proof-locked-span) (line-number-at-pos (span-end proof-locked-span)) ""))) (cl-assert (or locked (eq locked-state 'unlocked)) nil "test-check-locked 2nd argument wrong") (cct-goto-line line) (should (cct-implies locked (span-end proof-locked-span))) (should (or (and (not locked) (or (not proof-locked-span) (not (span-end proof-locked-span)))) (and (span-end proof-locked-span) (funcall (if locked '< '>) (point) (span-end proof-locked-span))))))) (defun cct-locked-ancestors (line ancestors) "Check that the vanilla span at line LINE has ANCESTORS recorded. The comparison treats ANCESTORS as set but the file names must be `equal' as strings. Ancestors are recoreded in the 'coq-locked-ancestors property of the vanilla spans of require commands, see the in-file documentation of coq/coq-par-compile.el." (let ((locked-ancestors (span-property (cct-get-vanilla-span line) 'coq-locked-ancestors))) (should (cct-list-set-equal 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)))) (when cct--debug-tests (message "file %s should be unchanged, recorded time: %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." (when cct--debug-tests (message "Files should be unchanged: %s" (mapconcat (lambda (file-time) (car file-time)) file-time-assoc ", "))) (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-generic-check-main-buffer (main-buf main-unlocked main-locked main-sum-line new-sum vo-times recompiled-files require-ancestors other-locked-files other-locked-line) "Perform various checks for recompilation in MAIN-BUF. MAIN-BUF is a buffer, MAIN-LOCKED and MAIN-SUM-line are line numbers in that buffer. NEW-SUM is a number as string. VO-TIMES is an association list of files and emacs times as returned by `cct-record-change-times' or `cct-split-change-times'. RECOMPILED-FILES is a list of some of the files in VO-TIMES. REQUIRE-ANCESTORS is a list of cons cells, each cons containing a line number in MAIN-BUF (which should contain a require) and a list of ancestor files that should get registered in the span of that require. OTHER-LOCKED-FILES is a list of buffers and OTHER-LOCKED-LINE is a common line number in those files. This function combines all the following tests in this order: - line MAIN-UNLOCKED in MAIN-BUF is unlocked - after replacing the sum on line MAIN-SUM-LINE with NEW-SUM, MAIN-BUF can be processed until line MAIN-LOCKED - 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 lines in REQUIRE-ANCESTORS have precisely the ancestors registered as specified in REQUIRE-ANCESTORS. - all the buffers in OTHER-LOCKED-FILES are locked until line OTHER-LOCKED-LINE." (let (splitted) (set-buffer main-buf) (cct-check-locked main-unlocked 'unlocked) (cct-replace-last-word main-sum-line new-sum) (cct-process-to-line (1+ main-locked)) (cct-check-locked main-locked 'locked) (setq splitted (cct-split-change-times vo-times recompiled-files)) ;; (message "check file dates, unmodified %s, modified %s" ;; (car splitted) (cdr splitted)) (cct-unmodified-change-times (car splitted)) (cct-older-change-times (cdr splitted)) (mapc (lambda (line-ancestors) (cct-locked-ancestors (car line-ancestors) (cdr line-ancestors))) require-ancestors) (mapc (lambda (b) (set-buffer b) (cct-check-locked other-locked-line 'locked)) other-locked-files))) (defun cct-configure-proof-general () "Configure Proof General for test execution." (setq delete-old-versions t coq-compile-before-require t coq-compile-keep-going t proof-auto-action-when-deactivating-scripting 'retract proof-three-window-enable nil coq-compile-auto-save 'save-coq coq--debug-auto-compilation nil ) (custom-set-variables '(coq-compile-quick 'ensure-vo)) (when (< coq--internal-max-jobs 4) (custom-set-variables '(coq-max-background-compilation-jobs 4))) (message "config coq-max-background-compilation-jobs: %s (means %d)" coq-max-background-compilation-jobs coq--internal-max-jobs)) (defun configure-delayed-coq () "Configure PG to honor artificial delays in background compilation. Configure Proof General to use coqdep-delayed and coqc-delayed from directory ../bin. These scripts delay the start of the real coqdep and coqc as specified in the Coq soure file, see ../bin/compile-test-start-delayed. This function uses relative file names and must be called in a test subdirectory parallel to the bin directory." (let ((bin-dir (file-truename "../bin"))) (add-to-list 'exec-path bin-dir) (setenv "PATH" (concat bin-dir ":" (getenv "PATH"))) (custom-set-variables '(coq-dependency-analyzer "coqdep-delayed") '(coq-compiler "coqc-delayed")))) (provide 'cct-lib)