From 9a25320acf24020fc0e2b97589f9d996f3d1d4fb Mon Sep 17 00:00:00 2001
From: Stefan Monnier <monnier@iro.umontreal.ca>
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.
---
 acl2/acl2.el                |  9 ++---
 coq/coq-autotest.el         |  6 ++-
 coq/coq-db.el               | 16 ++++----
 coq/coq-par-compile.el      | 34 ++++++++--------
 coq/coq-par-test.el         | 35 +++++++++--------
 coq/coq-seq-compile.el      |  5 ++-
 coq/coq-syntax.el           | 17 ++++----
 etc/testsuite/pg-test.el    |  8 ++--
 generic/pg-autotest.el      |  9 +++--
 generic/pg-movie.el         |  5 ++-
 generic/pg-user.el          | 16 ++++----
 generic/proof-script.el     | 96 +++++++++++++++++++++++----------------------
 generic/proof-splash.el     |  4 +-
 generic/proof-syntax.el     | 14 +++----
 generic/proof-useropts.el   |  4 +-
 generic/proof-utils.el      |  6 +--
 generic/proof.el            |  5 +--
 obsolete/plastic/plastic.el |  4 +-
 18 files changed, 147 insertions(+), 146 deletions(-)

diff --git a/acl2/acl2.el b/acl2/acl2.el
index cf9f521c..db3120ed 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.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
@@ -24,10 +24,9 @@
 (require 'proof-easy-config)            ; easy configure mechanism
 (require 'proof-syntax)			; functions for making regexps
 
-(setq auto-mode-alist                   ; ACL2 uses two file extensions
-      (cons				; Only grab .lisp extension after
-       (cons "\\.lisp$" 'acl2-mode)	; an acl2 file has been loaded
-       auto-mode-alist))
+(add-to-list 'auto-mode-alist                ; ACL2 uses two file extensions
+                                             ; Only grab .lisp extension after
+             (cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded
 
 (proof-easy-config  'acl2 "ACL2"
  proof-assistant-home-page       "http://www.cs.utexas.edu/users/moore/acl2"
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 8be4bed9..5ca66706 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,4 +1,4 @@
-;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress)  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -21,7 +21,9 @@
 (require 'proof-site)
 (defvar coq-compile-before-require)
 
-(unless (bound-and-true-p byte-compile-current-file)
+;;;###autoload
+(defun coq-autotest ()
+  (interactive)
 
   (pg-autotest start 'debug)
 
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 36812c4c..7e59bffb 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -25,7 +25,7 @@
 
 (eval-when-compile (require 'cl-lib))   ;decf
 
-(require 'proof-config)			; for proof-face-specs, a macro
+(require 'proof-config)
 (require 'proof-syntax)			; for proof-ids-to-regexp
 (require 'holes)
 
@@ -187,7 +187,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
   (let ((l db) (res ()) (size lgth)
 	(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
     (while (and l (> size 0))
-      (let* ((hd (car l))
+      (let* ((hd (pop l))
 	     (menu     	 (nth 0 hd)) ; e1 = menu entry
 	     (abbrev   	 (nth 1 hd)) ; e2 = abbreviation
 	     (complt   	 (nth 2 hd)) ; e3 = completion
@@ -209,10 +209,9 @@ Used by `coq-build-menu-from-db', which you should probably use instead.  See
 		  ;;insertion function if present otherwise insert completion
 		  (if insertfn insertfn `(holes-insert-and-expand ,complt))
 		  t)))
-	    (setq res (nconc res (list menu-entry)))));; append *in place*
-	(setq l (cdr l))
+	    (push menu-entry res)))
 	(cl-decf size)))
-    res))
+    (nreverse res)))
 
 
 (defun coq-build-title-menu (db size)
@@ -289,10 +288,9 @@ See `coq-syntax-db' for DB structure."
 
 ;;A new face for tactics which fail when they don't kill the current goal
 (defface coq-solve-tactics-face
-  (proof-face-specs
-   (:foreground "red") ; pour les fonds clairs
-   (:foreground "red1") ; pour les fonds foncés
-   ()) ; pour le noir et blanc
+  `((((background light)) :foreground "red")
+    (((background dark)) :foreground "red1")
+    ()) ; pour le noir et blanc
   "Face for names of closing tactics in proof scripts."
   :group 'proof-faces)
 
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)
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)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 4889ccaf..3cdcd02a 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -24,6 +24,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (defvar queueitems)       ; dynamic scope in p-s-extend-queue-hook
 
 (require 'coq-compile-common)
@@ -335,8 +336,8 @@ function returns () if MODULE-ID comes from the standard library."
           ;;            error-message)))
           ;; (coq-display-compile-response-buffer)
           (error error-message)))
-    (assert (<= (length result) 1)
-            "Internal error in coq-seq-map-module-id-to-obj-file")
+    (cl-assert (<= (length result) 1)
+               "Internal error in coq-seq-map-module-id-to-obj-file")
     (car-safe result)))
 
 (defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index bb32fc52..e1a9a7e3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.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
@@ -19,6 +19,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (require 'proof-syntax)
 (require 'proof-utils)                  ; proof-locate-executable
 (require 'coq-db)
@@ -509,12 +510,12 @@ so for the following reasons:
   )
 
 ;; modules and section are indented like goal starters
-;;; PC TODO: this category is used only for indentation, because
-;;; scripting uses information from coq to decide if a goal is
-;;; started. Since it is impossible for some commands to know
-;;; syntactically if they start something (ex: Instance), the
-;;; right thing to do would be to indent only on "Proof." and forget
-;;; about this category for indentation.
+;; PC TODO: this category is used only for indentation, because
+;; scripting uses information from coq to decide if a goal is
+;; started. Since it is impossible for some commands to know
+;; syntactically if they start something (ex: Instance), the
+;; right thing to do would be to indent only on "Proof." and forget
+;; about this category for indentation.
 
 (defvar coq-goal-starters-db
   '(
@@ -991,7 +992,7 @@ so for the following reasons:
 Empty matches are counted once."
   (let ((nbmatch 0) (str strg))
     (while (and (proof-string-match regexp str) (not (string-equal str "")))
-      (incf nbmatch)
+      (cl-incf nbmatch)
       (if (= (match-end 0) 0) (setq str (substring str 1))
         (setq str (substring str (match-end 0)))))
     nbmatch))
diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el
index 2e3c2c10..2c064827 100644
--- a/etc/testsuite/pg-test.el
+++ b/etc/testsuite/pg-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
@@ -14,6 +14,8 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
+
 (defconst pg-test-buffer "** PG test output **")
 
 (defvar pg-test-total-success-count  0)
@@ -68,8 +70,8 @@
 		  (format " %s failed: exprected result %s, got %s\n"
 			  name goodresult result))))
       (if errorresult
-	  (incf pg-test-suite-fail-count)
-	(incf pg-test-suite-success-count)
+	  (cl-incf pg-test-suite-fail-count)
+	(cl-incf pg-test-suite-success-count)
 	(setq errorresult (format " %s succeeded.\n" name)))
       ;; Return string
       errorresult))
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index e7cb19a9..7a22c9f7 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.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
@@ -25,6 +25,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 (require 'proof-splash)
 (setq proof-splash-enable nil)		; prevent splash when testing
 
@@ -215,7 +216,7 @@ completely processing the buffer as the last step."
 	 " random jump: processing whole buffer")
 	(proof-process-buffer)
 	(proof-shell-wait)
