Warnings with emacs 29.3

[fblanqui]

Hi. I get many warnings with emacs 29.3:

uname -a
Linux blanqui-Latitude-5500 6.8.0-41-generic #41-Ubuntu SMP PREEMPT_DYNAMIC Fri Aug  2 20:41:06 UTC 2024 x86_64 x86_64 x86_64 GNU/Linux

coqc --version
The Coq Proof Assistant, version 8.19.2
compiled with OCaml 4.14.1

emacs --version
GNU Emacs 29.3
Copyright (C) 2024 Free Software Foundation, Inc.
GNU Emacs comes with ABSOLUTELY NO WARRANTY.
You may redistribute copies of GNU Emacs
under the terms of the GNU General Public License.
For more information about these matters, see the file named COPYING.

proof-general 20240708.1525:

⛔ Warning (comp): proof-splash.el:285:47: Warning: reference to free variable ‘proof-assistant’

⛔ Warning (comp): proof-splash.el:305:49: Warning: reference to free variable ‘proof-assistant’
⛔ Warning (comp): proof-auxmodes.el:32:4: Warning: reference to free variable ‘proof-assistant-symbol’
⛔ Warning (comp): proof-auxmodes.el:35:10: Warning: reference to free variable ‘proof-assistant-symbol’
⛔ Warning (comp): proof-auxmodes.el:43:2: Warning: reference to free variable ‘proof-assistant-symbol’
⛔ Warning (comp): proof-tree.el:325:2: Warning: custom-declare-variable `proof-tree-display-stop-command' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-tree.el:508:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-tree.el:1020:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-tree.el:1156:10: Warning: the function ‘proof-assert-until-point’ might not be defined at runtime.
⛔ Warning (comp): proof-tree.el:1145:26: Warning: the function ‘span-end’ might not be defined at runtime.
⛔ Warning (comp): proof-tree.el:476:12: Warning: the function ‘proof-retract-until-point’ might not be defined at runtime.
⛔ Warning (comp): proof-tree.el:455:13: Warning: the function ‘proof-shell-action-list-item’ might not be defined at runtime.
⛔ Warning (comp): proof-tree.el:454:12: Warning: the function ‘proof-add-to-priority-queue’ might not be defined at runtime.
⛔ Warning (comp): proof-tree.el:135:32: Warning: the function ‘proof-locate-executable’ might not be defined at runtime.
⛔ Warning (comp): pg-assoc.el:28:3: Warning: reference to free variable ‘proof-general-name’
⛔ Warning (comp): pg-assoc.el:32:22: Warning: reference to free variable ‘proof-universal-keys’
⛔ Warning (comp): pg-assoc.el:43:9: Warning: reference to free variable ‘proof-goals-buffer’
⛔ Warning (comp): pg-assoc.el:44:9: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-assoc.el:45:9: Warning: reference to free variable ‘proof-trace-buffer’
⛔ Warning (comp): pg-assoc.el:46:9: Warning: reference to free variable ‘proof-thms-buffer’
⛔ Warning (comp): pg-response.el:57:4: Warning: ‘easy-menu-add’ is an obsolete function (as of 28.1); this was always a no-op in Emacs and can be safely removed.
⛔ Warning (comp): pg-response.el:58:4: Warning: ‘easy-menu-add’ is an obsolete function (as of 28.1); this was always a no-op in Emacs and can be safely removed.
⛔ Warning (comp): pg-response.el:60:9: Warning: assignment to free variable ‘pg-response-next-error’
⛔ Warning (comp): pg-response.el:145:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-response.el:198:29: Warning: reference to free variable ‘proof-goals-buffer’
⛔ Warning (comp): pg-response.el:199:29: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:202:8: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): pg-response.el:226:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-response.el:272:9: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): pg-response.el:298:24: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:310:17: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): pg-response.el:337:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-response.el:362:24: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:374:23: Warning: assignment to free variable ‘pg-response-next-error’
⛔ Warning (comp): pg-response.el:391:34: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:411:26: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:442:40: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:447:40: Warning: reference to free variable ‘proof-trace-buffer’
⛔ Warning (comp): pg-response.el:457:34: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:464:34: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:486:24: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:490:46: Warning: reference to free variable ‘pg-response-next-error’
⛔ Warning (comp): pg-response.el:507:21: Warning: assignment to free variable ‘pg-response-next-error’
⛔ Warning (comp): pg-response.el:526:29: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): pg-response.el:560:44: Warning: reference to free variable ‘proof-response-buffer’
⛔ Warning (comp): pg-response.el:581:26: Warning: reference to free variable ‘proof-trace-buffer’
⛔ Warning (comp): pg-response.el:590:2: Warning: docstring wider than 80 characters
⛔ Warning (comp): pg-response.el:594:44: Warning: reference to free variable ‘proof-trace-buffer’
⛔ Warning (comp): pg-response.el:616:24: Warning: reference to free variable ‘proof-thms-buffer’
⛔ Warning (comp): pg-response.el:376:22: Warning: the function ‘bufhist-checkpoint-and-erase’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:371:16: Warning: the function ‘proof-clean-buffer’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:311:18: Warning: the function ‘proof-get-window-for-buffer’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:300:13: Warning: the function ‘pg-response-buffers-hint’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:300:4: Warning: the function ‘pg-hint’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:277:11: Warning: the function ‘proof-display-and-keep-buffer’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:163:10: Warning: the function ‘proof-safe-split-window-vertically’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:74:8: Warning: the function ‘proof-aux-menu’ might not be defined at runtime.
⛔ Warning (comp): pg-response.el:59:4: Warning: the function ‘proof-toolbar-setup’ might not be defined at runtime.
⛔ Warning (comp): proof-toolbar.el:116:8: Warning: reference to free variable ‘proof-assistant-symbol’
⛔ Warning (comp): proof-toolbar.el:121:30: Warning: reference to free variable ‘proof-mode-for-script’
⛔ Warning (comp): proof-toolbar.el:165:5: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): proof-toolbar.el:174:5: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): proof-toolbar.el:188:5: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): proof-toolbar.el:203:5: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): proof-toolbar.el:229:9: Warning: reference to free variable ‘proof-shell-proof-completed’
⛔ Warning (comp): proof-toolbar.el:228:5: Warning: reference to free variable ‘proof-script-buffer’
⛔ Warning (comp): proof-toolbar.el:273:44: Warning: reference to free variable ‘proof-shell-busy’
⛔ Warning (comp): proof-toolbar.el:283:4: Warning: reference to free variable ‘proof-assistant-symbol’
⛔ Warning (comp): pg-goals.el:42:4: Warning: ‘easy-menu-add’ is an obsolete function (as of 28.1); this was always a no-op in Emacs and can be safely removed.
⛔ Warning (comp): pg-goals.el:43:4: Warning: ‘easy-menu-add’ is an obsolete function (as of 28.1); this was always a no-op in Emacs and can be safely removed.
⛔ Warning (comp): pg-goals.el:111:16: Warning: reference to free variable ‘pg-insert-text-function’
⛔ Warning (comp): pg-user.el:496:2: Warning: docstring wider than 80 characters
⛔ Warning (comp): pg-user.el:534:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-user.el:641:18: Warning: ‘looking-back’ called with 1 argument, but requires 2 or 3
⛔ Warning (comp): pg-user.el:675:50: Warning: reference to free variable ‘coq-project-filename’
⛔ Warning (comp): pg-user.el:723:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-user.el:1378:19: Warning: ‘point-at-eol’ is an obsolete function (as of 29.1); use ‘line-end-position’ or ‘pos-eol’ instead.
⛔ Warning (comp): pg-user.el:1382:17: Warning: ‘point-at-eol’ is an obsolete function (as of 29.1); use ‘line-end-position’ or ‘pos-eol’ instead.
⛔ Warning (comp): pg-user.el:1383:29: Warning: ‘point-at-eol’ is an obsolete function (as of 29.1); use ‘line-end-position’ or ‘pos-eol’ instead.
⛔ Warning (comp): pg-user.el:1393:19: Warning: ‘point-at-eol’ is an obsolete function (as of 29.1); use ‘line-end-position’ or ‘pos-eol’ instead.
⛔ Warning (comp): pg-user.el:1676:2: Warning: defvar `proof-autosend-modified-tick' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): pg-user.el:853:6: Warning: the function ‘proof-shell-exit’ is not known to be defined.
⛔ Warning (comp): pg-user.el:774:10: Warning: the function ‘proof-add-to-queue’ is not known to be defined.
⛔ Warning (comp): proof-shell.el:82:2: Warning: defvar `proof-action-list' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:727:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:770:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:1141:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:1166:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:1737:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:1946:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): proof-shell.el:2092:8: Warning: the function ‘proof-warn-if-unset’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1423:9: Warning: the function ‘proof-files-to-buffers’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1386:4: Warning: the function ‘proof-minibuffer-message’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1364:6: Warning: the function ‘pg-pgip-process-packet’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1361:6: Warning: the function ‘proof-clean-buffer’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1352:12: Warning: the function ‘proof-register-possibly-new-processed-file’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:1247:12: Warning: the function ‘proof-tree-check-proof-finish’ is not known to be defined.
⛔ Warning (comp): proof-shell.el:1171:31: Warning: the function ‘proof-unprocessed-begin’ might not be defined at runtime.
⛔ Warning (comp): proof-shell.el:765:8: Warning: the function ‘proof-display-and-keep-buffer’ might not be defined at runtime.
⛔ Warning (comp): coq-system.el:41:2: Warning: custom-declare-variable `coq-prog-env' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-system.el:41:12: Warning: defcustom for ‘coq-prog-env’ fails to specify type
⛔ Warning (comp): coq-system.el:292:2: Warning: custom-declare-variable `coq-load-path' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-system.el:539:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-system.el:587:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): local-vars-list.el:49:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:126:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:133:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:329:12: Warning: defcustom for ‘coq-compile-keep-going’ fails to specify type
⛔ Warning (comp): coq-compile-common.el:342:2: Warning: custom-declare-variable `coq-max-background-compilation-jobs' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:382:2: Warning: custom-declare-variable `coq-compile-second-stage-delay' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:452:2: Warning: defconst `coq-compile-substitution-list' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:473:2: Warning: custom-declare-variable `coq-compile-auto-save' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:599:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:607:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:795:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-compile-common.el:70:15: Warning: the function ‘coq-seq-preprocess-require-commands’ is not known to be defined.
⛔ Warning (comp): coq-compile-common.el:52:15: Warning: the function ‘coq-par-user-interrupt’ is not known to be defined.
⛔ Warning (comp): coq-compile-common.el:50:15: Warning: the function ‘coq-par-preprocess-require-commands’ is not known to be defined.
⛔ Warning (comp): coq-seq-compile.el:28:9: Warning: global/dynamic var ‘queueitems’ lacks a prefix
⛔ Warning (comp): coq-seq-compile.el:41:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-seq-compile.el:142:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-seq-compile.el:188:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-seq-compile.el:308:14: Warning: ‘coq-load-path-include-current’ is an obsolete variable (as of 4.3); Coq 8.5 does not need it
⛔ Warning (comp): coq-seq-compile.el:311:10: Warning: ‘coq-load-path-include-current’ is an obsolete variable (as of 4.3); Coq 8.5 does not need it
⛔ Warning (comp): coq-seq-compile.el:349:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:39:9: Warning: global/dynamic var ‘queueitems’ lacks a prefix
⛔ Warning (comp): coq-par-compile.el:512:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:675:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:731:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1095:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1187:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1358:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1440:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1452:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1468:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1497:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1516:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1582:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1714:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1743:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1776:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:1847:19: Warning: ‘coq-load-path-include-current’ is an obsolete variable (as of 4.3); Coq 8.5 does not need it
⛔ Warning (comp): coq-par-compile.el:1850:10: Warning: ‘coq-load-path-include-current’ is an obsolete variable (as of 4.3); Coq 8.5 does not need it
⛔ Warning (comp): coq-par-compile.el:1887:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2001:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2020:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2053:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2098:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2111:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2125:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-par-compile.el:2210:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq-diffs.el:28:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:30:64: Warning: reference to free variable ‘proof-assistant’
⛔ Warning (comp): coq.el:41:9: Warning: global/dynamic var ‘action’ lacks a prefix
⛔ Warning (comp): coq.el:42:9: Warning: global/dynamic var ‘string’ lacks a prefix
⛔ Warning (comp): coq.el:586:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:590:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:619:2: Warning: docstring wider than 80 characters
⛔ Warning (comp): coq.el:827:2: Warning: docstring wider than 80 characters
⛔ Warning (comp): coq.el:942:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:1131:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:1199:16: Warning: reference to free variable ‘coq-diffs’
⛔ Warning (comp): coq.el:1212:2: Warning: docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:1328:9: Warning: reference to free variable ‘coq-auto-adapt-printing-width’
⛔ Warning (comp): coq.el:1991:47: Warning: reference to free variable ‘coq-shell-theorem-dependency-list-regexp’
⛔ Warning (comp): coq.el:2030:42: Warning: reference to free variable ‘coq-dependency-menu-system-specific’
⛔ Warning (comp): coq.el:2031:39: Warning: reference to free variable ‘coq-dependencies-system-specific’
⛔ Warning (comp): coq.el:2134:49: Warning: reference to free variable ‘coq-diffs’
⛔ Warning (comp): coq.el:2145:31: Warning: reference to free variable ‘coq-diffs’
⛔ Warning (comp): coq.el:2548:2: Warning: custom-declare-variable `coq-accept-proof-using-suggestion' docstring has wrong usage of unescaped single quotes (use \= or different quoting)
⛔ Warning (comp): coq.el:2623:11: Warning: Unused lexical variable `proof-pos'
⛔ Warning (comp): coq.el:3314:18: Warning: the function ‘proof-inside-string’ might not be defined at runtime.
⛔ Warning (comp): coq.el:3313:18: Warning: the function ‘proof-inside-comment’ might not be defined at runtime.
⛔ Warning (comp): coq.el: Warning: the function ‘proof-deftoggle-fn’ might not be defined at runtime.
⛔ Warning (comp): coq.el:3242:10: Warning: the function ‘proof-set-value’ might not be defined at runtime.
⛔ Warning (comp): coq.el:2483:19: Warning: the function ‘proof-shell-invisible-cmd-get-result’ might not be defined at runtime.
⛔ Warning (comp): coq.el:2141:8: Warning: the function ‘proof-shell-available-p’ might not be defined at runtime.
⛔ Warning (comp): coq.el:2086:4: Warning: the function ‘proof-response-config-done’ might not be defined at runtime.
⛔ Warning (comp): coq.el:2080:4: Warning: the function ‘proof-goals-config-done’ might not be defined at runtime.
⛔ Warning (comp): coq.el:2060:4: Warning: the function ‘proof-shell-config-done’ might not be defined at runtime.
⛔ Warning (comp): coq.el:1978:4: Warning: the function ‘proof-config-done’ might not be defined at runtime.
⛔ Warning (comp): coq.el:1858:15: Warning: the function ‘proof-shell-live-buffer’ might not be defined at runtime.
⛔ Warning (comp): coq.el:1169:14: Warning: the function ‘proof-display-and-keep-buffer’ might not be defined at runtime.
⛔ Warning (comp): coq.el:929:6: Warning: the function ‘proof-shell-ready-prover’ might not be defined at runtime.
⛔ Warning (comp): coq.el:800:8: Warning: the function ‘proof-shell-invisible-command’ might not be defined at runtime.
⛔ Warning (comp): coq.el:708:29: Warning: the function ‘proof-clean-buffer’ might not be defined at runtime.
⛔ Warning (comp): coq.el:604:18: Warning: the function ‘proof-unprocessed-begin’ might not be defined at runtime.
⛔ Warning (comp): coq.el:458:6: Warning: the function ‘pg-response-display-with-face’ might not be defined at runtime.
⛔ Warning (comp): coq.el:444:4: Warning: the function ‘proof-minibuffer-message’ might not be defined at runtime.
⛔ Warning (comp): coq.el:443:4: Warning: the function ‘pg-response-maybe-erase’ might not be defined at runtime.
⛔ Warning (comp): coq.el:320:40: Warning: the function ‘proof-response-mode’ might not be defined at runtime.
⛔ Warning (comp): coq.el:316:37: Warning: the function ‘proof-shell-mode’ might not be defined at runtime.
⛔ Warning (comp): coq.el:29:6: Warning: the function ‘proof-ready-for-assistant’ might not be defined at runtime.

[Matafou]

Hi @fblanqui. Thanks for reporting.
This has already been reported (#686) and is not specific to PG. This is due to the new "compilation" feature of emacs. I think this should happen only the first time you load a new package and the first time you trigger some part of it too.
As explained in #686, to get rid of these warning you can set native-comp-async-report-warnings-errors to nil.

[monnier]

As explained in #686, to get rid of these warning you can set `native-comp-async-report-warnings-errors` to nil.

Well, it would be nice to adjust the code to avoid the warnings, of course. 🙂