From 9a25320acf24020fc0e2b97589f9d996f3d1d4fb Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Thu, 13 Dec 2018 22:57:15 -0500 Subject: Fix remaining uses of CL; Make files more declarative MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f), so loading a file should "no effect". Fix the most obvious such effects: the splash screen and the autotests by moving those effects into a function. * coq/coq-autotest.el: Make it declarative. Use lexical-binding. (coq-autotest): New function holding the code that used to be at top-level. * generic/proof.el: Use lexical-binding. Don't call proof-splash-message just because we're being loaded. * generic/proof-script.el: Use lexical-scoping; fix all warnings. (pg-show-all-portions): Simplify the code with a closure. (proof-activate-scripting): Declare activated-interactively as dyn-scoped. (proof--splash-done): New var. (proof-mode): Call proof-splash-message upon first use. * generic/proof-splash.el (proof-splash-message): Don't check byte-compile-current-file now that we're only called when the mode is activated. * acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'. * coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²). * coq/coq-seq-compile.el: * coq/coq-par-test.el: * coq/coq-par-compile.el: Fix leftover uses of CL's `assert`. * generic/proof-utils.el: * generic/pg-movie.el: * etc/testsuite/pg-test.el: * coq/coq-syntax.el: Fix leftover uses of CL's `incf`. * generic/pg-autotest.el: Fix leftover uses of CL's `decf`. * obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use of CL's `loop`. * generic/pg-user.el (proof-add-completions): Do nothing if no proof-assistant is set yet (i.e. during byte-compilation). (byte-compile-current-file): No need to test this any more. * generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat. Remove unnecessary "\\(?:...\\)". (proof-regexp-alt): Redefine in terms of proof-regexp-alt-list. --- coq/coq-par-test.el | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) (limited to 'coq/coq-par-test.el') diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el index ebc5ecd7..f2e3f01d 100644 --- a/coq/coq-par-test.el +++ b/coq/coq-par-test.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -31,6 +31,7 @@ ;;; Code: (require 'coq-par-compile) +(eval-when-compile (require 'cl-lib)) (defconst coq--par-job-needs-compilation-tests ;; for documentation see the doc string following the init value @@ -753,7 +754,7 @@ relative ages.") (lambda (test) (let ((test-id (format "%s" (car test)))) ;; a test is a list of 4 elements and the first element is a list itself - (assert + (cl-assert (and (eq (length test) 4) (listp (car test))) @@ -761,22 +762,22 @@ relative ages.") (mapc (lambda (variant) ;; a variant is a list of 4 elements - (assert (eq (length variant) 4) nil (concat test-id " 2")) + (cl-assert (eq (length variant) 4) nil (concat test-id " 2")) (let ((files (coq-par-test-flatten-files (car test))) (quick-mode (car variant)) (compilation-result (nth 1 variant)) (delete-result (nth 2 variant)) (req-obj-result (nth 3 variant))) ;; the delete field, when set, must be a member of the files list - (assert (or (not delete-result) + (cl-assert (or (not delete-result) (member delete-result files)) nil (concat test-id " 3")) ;; 8.4 compatibility check (when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo)) (not (member 'vio files))) - (assert (not delete-result) + (cl-assert (not delete-result) nil (concat test-id " 4")) - (assert (eq compilation-result + (cl-assert (eq compilation-result (not (eq (car (last (car test))) 'vo))) nil (concat test-id " 5"))))) (cdr test)))) @@ -789,7 +790,7 @@ relative ages.") ((eq sym 'dep) "dep.vo") ((eq sym 'vo) "a.vo") ((eq sym 'vio) "a.vio") - (t (assert nil))))) + (t (cl-assert nil))))) (concat dir "/" file))) (defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled) @@ -832,7 +833,7 @@ test the result and side effects wth `assert'." ;; different-counter (current-time)) (setq different-not-ok nil) (setq different-counter (1- different-counter)) - (assert (> different-counter 0) + (cl-assert (> different-counter 0) nil "create files with different time stamps failed") (dolist (same-descr file-descr) (when (symbolp same-descr) @@ -845,7 +846,7 @@ test the result and side effects wth `assert'." (setq same-not-ok t) (while same-not-ok (setq same-counter (1- same-counter)) - (assert (> same-counter 0) + (cl-assert (> same-counter 0) nil "create files with same time stamp filed") (dolist (file file-list) (with-temp-file file t)) @@ -875,40 +876,40 @@ test the result and side effects wth `assert'." (put job 'youngest-coqc-dependency 'just-compiled)) (setq result (coq-par-job-needs-compilation job)) ;; check result - (assert (eq result compilation-result) + (cl-assert (eq result compilation-result) nil (concat id " result")) ;; check file deletion - (assert (or (not delete-result) + (cl-assert (or (not delete-result) (not (file-attributes (test-coq-par-sym-to-file dir delete-result)))) nil (concat id " delete file")) ;; check no other file is deleted (dolist (f file-descr-flattened) (unless (eq f delete-result) - (assert (file-attributes (test-coq-par-sym-to-file dir f)) + (cl-assert (file-attributes (test-coq-par-sym-to-file dir f)) nil (format "%s non del file %s: %s" id f (test-coq-par-sym-to-file dir f))))) ;; check value of 'required-obj-file property - (assert (equal (get job 'required-obj-file) + (cl-assert (equal (get job 'required-obj-file) (test-coq-par-sym-to-file dir req-obj-result)) nil (concat id " required-obj-file")) ;; check 'obj-mod-time property (if obj-mod-result - (assert + (cl-assert (equal (get job 'obj-mod-time) (nth 5 (file-attributes (test-coq-par-sym-to-file dir obj-mod-result)))) nil (concat id " obj-mod-time non nil")) - (assert (not (get job 'obj-mod-time)) + (cl-assert (not (get job 'obj-mod-time)) nil (concat id " obj-mod-time nil"))) ;; check 'use-quick property - (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) + (cl-assert (eq (not (not (and compilation-result (eq req-obj-result 'vio)))) (get job 'use-quick)) nil (concat id " use-quick")) ;; check vio2vo-needed property - (assert (eq + (cl-assert (eq (and (eq quick-mode 'quick-and-vio2vo) (eq req-obj-result 'vio) (or (eq delete-result 'vo) -- cgit v1.2.3