Fix checkdoc warnings

Makefile

@@ -143,6 +143,14 @@ check-doc-magic:
 	+$(MAKE) -C doc magic
 	git diff --exit-code -- doc
 
+##
+## checkdoc : check the docstrings using the Emacs builtin checkdoc utility
+##
+.PHONY: checkdoc
+checkdoc: $(EL)
+	@$(EMACS) -Q --batch -l resources/checkdoc-config.el \
+	  $(foreach file,$^,"--eval=(checkdoc-file \"$(file)\")")
+
 ##
 ## Make an individual .elc.  Building separately means we need to be
 ## careful to add proper requires in source files and prevent

ci/compile-tests/001-mini-project/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;; 
 ;; © Copyright 2020  Hendrik Tews
 ;; 
@@ -24,6 +26,7 @@
 ;;        / \ / \
 ;;       d   e   f
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -42,3 +45,7 @@
   (cct-check-locked 24 'locked)
   (cct-locked-ancestors 22 '("./b.v" "./d.v" "./e.v"))
   (cct-locked-ancestors 23 '("./c.v" "./f.v")))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/002-require-no-dependencies/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;; 
 ;; © Copyright 2020  Hendrik Tews
 ;; 
@@ -21,6 +23,7 @@
 ;;           |
 ;;           c
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -46,3 +49,7 @@
   (cct-check-locked 24 'locked)
   (cct-locked-ancestors 22 '())
   (cct-locked-ancestors 23 '("./c.v")))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/003-require-error/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;;
 ;; © Copyright 2020  Hendrik Tews
 ;;
@@ -24,6 +26,7 @@
 ;;
 ;; and where a1, a2 and a3 are the 3 require commands in file a.v
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -43,3 +46,7 @@
     (cct-check-locked 23 'unlocked)
     (cct-file-newer "b.vo" test-start-time)
     (cct-file-newer "c.vo" test-start-time)))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/004-dependency-cycle/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;;
 ;; © Copyright 2020  Hendrik Tews
 ;;
@@ -24,6 +26,7 @@
 ;;
 ;; where a1 and a2 are the 2 require commands in file a.v.
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -59,3 +62,7 @@
 
     (cct-check-locked 21 'locked)
     (cct-check-locked 22 'unlocked)))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/005-change-recompile/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;;
 ;; © Copyright 2020  Hendrik Tews
 ;;
@@ -35,6 +37,8 @@
 ;;
 ;;
 
+;;; Code:
+
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
 
@@ -197,3 +201,7 @@ See `cct-generic-check-main-buffer'."
     (check-main-buffer vo-times "71" '("./b.vo" "./d.vo" "./g.vo")
                            other-locked-files)
   ))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/006-ready-dependee/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;;
 ;; © Copyright 2020  Hendrik Tews
 ;;
@@ -27,12 +29,13 @@
 ;;
 ;; The idea is that the coqdep chain from b to j takes so long, that k
 ;; has been compiled and is in state ready before the coqdep results
-;; from j are processed. This works - unless the disk cache is cold.
-;; If it works the test triggers two bugs. First, k is locked with the
+;; from j are processed.  This works - unless the disk cache is cold.
+;; If it works the test triggers two bugs.  First, k is locked with the
 ;; require command of c. Second, the modification time of k is not
 ;; propagated to j, such that the whole chain from j to b is not
 ;; recompiled after k has changed.
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -59,7 +62,7 @@
 (defun cct-replace-last-word (line word)
   "Replace last word in line LINE with WORD.
 In current buffer, go to the end of line LINE and one word
-backward. Replace the word there with WORD."
+backward.  Replace the word there with WORD."
   (cct-goto-line line)
   (end-of-line)
   (backward-word)
@@ -130,3 +133,7 @@ Combine all the following tests in this order:
        "./h.vo" "./i.vo" "./j.vo" "./k.vo")
      other-locked-files)
   ))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/007-slow-require/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;; 
 ;; © Copyright 2021  Hendrik Tews
 ;; 
@@ -14,11 +16,11 @@
 ;;
 ;; Test two require jobs with different delays such that
 ;; coq-par-retire-top-level-job happens when the other require job is
-;; in each possible state. For specifying the different delays there
-;; are 6 mini projects, one for each test in this file. Each project
+;; in each possible state.  For specifying the different delays there
+;; are 6 mini projects, one for each test in this file.  Each project
 ;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one
-;; and a6.v, b6.v, c6.v and d6.v for the sixth one. Each project is
-;; one ert test, described further below. In each project or test, the
+;; and a6.v, b6.v, c6.v and d6.v for the sixth one.  Each project is
+;; one ert test, described further below.  In each project or test, the
 ;; top level require commands are asserted and retracted several times
 ;; with changes in different files to test (almost) all possible
 ;; internal state combinations.
@@ -53,12 +55,14 @@
 ;; seconds, such that the dependency link d->c is created when d is in
 ;; state enqueued-coqc.
 
+;;; Code:
+
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
 
 ;;; set configuration
 (cct-configure-proof-general)
-(configure-delayed-coq)    
+(configure-delayed-coq)
 
 (defconst pre-b-ancestors '("./b" "./d")
     "Ancestors of b without suffixes.")
@@ -213,3 +217,7 @@ XXX Test a setting where the second require job is still in state
 (ert-deftest cct-slow-require-4 () (test-slow-require 4))
 (ert-deftest cct-slow-require-5 () (test-slow-require 5))
 (ert-deftest cct-slow-require-6 () (test-slow-require 6))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/008-default-dir/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;; 
 ;; © Copyright 2021  Hendrik Tews
 ;; 
@@ -29,13 +31,14 @@
 ;;           c
 ;;
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
 
 ;;; set configuration
 (cct-configure-proof-general)
-(configure-delayed-coq)    
+(configure-delayed-coq)
 
 (defconst all-ancestors '("./b.v" "./c.v")
   "All ancestors.")
@@ -151,3 +154,7 @@ situations. See Coq issue 15773."
           (cct-unmodified-change-times vo-times))
       (cct-older-change-times vo-times))
     ))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/009-failure-processing/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;;
 ;; © Copyright 2021  Hendrik Tews
 ;;
@@ -13,8 +15,8 @@
 ;; ert tests for parallel background compilation for Coq
 ;;
 ;; Test a partially successful and partially failing compilation with
-;; coq-compile-keep-going. Check that the right files are compiled,
-;; locked and unlocked. Check also the case, where unlocking of failed
+;; coq-compile-keep-going.  Check that the right files are compiled,
+;; locked and unlocked.  Check also the case, where unlocking of failed
 ;; files must be delayed, because some earlier successful require job
 ;; has not yet locked its ancestors.
 ;;
@@ -36,8 +38,8 @@
 ;;
 ;; Rb, Rc and Rd are three different require commands in file a. The
 ;; dependency e -> b is not present in test 5 and test 10 (but in all
-;; other tests). The error always happens in file g, for test 1-5 with
-;; coqdep, for tests 6-10 with coqc. There are 10 tests, each with
+;; other tests).  The error always happens in file g, for test 1-5 with
+;; coqdep, for tests 6-10 with coqc.  There are 10 tests, each with
 ;; slighly different delays, in 10 versions of the sources, e.g.,
 ;; a1-a10, b1-b10, and so on.
 ;;
@@ -58,14 +60,14 @@
 ;; 9: RB is ready and Rd is queue waiting
 ;; 10: without dependency b -> e: Rc, Rd are queue waiting, b finishes last
 
-
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
 
 ;;; set configuration
 (cct-configure-proof-general)
-(configure-delayed-coq)    
+(configure-delayed-coq)
 
 (defconst pre-b-ancestors '("b" "f")
     "Ancestors of b without suffixes.")
@@ -76,8 +78,8 @@
 (defun pre-not-compiled (n)
   "List of file name stems for which coqc must not be called.
 Files for which coqc must not be called have an ``X'' in
-coqc-delay. For such files `compile-test-start-delayed' would
-create a ``.X'' file, whose absense is checked in the test."
+coqc-delay.  For such files `compile-test-start-delayed' would
+create a ``.X'' file, whose absence is checked in the test."
   (cond
    ((< n 6) '("g" "c"))
    (t       '("c"))))
@@ -140,3 +142,7 @@ create a ``.X'' file, whose absense is checked in the test."
 (ert-deftest cct-failure-processing-08 () (test-failure-processing 8))
 (ert-deftest cct-failure-processing-09 () (test-failure-processing 9))
 (ert-deftest cct-failure-processing-10 () (test-failure-processing 10))
+
+(provide 'runtest)
+
+;;; runtest.el ends here

ci/compile-tests/010-coqdep-errors/runtest.el

@@ -1,4 +1,6 @@
-;; This file is part of Proof General.  -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
 ;; 
 ;; © Copyright 2024  Hendrik Tews
 ;; 
@@ -13,7 +15,7 @@
 ;; ert tests for parallel background compilation for Coq
 ;;
 ;; Test that parallel background compilation reliably detects coqdep
-;; errors. There are three tests that check the following coqdep errors:
+;; errors.  There are three tests that check the following coqdep errors:
 ;; - coqdep on a require fails because of a missing library (using a.v)
 ;; - coqdep on a dependency fails because of a syntax error (using b.v)
 ;; - coqdep on a dependency fails because of a missing library (using d.v)
@@ -24,6 +26,7 @@
 ;;       |   |
 ;;       c   e
 
+;;; Code:
 
 ;; require cct-lib for the elisp compilation, otherwise this is present already
 (require 'cct-lib "ci/compile-tests/cct-lib")
@@ -126,3 +129,7 @@
     (should (and coqdep-errror-in-response
                  missing-module-in-response
                  (not dependency-in-coq)))))
+
+(provide 'runtest)
+
+;;; runtest.el ends here