From 12be85a9032ebed02d9b65da7848ab173081f41a Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 15 Dec 2020 21:54:53 +0100 Subject: include compile tests in CI elisp compilation --- Makefile | 32 ++- Makefile.devel | 2 +- ci/compile-tests/001-mini-project/Makefile | 4 +- ci/compile-tests/001-mini-project/runtest.el | 43 ++++ ci/compile-tests/001-mini-project/test.el | 40 ---- .../002-require-no-dependencies/Makefile | 4 +- .../002-require-no-dependencies/runtest.el | 48 +++++ .../002-require-no-dependencies/test.el | 45 ----- ci/compile-tests/003-require-error/Makefile | 4 +- ci/compile-tests/003-require-error/runtest.el | 45 +++++ ci/compile-tests/003-require-error/test.el | 42 ---- ci/compile-tests/004-dependency-cycle/Makefile | 4 +- ci/compile-tests/004-dependency-cycle/runtest.el | 61 ++++++ ci/compile-tests/004-dependency-cycle/test.el | 58 ------ ci/compile-tests/005-change-recompile/Makefile | 4 +- ci/compile-tests/005-change-recompile/runtest.el | 221 +++++++++++++++++++++ ci/compile-tests/005-change-recompile/test.el | 218 -------------------- ci/compile-tests/006-ready-dependee/Makefile | 4 +- ci/compile-tests/006-ready-dependee/runtest.el | 132 ++++++++++++ ci/compile-tests/006-ready-dependee/test.el | 130 ------------ ci/compile-tests/cct-lib.el | 26 ++- 21 files changed, 611 insertions(+), 556 deletions(-) create mode 100644 ci/compile-tests/001-mini-project/runtest.el delete mode 100644 ci/compile-tests/001-mini-project/test.el create mode 100644 ci/compile-tests/002-require-no-dependencies/runtest.el delete mode 100644 ci/compile-tests/002-require-no-dependencies/test.el create mode 100644 ci/compile-tests/003-require-error/runtest.el delete mode 100644 ci/compile-tests/003-require-error/test.el create mode 100644 ci/compile-tests/004-dependency-cycle/runtest.el delete mode 100644 ci/compile-tests/004-dependency-cycle/test.el create mode 100644 ci/compile-tests/005-change-recompile/runtest.el delete mode 100644 ci/compile-tests/005-change-recompile/test.el create mode 100644 ci/compile-tests/006-ready-dependee/runtest.el delete mode 100644 ci/compile-tests/006-ready-dependee/test.el diff --git a/Makefile b/Makefile index 3bc393ed..21aed373 100644 --- a/Makefile +++ b/Makefile @@ -33,10 +33,26 @@ EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; PREFIX=$(DESTDIR)/usr DEST_PREFIX=$(DESTDIR)/usr +# subdirectories for provers: to be compiled and installed PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf + +# generic lisp code: to be compiled and installed OTHER_ELISP=generic lib -ELISP_DIRS=${PROVERS} ${OTHER_ELISP} + +# additional lisp code: to be compiled but not installed +ADDITIONAL_ELISP:=ci/compile-tests \ + $(wildcard ci/compile-tests/[0-9][0-9][0-9]-*) + +# directories with lisp code to be installed +ELISP_DIRS_INST=${PROVERS} ${OTHER_ELISP} + +# directories with lisp code to be compiled (superset of ELISP_DIRS_INST +ELISP_DIRS_COMP=${ELISP_DIRS_INST} ${ADDITIONAL_ELISP} + +# to be installed ELISP_EXTRAS= + +# to be installed EXTRA_DIRS = images DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER doc/*.pdf @@ -54,11 +70,11 @@ BIN_SCRIPTS = lego/legotags coq/coqtags isar/isartags # Setting load path might be better in Elisp, but seems tricky to do # only during compilation. Another idea: put a function in proof-site -# to output the compile-time load path and ELISP_DIRS so these are set +# to output the compile-time load path and ELISP_DIRS_COMP so these are set # just in that one place. ERROR_ON_WARN = nil -BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (${ELISP_DIRS}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn $(ERROR_ON_WARN)))' -f batch-byte-compile -EL=$(shell for f in $(ELISP_DIRS); do ls $$f/*.el; done) +BYTECOMP = $(BATCHEMACS) -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (${ELISP_DIRS_COMP}))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))) (setq byte-compile-error-on-warn $(ERROR_ON_WARN)))' -f batch-byte-compile +EL=$(shell for f in $(ELISP_DIRS_COMP); do ls $$f/*.el; done) ELC=$(EL:.el=.elc) .SUFFIXES: .el .elc @@ -189,15 +205,15 @@ install-elisp: install-el install-elc # Should use install program or fix ownerships afterwards here. install-el: mkdir -p ${ELISP} - for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done - for f in ${ELISP_DIRS}; do cp -pf $$f/*.el ${ELISP}/$$f; done + for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done + for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.el ${ELISP}/$$f; done for f in ${EXTRA_DIRS}; do cp -prf $$f/* ${ELISP}/$$f; done for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done install-elc: compile mkdir -p ${ELISP} - for f in ${ELISP_DIRS} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done - for f in ${ELISP_DIRS}; do cp -pf $$f/*.elc ${ELISP}/$$f; done + for f in ${ELISP_DIRS_INST} ${EXTRA_DIRS}; do mkdir -p ${ELISP}/$$f; done + for f in ${ELISP_DIRS_INST}; do cp -pf $$f/*.elc ${ELISP}/$$f; done for f in ${ELISP_EXTRAS}; do cp -pf $$f ${ELISP}/$$f; done install-init: diff --git a/Makefile.devel b/Makefile.devel index d4339a46..8705af31 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -169,7 +169,7 @@ RELEASENAMEDMG = $(RELEASENAME).dmg # Where to install a distribution DISTINSTALLDIR=/usr/local/share/elisp/proofgeneral -SUBDIRS=$(ELISP_DIRS) etc doc images +SUBDIRS=$(ELISP_DIRS_COMP) etc doc images PWD=$(shell pwd) diff --git a/ci/compile-tests/001-mini-project/Makefile b/ci/compile-tests/001-mini-project/Makefile index 4ae0a433..95f05017 100644 --- a/ci/compile-tests/001-mini-project/Makefile +++ b/ci/compile-tests/001-mini-project/Makefile @@ -11,8 +11,8 @@ .PHONY: test test: $(MAKE) clean - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit .PHONY: clean clean: diff --git a/ci/compile-tests/001-mini-project/runtest.el b/ci/compile-tests/001-mini-project/runtest.el new file mode 100644 index 00000000..9edbcbd5 --- /dev/null +++ b/ci/compile-tests/001-mini-project/runtest.el @@ -0,0 +1,43 @@ +;; 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 +;; +;; Test that parallel background compilation works for a simple +;; project and that the right files are recorded for unlocking at the +;; right places. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a +;; / \ +;; b c +;; / \ / \ +;; d e f + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the test + +(ert-deftest cct-mini-project () + "Test successful background compilation and ancestor recording." + (find-file "a.v") + (cct-process-to-line 25) + + (cct-check-locked 24 'locked) + (cct-locked-ancestors 22 '("./b.v" "./d.v" "./e.v")) + (cct-locked-ancestors 23 '("./c.v" "./f.v"))) diff --git a/ci/compile-tests/001-mini-project/test.el b/ci/compile-tests/001-mini-project/test.el deleted file mode 100644 index 49cc91f7..00000000 --- a/ci/compile-tests/001-mini-project/test.el +++ /dev/null @@ -1,40 +0,0 @@ -;; 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 -;; -;; Test that parallel background compilation works for a simple -;; project and that the right files are recorded for unlocking at the -;; right places. -;; -;; The following graph shows the file dependencies in this test: -;; -;; a -;; / \ -;; b c -;; / \ / \ -;; d e f - - -;;; set configuration -(cct-configure-proof-general) - -;;; Define the test - -(ert-deftest cct-mini-project () - "Test successful background compilation and ancestor recording." - (find-file "a.v") - (cct-process-to-line 25) - - (cct-check-locked 24 'locked) - (cct-locked-ancestors 22 '("./b.v" "./d.v" "./e.v")) - (cct-locked-ancestors 23 '("./c.v" "./f.v"))) diff --git a/ci/compile-tests/002-require-no-dependencies/Makefile b/ci/compile-tests/002-require-no-dependencies/Makefile index 4ae0a433..95f05017 100644 --- a/ci/compile-tests/002-require-no-dependencies/Makefile +++ b/ci/compile-tests/002-require-no-dependencies/Makefile @@ -11,8 +11,8 @@ .PHONY: test test: $(MAKE) clean - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit .PHONY: clean clean: diff --git a/ci/compile-tests/002-require-no-dependencies/runtest.el b/ci/compile-tests/002-require-no-dependencies/runtest.el new file mode 100644 index 00000000..f2feefad --- /dev/null +++ b/ci/compile-tests/002-require-no-dependencies/runtest.el @@ -0,0 +1,48 @@ +;; 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 +;; +;; Test parallel background compilation when one require command does +;; not produce any dependencies. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a b +;; | +;; c + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the tests + +(ert-deftest cct-one-require-with-no-dependencies () + "Test background compilation with an require with no dependencies." + (find-file "a.v") + (cct-process-to-line 25) + + (cct-check-locked 24 'locked) + (cct-locked-ancestors 22 '())) + +(ert-deftest cct-two-requires-first-no-dependencies () + "Test background compilation with an require with no dependencies." + (find-file "b.v") + (cct-process-to-line 25) + + (cct-check-locked 24 'locked) + (cct-locked-ancestors 22 '()) + (cct-locked-ancestors 23 '("./c.v"))) diff --git a/ci/compile-tests/002-require-no-dependencies/test.el b/ci/compile-tests/002-require-no-dependencies/test.el deleted file mode 100644 index 69de9baa..00000000 --- a/ci/compile-tests/002-require-no-dependencies/test.el +++ /dev/null @@ -1,45 +0,0 @@ -;; 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 -;; -;; Test parallel background compilation when one require command does -;; not produce any dependencies. -;; -;; The following graph shows the file dependencies in this test: -;; -;; a b -;; | -;; c - - -;;; set configuration -(cct-configure-proof-general) - -;;; Define the tests - -(ert-deftest cct-one-require-with-no-dependencies () - "Test background compilation with an require with no dependencies." - (find-file "a.v") - (cct-process-to-line 25) - - (cct-check-locked 24 'locked) - (cct-locked-ancestors 22 '())) - -(ert-deftest cct-two-requires-first-no-dependencies () - "Test background compilation with an require with no dependencies." - (find-file "b.v") - (cct-process-to-line 25) - - (cct-check-locked 24 'locked) - (cct-locked-ancestors 22 '()) - (cct-locked-ancestors 23 '("./c.v"))) diff --git a/ci/compile-tests/003-require-error/Makefile b/ci/compile-tests/003-require-error/Makefile index 4ae0a433..95f05017 100644 --- a/ci/compile-tests/003-require-error/Makefile +++ b/ci/compile-tests/003-require-error/Makefile @@ -11,8 +11,8 @@ .PHONY: test test: $(MAKE) clean - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit .PHONY: clean clean: diff --git a/ci/compile-tests/003-require-error/runtest.el b/ci/compile-tests/003-require-error/runtest.el new file mode 100644 index 00000000..c5e2a713 --- /dev/null +++ b/ci/compile-tests/003-require-error/runtest.el @@ -0,0 +1,45 @@ +;; 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 +;; +;; Test parallel background compilation when coqdep fails on a require +;; command. +;; +;; The following graph shows the file dependencies in this test, where +;; X does not exist: +;; +;; a1 a2 a3 +;; | / \ / +;; b X c +;; +;; and where a1, a2 and a3 are the 3 require commands in file a.v + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the tests + +(ert-deftest cct-require-error () + "Test background compilation with an require that yields a coqdep error." + (let ((test-start-time (current-time))) + (find-file "a.v") + (cct-process-to-line 26) + + (cct-check-locked 22 'locked) + (cct-check-locked 23 'unlocked) + (cct-file-newer "b.vo" test-start-time) + (cct-file-newer "c.vo" test-start-time))) diff --git a/ci/compile-tests/003-require-error/test.el b/ci/compile-tests/003-require-error/test.el deleted file mode 100644 index 0a0dd3d4..00000000 --- a/ci/compile-tests/003-require-error/test.el +++ /dev/null @@ -1,42 +0,0 @@ -;; 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 -;; -;; Test parallel background compilation when coqdep fails on a require -;; command. -;; -;; The following graph shows the file dependencies in this test, where -;; X does not exist: -;; -;; a1 a2 a3 -;; | / \ / -;; b X c -;; -;; and where a1, a2 and a3 are the 3 require commands in file a.v - - -;;; set configuration -(cct-configure-proof-general) - -;;; Define the tests - -(ert-deftest cct-require-error () - "Test background compilation with an require that yields a coqdep error." - (let ((test-start-time (current-time))) - (find-file "a.v") - (cct-process-to-line 26) - - (cct-check-locked 22 'locked) - (cct-check-locked 23 'unlocked) - (cct-file-newer "b.vo" test-start-time) - (cct-file-newer "c.vo" test-start-time))) diff --git a/ci/compile-tests/004-dependency-cycle/Makefile b/ci/compile-tests/004-dependency-cycle/Makefile index 4ae0a433..95f05017 100644 --- a/ci/compile-tests/004-dependency-cycle/Makefile +++ b/ci/compile-tests/004-dependency-cycle/Makefile @@ -11,8 +11,8 @@ .PHONY: test test: $(MAKE) clean - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit .PHONY: clean clean: diff --git a/ci/compile-tests/004-dependency-cycle/runtest.el b/ci/compile-tests/004-dependency-cycle/runtest.el new file mode 100644 index 00000000..97d60fb5 --- /dev/null +++ b/ci/compile-tests/004-dependency-cycle/runtest.el @@ -0,0 +1,61 @@ +;; 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 +;; +;; Test parallel background compilation for a dependency cycle. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a1 a2 +;; / | +;; b<-e f +;; | | +;; c->d +;; +;; where a1 and a2 are the 2 require commands in file a.v. + + +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + +;;; set configuration +(cct-configure-proof-general) + +;;; Define the tests + +(ert-deftest cct-require-error () + "Test background compilation on cyclic dependencies." + (find-file "a.v") + (cct-process-to-line 25) + (let ((last-message (cct-last-message-line)) + message-cycle) + (should (equal "Coq compilation error: Circular dependency" + (substring last-message 0 42))) + + (should + (string-match + (concat + "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v -> " + "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v") + last-message)) + (setq message-cycle + (list (match-string 1 last-message) (match-string 2 last-message) + (match-string 3 last-message) (match-string 4 last-message))) + (should + (or (equal message-cycle '("b" "c" "d" "e")) + (equal message-cycle '("c" "d" "e" "b")) + (equal message-cycle '("d" "e" "b" "c")) + (equal message-cycle '("e" "b" "c" "d")))) + + (cct-check-locked 21 'locked) + (cct-check-locked 22 'unlocked))) diff --git a/ci/compile-tests/004-dependency-cycle/test.el b/ci/compile-tests/004-dependency-cycle/test.el deleted file mode 100644 index 5f9f63f3..00000000 --- a/ci/compile-tests/004-dependency-cycle/test.el +++ /dev/null @@ -1,58 +0,0 @@ -;; 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 -;; -;; Test parallel background compilation for a dependency cycle. -;; -;; The following graph shows the file dependencies in this test: -;; -;; a1 a2 -;; / | -;; b<-e f -;; | | -;; c->d -;; -;; where a1 and a2 are the 2 require commands in file a.v. - - -;;; set configuration -(cct-configure-proof-general) - -;;; Define the tests - -(ert-deftest cct-require-error () - "Test background compilation on cyclic dependencies." - (find-file "a.v") - (cct-process-to-line 25) - (let ((last-message (cct-last-message-line)) - message-cycle) - (should (equal "Coq compilation error: Circular dependency" - (substring last-message 0 42))) - - (should - (string-match - (concat - "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v -> " - "\\./\\([b-e]\\).v -> \\./\\([b-e]\\).v") - last-message)) - (setq message-cycle - (list (match-string 1 last-message) (match-string 2 last-message) - (match-string 3 last-message) (match-string 4 last-message))) - (should - (or (equal message-cycle '("b" "c" "d" "e")) - (equal message-cycle '("c" "d" "e" "b")) - (equal message-cycle '("d" "e" "b" "c")) - (equal message-cycle '("e" "b" "c" "d")))) - - (cct-check-locked 21 'locked) - (cct-check-locked 22 'unlocked))) diff --git a/ci/compile-tests/005-change-recompile/Makefile b/ci/compile-tests/005-change-recompile/Makefile index 983227be..4cdc6503 100644 --- a/ci/compile-tests/005-change-recompile/Makefile +++ b/ci/compile-tests/005-change-recompile/Makefile @@ -17,8 +17,8 @@ TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v test: $(MAKE) clean $(MAKE) $(TEST_SOURCES) - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit %.v: %.v.orig cp $< $@ 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 +;; +;; 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) + )) diff --git a/ci/compile-tests/005-change-recompile/test.el b/ci/compile-tests/005-change-recompile/test.el deleted file mode 100644 index 4bbc4f81..00000000 --- a/ci/compile-tests/005-change-recompile/test.el +++ /dev/null @@ -1,218 +0,0 @@ -;; 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 -;; -;; 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 -;; -;; -;; -;; -;; -;; -;; - -;;; 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) - )) diff --git a/ci/compile-tests/006-ready-dependee/Makefile b/ci/compile-tests/006-ready-dependee/Makefile index fe014bfc..eb622301 100644 --- a/ci/compile-tests/006-ready-dependee/Makefile +++ b/ci/compile-tests/006-ready-dependee/Makefile @@ -17,8 +17,8 @@ TEST_SOURCES:=a.v b.v c.v d.v e.v f.v g.v h.v i.v j.v k.v test: $(MAKE) clean $(MAKE) $(TEST_SOURCES) - emacs -batch -l ert -l ../../../generic/proof-site.el -l ../cct-lib.el \ - -l test.el -f ert-run-tests-batch-and-exit + emacs -batch -l ../../../generic/proof-site.el -l ../cct-lib.el \ + -l runtest.el -f ert-run-tests-batch-and-exit %.v: %.v.orig cp $< $@ diff --git a/ci/compile-tests/006-ready-dependee/runtest.el b/ci/compile-tests/006-ready-dependee/runtest.el new file mode 100644 index 00000000..9f4a2ce0 --- /dev/null +++ b/ci/compile-tests/006-ready-dependee/runtest.el @@ -0,0 +1,132 @@ +;; 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 +;; +;; Test recompilation and ancestor registration for the case a +;; dependency is in state ready already. +;; +;; The following graph shows the file dependencies in this test: +;; +;; a +;; / \ +;; b c +;; | |____________ +;; d \ +;; | | +;; e--f--g--h--i--j--k +;; +;; The idea is that the coqdep chain from b to j takes so long, that k +;; has been compiled and is in state ready before the coqdep results +;; from j are processed. This works - unless the disk cache is cold. +;; If it works the test triggers two bugs. First, k is locked with the +;; require command of c. Second, the modification time of k is not +;; propagated to j, such that the whole chain from j to b is not +;; recompiled after k has changed. + + +;; 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" "./e.v" "./f.v" "./g.v" + "./h.v" "./i.v" "./j.v" "./k.v") + "Ancestors of b.v.") + +(defconst c-ancestors '("./c.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 for a dependency in state ready." + ;;(setq coq--debug-auto-compilation t) + (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 "9" nil nil) + + ;; 3. change k and process again - everything should be compiled + (message "\n3. change k and process again - everything should be compiled\n") + (find-file "k.v") + (push "k.v" other-locked-files) + (cct-check-locked 21 'locked) + (cct-replace-last-word 21 "5") + (cct-check-main-buffer + vo-times "10" + '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./g.vo" + "./h.vo" "./i.vo" "./j.vo" "./k.vo") + other-locked-files) + )) diff --git a/ci/compile-tests/006-ready-dependee/test.el b/ci/compile-tests/006-ready-dependee/test.el deleted file mode 100644 index 7105c6e7..00000000 --- a/ci/compile-tests/006-ready-dependee/test.el +++ /dev/null @@ -1,130 +0,0 @@ -;; 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 -;; -;; Test recompilation and ancestor registration for the case a -;; dependency is in state ready already. -;; -;; The following graph shows the file dependencies in this test: -;; -;; a -;; / \ -;; b c -;; | |____________ -;; d \ -;; | | -;; e--f--g--h--i--j--k -;; -;; The idea is that the coqdep chain from b to j takes so long, that k -;; has been compiled and is in state ready before the coqdep results -;; from j are processed. This works - unless the disk cache is cold. -;; If it works the test triggers two bugs. First, k is locked with the -;; require command of c. Second, the modification time of k is not -;; propagated to j, such that the whole chain from j to b is not -;; recompiled after k has changed. - - -;;; set configuration -(cct-configure-proof-general) - -;;; Data and utility functions - -(defconst b-ancestors '("./b.v" "./d.v" "./e.v" "./f.v" "./g.v" - "./h.v" "./i.v" "./j.v" "./k.v") - "Ancestors of b.v.") - -(defconst c-ancestors '("./c.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 for a dependency in state ready." - ;; :expected-result :failed - ;;(setq coq--debug-auto-compilation t) - (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 "9" nil nil) - - ;; 3. change k and process again - everything should be compiled - (message "\n3. change k and process again - everything should be compiled\n") - (find-file "k.v") - (push "k.v" other-locked-files) - (cct-check-locked 21 'locked) - (cct-replace-last-word 21 "5") - (cct-check-main-buffer - vo-times "10" - '("./b.vo" "./c.vo" "./d.vo" "./e.vo" "./f.vo" "./g.vo" - "./h.vo" "./i.vo" "./j.vo" "./k.vo") - other-locked-files) - )) diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el index 532cd92a..1a10fc15 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -16,6 +16,27 @@ ;; 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) + +;; needed for seq-set-equal-p +(require 'seq) + (defmacro cct-implies (p q) "Short-circuit logical implication. @@ -97,8 +118,7 @@ reports a test failure if there is none or more than one vanilla spans." "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." - (save-excursion - (set-buffer "*Messages*") + (with-current-buffer "*Messages*" (goto-char (point-max)) (forward-line -1) (buffer-substring (point) (- (point-max) 1)))) @@ -193,3 +213,5 @@ or changed since recording the time in the association." proof-three-window-enable nil coq-compile-auto-save 'save-coq coq--debug-auto-compilation nil)) + +(provide 'cct-lib) -- cgit v1.2.3