`agda-mode compile` errors with emacs 29.1

[csams]

There are several instances of

Error: docstring has wrong usage of unescaped single quotes (use \= or different quoting)

and one instance of

Error: Doc string after `interactive'

for share/emacs-mode/agda2-mode.el

This may be fixed with Agda 2.6.4? See https://github.com/agda/agda/issues/6714

[wenkokke]

Unfortunately, moving to Agda 2.6.4 is blocked.

[sepehr541]

Here are the minor changes I made to fix the compile errors. Hope this is helpful. Feel free to look at the agda2-mode.el from v2.6.4.

--- agda2-mode.el   2024-05-17 20:56:08.379606368 -0700
+++ ~/.cabal/store/ghc-9.4.8/Agda-2.6.3-98dc26f0512b6fc265477ce47f51b6dff9479f98d0ec42d10fc1bbfff8708d2f/share/emacs-mode/agda2-mode.el 2024-05-17 20:47:56.079686691 -0700
@@ -261,8 +261,8 @@
   "Table of commands, used to build keymaps and menus.
 Each element has the form (CMD &optional KEYS WHERE DESC) where
 CMD is a command; KEYS is its key binding (if any); WHERE is a
-list which should contain 'local if the command should exist in
-the goal menu and 'global if the command should exist in the main
+list which should contain \\='local if the command should exist in
+the goal menu and \\='global if the command should exist in the main
 menu; and DESC is the description of the command used in the
 menus.")

@@ -530,7 +530,7 @@
 Sends the list of strings ARGS to the Agda2 interpreter, waits
 for output and executes the responses, if any.

-If SAVE is 'save, then the buffer is saved first.
+If SAVE is \\='save, then the buffer is saved first.

 If HIGHLIGHT is non-nil, then the buffer's syntax highlighting
 may be updated. This is also the case if the Agda process is
@@ -759,13 +759,13 @@
   contains whitespace, then the input is taken from the
   minibuffer. In this case WANT is used as the prompt string.

-* Otherwise (including if WANT is 'goal) the goal contents are
+* Otherwise (including if WANT is \\='goal) the goal contents are
   used.

 If the user input is not taken from the goal, then an empty goal
 range is given.

-If SAVE is 'save, then the buffer is saved just before the
+If SAVE is \\='save, then the buffer is saved just before the
 command is sent to Agda (if it is sent)."
   (cl-multiple-value-bind (o g) (agda2-goal-at (point))
     (unless g (error "For this command, please place the cursor in a goal"))
@@ -892,8 +892,8 @@
  (agda2-goal-cmd "Cmd_autoOne" 'save 'goal))

 (defun agda2-autoAll ()
-  (interactive)
   "Solves all goals by simple proof search."
+  (interactive)
   (agda2-go nil nil 'busy t "Cmd_autoAll")
 )

@@ -1949,7 +1949,7 @@

 (defun agda2-get-agda-program-versions ()
   "Get \"version strings\" of executables starting with
-'agda-mode' in current path."
+`agda-mode' in current path."
   (delete-dups
    (mapcar (lambda (path)
              ;; strip 'agda-mode' prefix