-	(decf jumps))
+	(cl-decf jumps))
 
 	((and (eq random-thing 1)
 	      (not (proof-locked-region-empty-p)))
@@ -223,7 +224,7 @@ completely processing the buffer as the last step."
 	  " random jump: retracting whole buffer")
 	 (proof-retract-buffer)
 	 (proof-shell-wait)
-	 (decf jumps))
+	 (cl-decf jumps))
 
 	(t
 	 (pg-autotest-message
@@ -241,7 +242,7 @@ completely processing the buffer as the last step."
 		    " random jump: interrupting prover")
 		   (proof-interrupt-process)))
 	     (proof-shell-wait))
-	   (decf jumps)))))
+	   (cl-decf jumps)))))
   (unless (proof-locked-region-full-p)
     (proof-process-buffer)
     (proof-shell-wait))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 9be95972..755d41f5 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.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
@@ -30,6 +30,7 @@
 ;;
 
 ;;; Code:
+(eval-when-compile (require 'cl-lib))
 (eval-when-compile
   (require 'span)
   (require 'unicode-tokens))
@@ -72,7 +73,7 @@
 		    (t "command")))
 	 (label    (span-property span 'rawname))
 	 (frameid  (int-to-string pg-movie-frame)))
-    (incf pg-movie-frame)
+    (cl-incf pg-movie-frame)
     (pg-xml-node frame
 		 (list (pg-xml-attr frameNumber frameid))
 		 (list
diff --git a/generic/pg-user.el b/generic/pg-user.el
index a5ed27a9..57d29f18 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -558,18 +558,18 @@ last use time, to discourage saving these into the users database."
   (defvar completion-min-length)
   (declare-function add-completion "completion"
                     (string &optional num-uses last-use-time))
-  (mapcar (lambda (cmpl)
-	    ;; completion gives error; trapping is tricky so test again
-	    (if (>= (length cmpl) completion-min-length)
-		(add-completion cmpl -1000 0)))
-	  (proof-ass completion-table)))
+  (when proof-assistant
+    (mapcar (lambda (cmpl)
+	      ;; completion gives error; trapping is tricky so test again
+	      (if (>= (length cmpl) completion-min-length)
+		  (add-completion cmpl -1000 0)))
+	    (proof-ass completion-table))))
 
 ;; NB: completion table is expected to be set when proof-script
 ;; is loaded!  Call `proof-script-add-completions' to update.
 
-(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck!
-  (eval-after-load "completion"
-    '(proof-add-completions)))
+(eval-after-load "completion"
+  '(proof-add-completions))
 
 (defun proof-script-complete (&optional arg)
   "Like `complete' but case-fold-search set to `proof-case-fold-search'."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4c56fc7b..f8cf0cab 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,4 +1,4 @@
-;;; proof-script.el --- Major mode for proof assistant script files.
+;;; proof-script.el --- Major mode for proof assistant script files.  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -42,6 +42,7 @@
 (declare-function proof-segment-up-to "proof-script")
 (declare-function proof-autosend-enable "pg-user")
 (declare-function proof-interrupt-process "pg-shell")
+(declare-function proof-cd-sync "pg-user" ())
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -142,7 +143,7 @@ scripting buffer may have an active queue span.")
 
 ;; ** Getters and setters
 
-(defun proof-span-give-warning (&rest args)
+(defun proof-span-give-warning (&rest _args)
   "Give a warning message.
 Optional argument ARGS is ignored."
   (unless inhibit-read-only
@@ -506,7 +507,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
 (defun pg-clear-script-portions ()
   "Clear record of script portion names and types from internal list."
   (dolist (idtbl pg-script-portions)
-    (maphash (lambda (k span) (span-delete span)) (cdr idtbl))
+    (maphash (lambda (_k span) (span-delete span)) (cdr idtbl))
     (clrhash (cdr idtbl))))
 
 (defun pg-remove-element (idiom id)
@@ -628,14 +629,11 @@ IDIOMSYM is a symbol and ID is a strings."
       (concat "Make "
 	      (if current-prefix-arg "in" "")
 	      "visible all regions of: ")
-      (apply 'vector pg-idioms) nil t))
+      (apply #'vector pg-idioms) nil t))
     current-prefix-arg))
   (let ((elts    (cdr-safe (assq idiom pg-script-portions)))
-	(alterfn (if hide
-		     (lambda (k span)
-		       (pg-set-element-span-invisible span t))
-		   (lambda (k span)
-		     (pg-set-element-span-invisible span nil)))))
+	(alterfn (lambda (_k span)
+		   (pg-set-element-span-invisible span hide))))
     (when elts
       (proof-with-script-buffer ; may be called from menu
        (maphash alterfn elts)))))
@@ -668,7 +666,6 @@ Each span has a 'type property, one of:
     'pbp	  A PBP command inserted automatically into the script."
   (let ((type    (span-property span 'type))
 	(idiom   (span-property span 'idiom))
-	(name    (span-property span 'name))
 	(rawname (span-property span 'rawname)))
     (cond
      (idiom
@@ -1213,10 +1210,10 @@ activation is considered to have failed and an error is given."
       ;; If there's another buffer currently active, we need to
       ;; deactivate it (also fixing up the included files list).
       (when proof-script-buffer
-	    (proof-deactivate-scripting)
-	    ;; Test whether deactivation worked
-	    (if proof-script-buffer
-		(error
+	(proof-deactivate-scripting)
+	;; Test whether deactivation worked
+	(if proof-script-buffer
+	    (error
 	     "You cannot have more than one active scripting buffer!")))
 
       ;; Ensure this buffer is off the included files list.  If we
@@ -1265,21 +1262,21 @@ activation is considered to have failed and an error is given."
       ;; block.  NB: The hook function may send commands to the
       ;; process which will re-enter this function, but should exit
       ;; immediately because scripting has been turned on now.
-      (if proof-activate-scripting-hook
-	  (let
-	      ((activated-interactively	(called-interactively-p 'any)))
-	    (setq proof-shell-last-output-kind nil)
-	    (run-hooks 'proof-activate-scripting-hook)
-	    ;; If activate scripting functions caused an error,
-	    ;; prevent switching to another buffer.  Might be better
-	    ;; to leave to specific instances, or simply run the hooks
-	    ;; as the last step before turning on scripting properly.
-	    (when (or (eq 'error proof-shell-last-output-kind)
-		      (eq 'interrupt proof-shell-last-output-kind))
-	      (proof-deactivate-scripting) ;; turn off again!
-	      ;; Give an error to prevent further actions.
-	      (error
-	       "Scripting not activated because of error or interrupt")))))))
+      (when proof-activate-scripting-hook
+        (defvar activated-interactively)
+	(let ((activated-interactively (called-interactively-p 'any)))
+	  (setq proof-shell-last-output-kind nil)
+	  (run-hooks 'proof-activate-scripting-hook)
+	  ;; If activate scripting functions caused an error,
+	  ;; prevent switching to another buffer.  Might be better
+	  ;; to leave to specific instances, or simply run the hooks
+	  ;; as the last step before turning on scripting properly.
+	  (when (or (eq 'error proof-shell-last-output-kind)
+		    (eq 'interrupt proof-shell-last-output-kind))
+	    (proof-deactivate-scripting) ;; turn off again!
+	    ;; Give an error to prevent further actions.
+	    (error
+	     "Scripting not activated because of error or interrupt")))))))
 
 
 (defun proof-toggle-active-scripting (&optional arg)
@@ -1415,7 +1412,8 @@ Argument SPAN has just been processed."
 						(span-end span)))
       (if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str)
 	  (condition-case nil
-	      (eval (car (read-from-string (match-string-no-properties 1 str))))
+	      (eval (car (read-from-string (match-string-no-properties 1 str)))
+                    t)
 	    (t (proof-debug
 		(concat
 		 "lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n"
@@ -1599,7 +1597,7 @@ Subroutine of `proof-done-advancing-save'."
       ;; start of the buffer, we make a fake goal-save region.
 
       ;; Delete spans between the previous goal and new command
-      (mapc 'span-delete dels)
+      (mapc #'span-delete dels)
 
       ;; Try to set the name from the goal... [as above]
       (setq nam (or (proof-get-name-from-goal gspan)
@@ -1643,7 +1641,7 @@ Subroutine of `proof-done-advancing-save'."
 ;; command syntax (terminated, not terminated, or lisp-style), whether
 ;; or not PG silently ignores comments, etc.
 
-(defun proof-segment-up-to-parser (pos &optional next-command-end)
+(defun proof-segment-up-to-parser (pos &optional _next-command-end)
   "Parse the script buffer from end of queue/locked region to POS.
 This partitions the script buffer into contiguous regions, classifying
 them by type.  Return a list of lists of the form
@@ -1838,7 +1836,7 @@ The optional QUEUEFLAGS are added to each queue item."
   (let ((start (proof-queue-or-locked-end))
 	(file  (or (buffer-file-name) (buffer-name)))
 	(cb    'proof-done-advancing)
-	span alist semi item end)
+	span alist end)
     (setq semis (nreverse semis))
     (save-match-data
       (dolist (semi semis)
@@ -1927,7 +1925,7 @@ always defaults to inserting a semi (nicer might be to parse for a
 comment, and insert or skip to the next semi)."
   (let ((mrk         (point))
 	(termregexp  (regexp-quote proof-terminal-string))
-	ins incomment nwsp)
+	ins nwsp)
     (if (< mrk (proof-unprocessed-begin))
 	(insert proof-terminal-string) ; insert immediately in locked region
       (if (proof-only-whitespace-to-locked-region-p)
@@ -1953,7 +1951,6 @@ comment, and insert or skip to the next semi)."
 	(unless semis
 	  (error "Can't find a parseable command!"))
 	(when (eq 'unclosed-comment (caar semis))
-	  (setq incomment t)
 	  ;; delete spurious char in comment
 	  (if ins (backward-delete-char 1))
 	  (goto-char mrk)
@@ -2258,17 +2255,22 @@ query saves here."
 ;; Proof General scripting mode definition, part 1.
 ;;
 
+(defvar proof--splash-done nil)
+
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode
   proof-general-name
   "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
 
+  (unless (or proof--splash-done noninteractive)
+    (setq proof--splash-done t)
+    (proof-splash-message))
+
   (setq proof-buffer-type 'script)
 
   ;; Set default indent function (can be overriden in derived modes)
-  (make-local-variable 'indent-line-function)
-  (setq indent-line-function 'proof-indent-line)
+  (setq-local indent-line-function #'proof-indent-line)
 
   ;; During write-file it can happen that we re-set the mode for the
   ;; currently active scripting buffer.  The user might also do this
@@ -2286,9 +2288,9 @@ query saves here."
   (proof-script-set-after-change-functions)
 
   (add-hook 'after-set-visited-file-name-hooks
-	    'proof-script-set-visited-file-name nil t)
+	    #'proof-script-set-visited-file-name nil t)
 
-  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+  (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
 
 ;; NB: proof-mode-map declared above
 (proof-menu-define-keys proof-mode-map)
@@ -2321,9 +2323,9 @@ This hook also gives a warning in case this is the active scripting buffer."
   "Set the hooks for a proof script buffer.
 The hooks set here are cleared by `write-file', so we use this function
 to restore them using `after-set-visited-file-name-hooks'."
-  (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
+  (add-hook 'kill-buffer-hook #'proof-script-kill-buffer-fn t t)
   ;; Reverting buffer is same as killing it as far as PG is concerned
-  (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t))
+  (add-hook 'before-revert-hook #'proof-script-kill-buffer-fn t t))
 
 (defun proof-script-kill-buffer-fn ()
   "Value of `kill-buffer-hook' for proof script buffers.
@@ -2616,17 +2618,17 @@ finish setup which depends on specific proof assistant configuration."
   "Choose parsing mechanism according to different kinds of script syntax.
 Choice of function depends on configuration setting."
   (unless (fboundp 'proof-segment-up-to)
-    (defalias 'proof-segment-up-to 'proof-segment-up-to-parser)
+    (defalias 'proof-segment-up-to #'proof-segment-up-to-parser)
     (cond
      (proof-script-parse-function
       ;; already set, nothing to do
       )
      (proof-script-sexp-commands
-      (setq proof-script-parse-function 'proof-script-generic-parse-sexp))
+      (setq proof-script-parse-function #'proof-script-generic-parse-sexp))
      (proof-script-command-start-regexp
-      (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart))
+      (setq proof-script-parse-function #'proof-script-generic-parse-cmdstart))
      ((or proof-script-command-end-regexp proof-terminal-string)
-      (setq  proof-script-parse-function 'proof-script-generic-parse-cmdend)
+      (setq  proof-script-parse-function #'proof-script-generic-parse-cmdend)
       (unless proof-script-command-end-regexp
 	(proof-warn-if-unset "probof-config-done" 'proof-terminal-string)
 	(setq proof-script-command-end-regexp
@@ -2726,7 +2728,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 		  (cdr semis))))
       usedsemis)))
 
-(defun proof-script-after-change-function (start end prelength)
+(defun proof-script-after-change-function (start _end _prelength)
   "Value for `after-change-functions' in proof script buffers."
   (setq proof-last-edited-low-watermark
 	(min (or proof-last-edited-low-watermark (point-max))
@@ -2741,7 +2743,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
 (defun proof-script-set-after-change-functions ()
   "Set `after-change-functions' for script buffers."
   (add-hook 'after-change-functions
-	    'proof-script-after-change-function nil t))
+	    #'proof-script-after-change-function nil t))
 
 
 
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 75164890..600e9b4e 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.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
@@ -270,7 +270,7 @@ binding to remove this buffer."
 (defun proof-splash-message ()
   "Make sure the user gets welcomed one way or another."
   (interactive)
-  (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
+  (unless (or proof-splash-seen noninteractive)
     (if proof-splash-enable
 	(progn
 	  ;; disable ordinary emacs splash
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index e93f5ca4..d494279a 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -36,18 +36,14 @@ Uses a regexp of the form \\_<...\\_>."
 (defconst proof-no-regexp "\\<\\>"
   "A regular expression that never matches anything.")
 
-(defsubst proof-regexp-alt (&rest args)
+(defsubst proof-regexp-alt-list (args)
   "Return the regexp which matches any of the regexps ARGS."
-  ;; see regexp-opt (NB: but that is for strings, not regexps)
-  (let ((res ""))
-    (dolist (regexp args)
-      (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:")
-			regexp "\\)")))
-    res))
+  (mapconcat #'identity args "\\|"))
 
-(defsubst proof-regexp-alt-list (args)
+(defsubst proof-regexp-alt (&rest args)
   "Return the regexp which matches any of the regexps ARGS."
-  (apply 'proof-regexp-alt args))
+  ;; see regexp-opt (NB: but that is for strings, not regexps)
+  (proof-regexp-alt-list args))
 
 (defsubst proof-re-search-forward-region (startre endre)
   "Search for a region delimited by regexps STARTRE and ENDRE.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 9a60e0ac..4ce51c99 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.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
@@ -50,7 +50,7 @@ approximation we test whether proof-config is fully-loaded yet."
   (set-default sym value)
   (when (and
 	 (not noninteractive)
-	 (not (bound-and-true-p byte-compile-current-file))
+	 (not (bound-and-true-p byte-compile-current-file)) ;FIXME: Yuck!
 	 (featurep 'pg-custom)
 	 (featurep 'proof-config))
       (if (fboundp sym)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 99e537c5..1568b2f0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -23,6 +23,7 @@
 
 ;;; Code:
 
+(eval-when-compile (require 'cl-lib))
 ;;
 ;; Give Emacs version mismatch error here.
 ;;
@@ -58,8 +59,6 @@
 (require 'proof-autoloads)		; interface fns
 (require 'scomint)			; for proof-shell-live-buffer
 
-;;; Code:
-
 ;;
 ;; Handy macros
 ;;
@@ -247,7 +246,8 @@ Experimentally we display a message from time to time advertising
   ;; IF there *isn't* a visible window showing buffer...
   (unless (get-buffer-window buffer 0)
     (if proof-three-window-enable
-        (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count)
+        (if (< proof-advertise-layout-count 30)
+            (cl-incf proof-advertise-layout-count)
           (message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout"))
           (setq proof-advertise-layout-count 0)))
     ;; THEN either we are in 2 wins mode and we must switch the assoc
diff --git a/generic/proof.el b/generic/proof.el
index f3b3b276..769459df 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;;; proof.el --- Proof General theorem prover interface
+;;; proof.el --- Proof General theorem prover interface  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -33,9 +33,6 @@
 
 (require 'proof-site)			; site/prover config, global vars, autoloads
 
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
-  (proof-splash-message))		; welcome the user now.
-
 (require 'proof-utils)			; utilities
 (require 'proof-config)			; configuration variables
 (require 'proof-auxmodes)		; auxmode functions
diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
index cf69a731..39f6c01f 100644
--- a/obsolete/plastic/plastic.el
+++ b/obsolete/plastic/plastic.el
@@ -546,8 +546,8 @@ For Plastic, we assume that module identifiers coincide with file names."
 		      (aset string i ?\ )
 		      (cl-incf i) )))
 	(keep-rest (lambda ()
-		     (loop for x in (string-to-list plastic-lit-string)
-		       do (aset string i ?\ ) (cl-incf i))
+		     (cl-loop for x in (string-to-list plastic-lit-string)
+		              do (aset string i ?\ ) (cl-incf i))
 		     (while (and (< i l)
 				 (/= (aref string i) ?\n)
 				 (/= (aref string i) ?-))
-- 
cgit v1.2.3