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, 17 insertions, 17 deletions

diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index c6822dc5..ac2e82bf 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -35,7 +35,7 @@
 ;;; Code:
 
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
-
+(eval-when-compile (require 'cl-lib))
 (require 'coq-compile-common)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -712,7 +712,7 @@ function returns () if MODULE-ID comes from the standard library."
           ;;            error-message)))
           ;; (coq-seq-display-compile-response-buffer)
           (error error-message)))
-    (assert (<= (length result) 1)
+    (cl-assert (<= (length result) 1)
 	    nil "Internal error in coq-seq-map-module-id-to-obj-file")
     (car-safe result)))
 
@@ -949,7 +949,7 @@ errors are reported with an error message."
 
 (defun coq-par-run-vio2vo-queue ()
   "Start delayed vio2vo compilation."
-  (assert (not coq--last-compilation-job)
+  (cl-assert (not coq--last-compilation-job)
 	  nil "normal compilation and vio2vo in parallel 3")
   (setq coq--compile-vio2vo-in-progress t)
   (setq coq--compile-vio2vo-delay-timer nil)
@@ -1011,7 +1011,7 @@ somewhere after the last require command."
 
 (defun coq-par-add-queue-dependency (dependee dependant)
   "Add queue dependency from child job DEPENDEE to parent job DEPENDANT."
-  (assert (and (not (get dependant 'queue-dependant-waiting))
+  (cl-assert (and (not (get dependant 'queue-dependant-waiting))
 	       (not (get dependee 'queue-dependant)))
 	  nil "queue dependency cannot be added")
   (put dependant 'queue-dependant-waiting t)
@@ -1202,13 +1202,13 @@ when they transition from 'waiting-queue to 'ready:
 
 This function can safely be called for non-top-level jobs. This
 function must not be called for failed jobs."
-  (assert (not (get job 'failed))
+  (cl-assert (not (get job 'failed))
 	  nil "coq-par-retire-top-level-job precondition failed")
   (let ((span (get job 'require-span))
 	(items (get job 'queueitems)))
     (when (and span coq-lock-ancestors)
       (dolist (anc-job (get job 'ancestors))
-	(assert (not (eq (get anc-job 'lock-state) 'unlocked))
+	(cl-assert (not (eq (get anc-job 'lock-state) 'unlocked))
 		nil "bad ancestor lock state")
 	(when (eq (get anc-job 'lock-state) 'locked)
 	  (put anc-job 'lock-state 'asserted)
@@ -1290,7 +1290,7 @@ case, the following actions are taken:
       (let ((dependant (get job 'queue-dependant)))
 	(if dependant
 	    (progn
-	      (assert (not (eq coq--last-compilation-job job))
+	      (cl-assert (not (eq coq--last-compilation-job job))
 		      nil "coq--last-compilation-job invariant error")
 	      (put dependant 'queue-dependant-waiting nil)
 	      (when coq--debug-auto-compilation
@@ -1309,7 +1309,7 @@ case, the following actions are taken:
 		(proof-script-clear-queue-spans-on-error nil))
 	      (proof-release-lock)
 	      (when (eq coq-compile-quick 'quick-and-vio2vo)
-		(assert (not coq--compile-vio2vo-delay-timer)
+		(cl-assert (not coq--compile-vio2vo-delay-timer)
 			nil "vio2vo timer set before last compilation job")
 		(setq coq--compile-vio2vo-delay-timer
 		      (run-at-time coq-compile-vio2vo-delay nil
@@ -1362,7 +1362,7 @@ if it reaches 0, the next transition is triggered for DEPENDANT.
 For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
 'clone jobs this 'waiting-dep -> 'waiting-queue."
   ;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time)
-  (assert (eq (get dependant 'state) 'waiting-dep)
+  (cl-assert (eq (get dependant 'state) 'waiting-dep)
 	  nil "wrong state of parent dependant job")
   (when (coq-par-time-less (get dependant 'youngest-coqc-dependency)
 			   dependee-time)
@@ -1371,7 +1371,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
        (append dependee-ancestors (get dependant 'ancestors)))
   (put dependant 'coqc-dependency-count
        (1- (get dependant 'coqc-dependency-count)))
-  (assert (<= 0 (get dependant 'coqc-dependency-count))
+  (cl-assert (<= 0 (get dependant 'coqc-dependency-count))
 	  nil "dependency count below zero")
   (when coq--debug-auto-compilation
     (message "%s: coqc dependency count down to %d"
@@ -1439,7 +1439,7 @@ This function makes the following actions.
 		       "maybe kickoff queue")
 	       (get job 'name)
 	       (if dependant-alive "some" "no")))
-    (assert (or (not (get job 'failed)) (not dependant-alive))
+    (cl-assert (or (not (get job 'failed)) (not dependant-alive))
 	    nil "failed job with non-failing dependant")
     (when (or (and (not dependant-alive)
 		   (not (get job 'require-span))
@@ -1512,7 +1512,7 @@ coqdep or coqc are started for it."
 	 (get job 'required-obj-file))))
      ((eq job-state 'ready)
       (coq-par-start-vio2vo job))
-     (t (assert nil nil "coq-par-start-task with invalid job")))))
+     (t (cl-assert nil nil "coq-par-start-task with invalid job")))))
 
 (defun coq-par-start-jobs-until-full ()
   "Start background jobs until the limit is reached."
@@ -1622,7 +1622,7 @@ Return t if job has a direct or indirect dependant that has not
 failed yet and that is in a state before 'waiting-queue. Also,
 return t if JOB has a dependant that is a top-level job which has
 not yet failed."
-  (assert (not (eq (get job 'lock-state) 'asserted))
+  (cl-assert (not (eq (get job 'lock-state) 'asserted))
 	  nil "coq-par-ongoing-compilation precondition failed")
   (cond
    ((get job 'failed)
@@ -1653,7 +1653,7 @@ not yet failed."
 	(setq res (coq-par-ongoing-compilation dep)))
       res))
    (t
-    (assert nil nil
+    (cl-assert nil nil
 	    "impossible ancestor state %s on job %s"
 	    (get job 'state) (get job 'name)))))
 
@@ -1680,7 +1680,7 @@ Mark JOB with 'queue-failed, and, if JOB is in state
 appropriate."
   (unless (or (get job 'failed) (get job 'queue-failed))
     (put job 'queue-failed t)
-    (assert (not (eq (get job 'state) 'ready))
+    (cl-assert (not (eq (get job 'state) 'ready))
 	    nil "coq-par-mark-queue-failing impossible state")
     (when coq--debug-auto-compilation
       (message "%s: mark as queue-failed, %s"
@@ -1893,7 +1893,7 @@ there is no last compilation job."
     ;; add the asserted items to the last compilation job
     (if coq--last-compilation-job
 	(progn
-	  (assert (not (coq-par-job-is-ready coq--last-compilation-job))
+	  (cl-assert (not (coq-par-job-is-ready coq--last-compilation-job))
 		  nil "last compilation job from previous compilation ready")
 	  (put coq--last-compilation-job 'queueitems
 	       (nconc (get coq--last-compilation-job 'queueitems)
@@ -1979,7 +1979,7 @@ the maximal number of background compilation jobs is started."
 	(cancel-timer coq--compile-vio2vo-delay-timer)
 	(setq coq--compile-vio2vo-delay-timer nil))
       (when coq--compile-vio2vo-in-progress
-	(assert (not coq--last-compilation-job)
+	(cl-assert (not coq--last-compilation-job)
 		nil "normal compilation and vio2vo in parallel 2")
 	;; there are only vio2vo background processes
 	(coq-par-kill-all-processes)