Fix remaining uses of CL; Make files more declarative

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.

1 files changed, 18 insertions, 17 deletions

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)