diff options
15 files changed, 79 insertions, 24 deletions
@@ -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/test.el b/ci/compile-tests/001-mini-project/runtest.el index 49cc91f7..9edbcbd5 100644 --- a/ci/compile-tests/001-mini-project/test.el +++ b/ci/compile-tests/001-mini-project/runtest.el @@ -25,6 +25,9 @@ ;; d e f +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + ;;; set configuration (cct-configure-proof-general) 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/test.el b/ci/compile-tests/002-require-no-dependencies/runtest.el index 69de9baa..f2feefad 100644 --- a/ci/compile-tests/002-require-no-dependencies/test.el +++ b/ci/compile-tests/002-require-no-dependencies/runtest.el @@ -22,6 +22,9 @@ ;; c +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + ;;; set configuration (cct-configure-proof-general) 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/test.el b/ci/compile-tests/003-require-error/runtest.el index 0a0dd3d4..c5e2a713 100644 --- a/ci/compile-tests/003-require-error/test.el +++ b/ci/compile-tests/003-require-error/runtest.el @@ -25,6 +25,9 @@ ;; 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) 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/test.el b/ci/compile-tests/004-dependency-cycle/runtest.el index 5f9f63f3..97d60fb5 100644 --- a/ci/compile-tests/004-dependency-cycle/test.el +++ b/ci/compile-tests/004-dependency-cycle/runtest.el @@ -25,6 +25,9 @@ ;; 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) 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/test.el b/ci/compile-tests/005-change-recompile/runtest.el index 4bbc4f81..c5d7f9b3 100644 --- a/ci/compile-tests/005-change-recompile/test.el +++ b/ci/compile-tests/005-change-recompile/runtest.el @@ -35,6 +35,9 @@ ;; ;; +;; require cct-lib for the elisp compilation, otherwise this is present already +(require 'cct-lib) + ;;; set configuration (cct-configure-proof-general) 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/test.el b/ci/compile-tests/006-ready-dependee/runtest.el index 7105c6e7..9f4a2ce0 100644 --- a/ci/compile-tests/006-ready-dependee/test.el +++ b/ci/compile-tests/006-ready-dependee/runtest.el @@ -34,6 +34,9 @@ ;; 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) @@ -97,7 +100,6 @@ Combine all the following tests in this order: (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") 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) |