Avoid a possibly-undefined function in acl2-doc. Avoid ACL2 customiza…

…tion file in "make DOC".

Changed code in acl2-doc to avoid the use of function cl-position,
which isn't available in every reasonable Emacs.  Thanks to Eric Smith
for reporting this problem.

Quoting :doc note-7-4:

  An ACL2 customization file is no longer loaded by default (when it
  exists) when invoking `make' from the top-level ACL2 directory.
  This change is not necessary for `make regression' because the
  build system for the books already takes care of it. However we
  need this change for `make DOC', at the least; thanks to Eric Smith
  for bringing our attention to a failure of `make DOC'.

GNUmakefile

@@ -105,6 +105,11 @@
 #  option below.  If you want to get rid of the metering in the
 #  compiled code, do make full.
 
+# Avoid loading the ACL2 customization file.  This is already done by
+# the books build system; however we need this for "make DOC" and
+# perhaps other targets.
+export ACL2_CUSTOMIZATION ?= NONE
+
 # Avoid escape characters in regression log:
 export CERT_PL_NO_COLOR ?= t
 

books/system/doc/acl2-doc.lisp

@@ -75151,6 +75151,13 @@ it."
 
  <h3>Changes at the System Level</h3>
 
+ <p>An ACL2 customization file is no longer loaded by default (when it exists)
+ when invoking `@('make')' from the top-level ACL2 directory.  This change is
+ not necessary for `@('make regression')' because the build system for the
+ books already takes care of it.  However we need this change for `@('make
+ DOC')', at the least; thanks to Eric Smith for bringing our attention to a
+ failure of `@('make DOC')'.</p>
+
  <h3>EMACS Support</h3>
 
  <p>Made minor @(see acl2-doc) improvements: fixed a bug in `@('u')' command's

doc.lisp

@@ -73777,6 +73777,13 @@ Bug Fixes
 
 Changes at the System Level
 
+  An ACL2 customization file is no longer loaded by default (when it
+  exists) when invoking `make' from the top-level ACL2 directory.
+  This change is not necessary for `make regression' because the
+  build system for the books already takes care of it. However we
+  need this change for `make DOC', at the least; thanks to Eric Smith
+  for bringing our attention to a failure of `make DOC'.
+
 
 EMACS Support
 

emacs/acl2-doc.el

@@ -118,14 +118,31 @@
 ; not smashed by invoking that macro after running acl2-doc-alist-create.
 (defv *acl2-doc-directory* nil)
 
+(defun my-cl-position (ch str)
+
+;;; We include this simple variant of cl-position because it is not
+;;; available in some versions of emacs (we have had a report of this
+;;; problem for GNU Emacs 24.3.1 on redhat).
+
+  (let ((continue t)
+	(pos 0)
+	(len (length str))
+	(ans))
+    (while (and continue (< pos len))
+      (when (eql (aref str pos) ch)
+	(setq ans pos)
+	(setq continue nil))
+      (setq pos (1+ pos)))
+    ans))
+
 (defun acl2-doc-fix-symbol (sym)
 
 ;;; Since Emacs Lisp doesn't seem to use |..| for escaping, we simply
 ;;; remove those vertical bars that seem to have been placed by Common
 ;;; Lisp.
 
   (let* ((name (symbol-name sym))
-	 (pos (cl-position ?| name)))
+	 (pos (my-cl-position ?| name)))
     (cond ((null pos)			; common case
 	   sym)
 	  (t (let ((max (1- (length name))))