Mock Version: 3.3
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs  --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], chrootPath='/var/lib/mock/fedora-rawhide-x86_64-1668094896.354889/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x7fa1995b1fc0>timeout=0uid=1001gid=135user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=True)
Using nspawn with args ['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', 'f524b6f89e2c426ba8517ed36e46b354', '-D', '/var/lib/mock/fedora-rawhide-x86_64-1668094896.354889/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bs  --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
warning: line 60: Possible unexpanded macro in: Requires:       emacs(bin) >= %{_emacs_version}
Building target platforms: x86_64
Building for target x86_64
setting SOURCE_DATE_EPOCH=1658361600
Wrote: /builddir/build/SRPMS/emacs-common-proofgeneral-4.5-2.fc38.src.rpm
RPM build warnings:
    line 60: Possible unexpanded macro in: Requires:       emacs(bin) >= %{_emacs_version}
Child return code was: 0
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb  --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], chrootPath='/var/lib/mock/fedora-rawhide-x86_64-1668094896.354889/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x7fa1995b1fc0>timeout=0uid=1001gid=135user='mockbuild'nspawn_args=['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']unshare_net=TrueprintOutput=True)
Using nspawn with args ['--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11']
Executing command: ['/usr/bin/systemd-nspawn', '-q', '-M', '0d812fbc7c0b4f08a7a073cfddfd2b9b', '-D', '/var/lib/mock/fedora-rawhide-x86_64-1668094896.354889/root', '-a', '-u', 'mockbuild', '--capability=cap_ipc_lock', '--rlimit=RLIMIT_NOFILE=10240', '--capability=cap_ipc_lock', '--bind=/tmp/mock-resolv.urxnn21e:/etc/resolv.conf', '--bind=/dev/btrfs-control', '--bind=/dev/loop-control', '--bind=/dev/loop0', '--bind=/dev/loop1', '--bind=/dev/loop2', '--bind=/dev/loop3', '--bind=/dev/loop4', '--bind=/dev/loop5', '--bind=/dev/loop6', '--bind=/dev/loop7', '--bind=/dev/loop8', '--bind=/dev/loop9', '--bind=/dev/loop10', '--bind=/dev/loop11', '--console=pipe', '--setenv=TERM=vt100', '--setenv=SHELL=/bin/bash', '--setenv=HOME=/builddir', '--setenv=HOSTNAME=mock', '--setenv=PATH=/usr/bin:/bin:/usr/sbin:/sbin', '--setenv=PROMPT_COMMAND=printf "\\033]0;<mock-chroot>\\007"', '--setenv=PS1=<mock-chroot> \\s-\\v\\$ ', '--setenv=LANG=C.UTF-8', '--resolv-conf=off', 'bash', '--login', '-c', '/usr/bin/rpmbuild -bb  --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8', 'SYSTEMD_NSPAWN_TMPFS_TMP': '0', 'SYSTEMD_SECCOMP': '0'} and shell False
Building target platforms: x86_64
Building for target x86_64
setting SOURCE_DATE_EPOCH=1658361600
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.qHFCge
+ umask 022
+ cd /builddir/build/BUILD
+ cd /builddir/build/BUILD
+ rm -rf PG-4.5
+ /usr/lib/rpm/rpmuncompress -x /builddir/build/SOURCES/PG-4.5.tar.gz
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd PG-4.5
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ /usr/lib/rpm/rpmuncompress /builddir/build/SOURCES/pg-4.2-Makefile.patch
+ /usr/bin/patch -p0 -s --fuzz=0 --no-backup-if-mismatch -f
+ /usr/lib/rpm/rpmuncompress /builddir/build/SOURCES/pg-4.2-desktop.patch
+ /usr/bin/patch -p0 -s --fuzz=0 --no-backup-if-mismatch -f
+ find . -name .cvsignore -delete
+ for f in phox/sqrt2.phx
+ mv phox/sqrt2.phx phox/sqrt2.phx.orig
+ iconv -f iso-8859-1 -t utf8 phox/sqrt2.phx.orig
+ fixtimestamp phox/sqrt2.phx
+ touch -r phox/sqrt2.phx.orig phox/sqrt2.phx
+ rm -f phox/sqrt2.phx.orig
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.BZQYmb
+ umask 022
+ cd /builddir/build/BUILD
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection'
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection'
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection -I/usr/lib64/gfortran/modules'
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection -I/usr/lib64/gfortran/modules'
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd PG-4.5
+ make clean
(for i in coq/coqtags; do \
   if [ -f $i.rm ] ; then    \
     rm -f $i.rm; 	      \
   fi; 			      \
   if [ -f $i.orig ] ; then  \
             mv -f $i.orig $i;      \
           fi; 			      \
 done)
rm -f coq/coq-abbrev.elc coq/coq-autotest.elc coq/coq-compile-common.elc coq/coq-db.elc coq/coq-diffs.elc coq/coq-indent.elc coq/coq-local-vars.elc coq/coq-mode.elc coq/coq-par-compile.elc coq/coq-seq-compile.elc coq/coq-smie.elc coq/coq-syntax.elc coq/coq-system.elc coq/coq-unicode-tokens.elc coq/coq.elc easycrypt/easycrypt-abbrev.elc easycrypt/easycrypt-hooks.elc easycrypt/easycrypt-keywords.elc easycrypt/easycrypt-syntax.elc easycrypt/easycrypt.elc pghaskell/pghaskell.elc pgocaml/pgocaml.elc pgshell/pgshell.elc phox/phox.elc qrhl/qrhl-input.elc qrhl/qrhl.elc generic/pg-assoc.elc generic/pg-autotest.elc generic/pg-custom.elc generic/pg-goals.elc generic/pg-movie.elc generic/pg-pamacs.elc generic/pg-pbrpm.elc generic/pg-pgip.elc generic/pg-response.elc generic/pg-user.elc generic/pg-vars.elc generic/pg-xml.elc generic/proof-autoloads.elc generic/proof-auxmodes.elc generic/proof-config.elc generic/proof-depends.elc generic/proof-easy-config.elc generic/proof-faces.elc generic/proof-indent.elc generic/proof-maths-menu.elc generic/proof-menu.elc generic/proof-script.elc generic/proof-shell.elc generic/proof-site.elc generic/proof-splash.elc generic/proof-syntax.elc generic/proof-toolbar.elc generic/proof-tree.elc generic/proof-unicode-tokens.elc generic/proof-useropts.elc generic/proof-utils.elc generic/proof.elc lib/bufhist.elc lib/holes.elc lib/local-vars-list.elc lib/maths-menu.elc lib/pg-dev.elc lib/pg-fontsets.elc lib/proof-compat.elc lib/scomint.elc lib/span.elc lib/texi-docstring-magic.elc lib/unicode-chars.elc lib/unicode-tokens.elc ci/compile-tests/cct-lib.elc ci/compile-tests/001-mini-project/runtest.elc ci/compile-tests/002-require-no-dependencies/runtest.elc ci/compile-tests/003-require-error/runtest.elc ci/compile-tests/004-dependency-cycle/runtest.elc ci/compile-tests/005-change-recompile/runtest.elc ci/compile-tests/006-ready-dependee/runtest.elc ci/compile-tests/007-slow-require/runtest.elc ci/compile-tests/008-default-dir/runtest.elc ci/compile-tests/009-failure-processing/runtest.elc ci/simple-tests/test-coq-par-job-needs-compilation-quick.elc ci/simple-tests/test-coqtop-unavailable.elc ci/simple-tests/test-omit-proofs.elc ci/simple-tests/test-prelude-correct.elc ci/simple-tests/test-qrhl.elc .\#* */.\#* */.autotest.log */.profile.log
(cd doc; make clean)
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" clean
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
rm -f PG-adapting.cp PG-adapting.fn PG-adapting.vr PG-adapting.tp PG-adapting.ky PG-adapting.kys PG-adapting.pg PG-adapting.fns PG-adapting.vrs PG-adapting.cps PG-adapting.aux PG-adapting.log PG-adapting.cp PG-adapting.cp0 PG-adapting.toc
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" clean 
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
rm -f ProofGeneral.cp ProofGeneral.fn ProofGeneral.vr ProofGeneral.tp ProofGeneral.ky ProofGeneral.kys ProofGeneral.pg ProofGeneral.fns ProofGeneral.vrs ProofGeneral.cps ProofGeneral.aux ProofGeneral.log ProofGeneral.cp ProofGeneral.cp0 ProofGeneral.toc
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
+ make EMACS=emacs compile bashscripts perlscripts doc
****************************************************************
 Byte compiling... 
****************************************************************
make elc
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-abbrev.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-autotest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-compile-common.el
In toplevel form:
coq/coq-compile-common.el:329:1: Warning: defcustom for
    `coq-compile-keep-going' fails to specify type
coq/coq-compile-common.el:329:1: Warning: defcustom for
    `coq-compile-keep-going' fails to specify type
In end of data:
coq/coq-compile-common.el:70:15: Warning: the function
    `coq-seq-preprocess-require-commands' is not known to be defined.
coq/coq-compile-common.el:52:15: Warning: the function
    `coq-par-user-interrupt' is not known to be defined.
coq/coq-compile-common.el:50:15: Warning: the function
    `coq-par-preprocess-require-commands' is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-db.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-diffs.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-indent.el
In coq-looking-at-comment:
coq/coq-indent.el:267:8: Warning: function `coq-looking-at-comment' defined
    multiple times in this file
In coq-empty-command-p:
coq/coq-indent.el:387:6: Warning: looking-back called with 1 argument, but
    requires 2-3
coq/coq-indent.el:387:6: Warning: looking-back called with 1 argument, but
    requires 2-3
In end of data:
coq/coq-indent.el:198:8: Warning: the function `proof-inside-comment' is not
    known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-local-vars.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-mode.el
In end of data:
coq/coq-mode.el:237:19: Warning: the function `coq-pg-setup' is not known to
    be defined.
coq/coq-mode.el:183:19: Warning: the function `proof-mode' is not known to be
    defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-par-compile.el
In toplevel form:
coq/coq-par-compile.el:39:1: Warning: global/dynamic var `queueitems' lacks a
    prefix
In coq-par-start-coqdep-on-require:
coq/coq-par-compile.el:1833:19: Warning: `coq-load-path-include-current' is an
    obsolete variable (as of 4.3); Coq 8.5 does not need it
coq/coq-par-compile.el:1836:10: Warning: `coq-load-path-include-current' is an
    obsolete variable (as of 4.3); Coq 8.5 does not need it
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-seq-compile.el
In toplevel form:
coq/coq-seq-compile.el:28:1: Warning: global/dynamic var `queueitems' lacks a
    prefix
In coq-seq-map-module-id-to-obj-file:
coq/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
coq/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
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-smie.el
In coq-debug-smie--parent:
coq/coq-smie.el:1286:21: Warning: Unused lexical variable `regi'
coq/coq-smie.el:1287:32: Warning: Unused lexical variable `tok'
coq/coq-smie.el:1288:26: Warning: Unused lexical variable `face'
coq/coq-smie.el:1371:1: Warning: defcustom for
    `coq-indent-align-with-first-arg' fails to specify containing group
coq/coq-smie.el:1371:1: Warning: defcustom for
    `coq-indent-align-with-first-arg' fails to specify containing group
In end of data:
coq/coq-smie.el:1305:5: Warning: the function `hlt-unhighlight-region' is not
    known to be defined.
coq/coq-smie.el:1297:6: Warning: the function `hlt-highlight-regions' is not
    known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-syntax.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-system.el
In toplevel form:
coq/coq-system.el:41:1: Warning: defcustom for `coq-prog-env' fails to specify
    type
coq/coq-system.el:41:1: Warning: defcustom for `coq-prog-env' fails to specify
    type
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq-unicode-tokens.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile coq/coq.el
In toplevel form:
coq/coq.el:30:64: Warning: reference to free variable `proof-assistant'
coq/coq.el:42:1: Warning: global/dynamic var `action' lacks a prefix
coq/coq.el:43:1: Warning: global/dynamic var `string' lacks a prefix
In coq-set-state-infos:
coq/coq.el:626:8: Warning: docstring wider than 80 characters
In coq-grab-punctuation-left:
coq/coq.el:817:8: Warning: docstring wider than 80 characters
In coq--show-proof-stepwise-cmds:
coq/coq.el:1189:16: Warning: reference to free variable `coq-diffs'
In coq-adapt-printing-width:
coq/coq.el:1318:9: Warning: reference to free variable
    `coq-auto-adapt-printing-width'
In coq-shell-mode-config:
coq/coq.el:1971:47: Warning: reference to free variable
    `coq-shell-theorem-dependency-list-regexp'
coq/coq.el:2006:42: Warning: reference to free variable
    `coq-dependency-menu-system-specific'
coq/coq.el:2007:39: Warning: reference to free variable
    `coq-dependencies-system-specific'
In coq-diffs:
coq/coq.el:2113:49: Warning: reference to free variable `coq-diffs'
In coq-diffs--setter:
coq/coq.el:2124:19: Warning: reference to free variable `coq-diffs'
In coq-highlight-span-dependencies:
coq/coq.el:2707:14: Warning: Unused lexical variable `proof-pos'
In end of data:
coq/coq.el:29:6: Warning: the function `proof-ready-for-assistant' might not
    be defined at runtime.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile easycrypt/easycrypt-abbrev.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile easycrypt/easycrypt-hooks.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile easycrypt/easycrypt-keywords.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile easycrypt/easycrypt-syntax.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile easycrypt/easycrypt.el
In easycrypt-build-prog-args:
easycrypt/easycrypt.el:64:20: Warning: reference to free variable
    `easycrypt-prog-args'
easycrypt/easycrypt.el:65:18: Warning: assignment to free variable
    `easycrypt-prog-args'
In easycrypt-prog-args:
easycrypt/easycrypt.el:71:11: Warning: reference to free variable
    `easycrypt-prog-args'
easycrypt/easycrypt.el:256:13: Warning: reference to free variable
    `easycrypt-keymap'
In end of data:
easycrypt/easycrypt.el:219:4: Warning: the function `easycrypt-redisplay' is
    not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile pghaskell/pghaskell.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile pgocaml/pgocaml.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile pgshell/pgshell.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile phox/phox.el
In substitute-patterns-with-unicode-symbol:
phox/phox.el:102:8: Warning: docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile qrhl/qrhl-input.el
Loading /usr/share/emacs/28.1/lisp/international/uni-name.el (source)...
qrhl-input: 1539 rules (+ 0 conflicts)!
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile qrhl/qrhl.el
In toplevel form:
qrhl/qrhl.el:97:3: Warning: assignment to free variable `qrhl-prog-args'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-assoc.el
In proof-universal-keys-only-mode:
generic/pg-assoc.el:28:3: Warning: reference to free variable
    `proof-general-name'
generic/pg-assoc.el:32:22: Warning: reference to free variable
    `proof-universal-keys'
In proof-associated-buffers:
generic/pg-assoc.el:43:9: Warning: reference to free variable
    `proof-goals-buffer'
generic/pg-assoc.el:44:9: Warning: reference to free variable
    `proof-response-buffer'
generic/pg-assoc.el:45:9: Warning: reference to free variable
    `proof-trace-buffer'
generic/pg-assoc.el:46:9: Warning: reference to free variable
    `proof-thms-buffer'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-autotest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-custom.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-goals.el
In proof-goals-mode:
generic/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.
generic/pg-goals.el:42:18: 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.
In pg-goals-display:
generic/pg-goals.el:111:16: Warning: reference to free variable
    `pg-insert-text-function'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-movie.el
In pg-movie-of-span:
generic/pg-movie.el:51:26: Warning: reference to free variable
    `proof-assistant-symbol'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-pamacs.el
In proof-ass-differs-from-default:
generic/pg-pamacs.el:75:8: Warning: docstring wider than 80 characters
generic/pg-pamacs.el:75:40: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-defpgcustom-fn:
generic/pg-pamacs.el:100:42: Warning: reference to free variable
    `proof-assistant-symbol'
In undefpgcustom:
generic/pg-pamacs.el:110:59: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-defpgdefault-fn:
generic/pg-pamacs.el:127:35: Warning: reference to free variable
    `proof-assistant-symbol'
In defpgfun:
generic/pg-pamacs.el:154:5: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-defpacustom-fn:
generic/pg-pamacs.el:168:16: Warning: reference to free variable
    `proof-assistant'
generic/pg-pamacs.el:231:11: Warning: reference to free variable
    `proof-assistant-settings'
generic/pg-pamacs.el:216:24: Warning: reference to free variable
    `proof-assistant-cusgrp'
generic/pg-pamacs.el:228:43: Warning: assignment to free variable
    `proof-assistant-settings'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-pbrpm.el
In pg-pbrpm-menu-change-hook:
generic/pg-pbrpm.el:92:45: Warning: Unused lexical argument `end'
generic/pg-pbrpm.el:92:45: Warning: Unused lexical argument `len'
In pg-pbrpm-build-menu:
generic/pg-pbrpm.el:264:29: Warning: Unused lexical argument `n'
In pg-pbrpm-setup-span:
generic/pg-pbrpm.el:328:56: Warning: Unused lexical argument `sp2'
In pg-pbrpm-get-pos-info:
generic/pg-pbrpm.el:393:25: Warning: Unused lexical variable `start-hyp-text'
generic/pg-pbrpm.el:470:52: Warning: Unused lexical argument `count'
In pg-pbrpm-remember-region-drag-up-hook:
generic/pg-pbrpm.el:518:53: Warning: Unused lexical argument `click-count'
In pg-pbrpm-remember-region:
generic/pg-pbrpm.el:530:4: Warning: Unused lexical argument `delete'
generic/pg-pbrpm.el:537:27: Warning: Unused lexical variable
    `mouse-track-drag-up-hook'
generic/pg-pbrpm.el:537:27: Warning: Unused lexical variable
    `mouse-track-click-hook'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-pgip.el
In pg-pgip-process-packet:
generic/pg-pgip.el:51:8: Warning: docstring wider than 80 characters
In pg-pgip-process-newfile:
generic/pg-pgip.el:402:49: Warning: global/dynamic var `proverid' lacks a
    prefix
In pg-pgip-issue:
generic/pg-pgip.el:617:8: Warning: docstring wider than 80 characters
In end of data:
generic/pg-pgip.el:454:21: Warning: the function `proof-segment-up-to' is not
    known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-response.el
In proof-response-mode:
generic/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.
generic/pg-response.el:57:18: 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.
generic/pg-response.el:60:9: Warning: assignment to free variable
    `pg-response-next-error'
In proof-display-three-b:
generic/pg-response.el:196:28: Warning: reference to free variable
    `proof-goals-buffer'
generic/pg-response.el:196:47: Warning: reference to free variable
    `proof-response-buffer'
generic/pg-response.el:196:8: Warning: reference to free variable
    `proof-script-buffer'
In proof-layout-windows:
generic/pg-response.el:266:9: Warning: reference to free variable
    `proof-script-buffer'
generic/pg-response.el:288:24: Warning: reference to free variable
    `proof-response-buffer'
In proof-delete-other-frames:
generic/pg-response.el:301:46: Warning: reference to free variable
    `proof-script-buffer'
In pg-response-maybe-erase:
generic/pg-response.el:352:24: Warning: reference to free variable
    `proof-response-buffer'
generic/pg-response.el:364:23: Warning: assignment to free variable
    `pg-response-next-error'
In pg-response-display:
generic/pg-response.el:381:34: Warning: reference to free variable
    `proof-response-buffer'
In pg-response-display-with-face:
generic/pg-response.el:401:26: Warning: reference to free variable
    `proof-response-buffer'
In pg-response-clear-displays:
generic/pg-response.el:432:40: Warning: reference to free variable
    `proof-response-buffer'
generic/pg-response.el:437:40: Warning: reference to free variable
    `proof-trace-buffer'
In pg-response-message:
generic/pg-response.el:447:34: Warning: reference to free variable
    `proof-response-buffer'
In pg-response-warning:
generic/pg-response.el:454:34: Warning: reference to free variable
    `proof-response-buffer'
In proof-next-error:
generic/pg-response.el:476:24: Warning: reference to free variable
    `proof-response-buffer'
generic/pg-response.el:480:46: Warning: reference to free variable
    `pg-response-next-error'
generic/pg-response.el:542:19: Warning: assignment to free variable
    `pg-response-next-error'
generic/pg-response.el:516:29: Warning: reference to free variable
    `proof-script-buffer'
In pg-response-has-error-location:
generic/pg-response.el:550:44: Warning: reference to free variable
    `proof-response-buffer'
In proof-trace-buffer-display:
generic/pg-response.el:571:26: Warning: reference to free variable
    `proof-trace-buffer'
In proof-trace-buffer-finish:
generic/pg-response.el:580:8: Warning: docstring wider than 80 characters
generic/pg-response.el:584:44: Warning: reference to free variable
    `proof-trace-buffer'
In pg-thms-buffer-clear:
generic/pg-response.el:606:24: Warning: reference to free variable
    `proof-thms-buffer'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-user.el
In proof-find-theorems:
generic/pg-user.el:485:41: Warning: docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-vars.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/pg-xml.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-autoloads.el
In toplevel form:
generic/proof-autoloads.el:507:1: Warning: autoload `pg-pgip-process-packet'
    docstring wider than 80 characters
generic/proof-autoloads.el:839:1: Warning: autoload `proof-colour-locked'
    docstring wider than 80 characters
generic/proof-autoloads.el:1043:1: Warning: autoload
    `proof-replace-regexp-in-string' docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-auxmodes.el
In proof-maths-menu-support-available:
generic/proof-auxmodes.el:29:8: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-auxmodes.el:37:38: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-unicode-tokens-support-available:
generic/proof-auxmodes.el:43:8: Warning: reference to free variable
    `proof-assistant-symbol'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-config.el
In toplevel form:
generic/proof-config.el:828:1: Warning: custom-declare-variable
    `proof-script-font-lock-keywords' docstring wider than 80 characters
generic/proof-config.el:1942:1: Warning: custom-declare-variable
    `proof-goals-font-lock-keywords' docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-depends.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-easy-config.el
In proof-easy-config-define-derived-modes:
generic/proof-easy-config.el:41:44: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-easy-config.el:45:31: Warning: reference to free variable
    `proof-assistant'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-faces.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-indent.el
In proof-indent-goto-prev:
generic/proof-indent.el:60:8: Warning: docstring wider than 80 characters
In proof-indent-line:
generic/proof-indent.el:90:4: Warning: reference to free variable
    `proof-assistant-symbol'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-maths-menu.el
In proof-maths-menu-set-global:
generic/proof-maths-menu.el:35:37: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-maths-menu.el:43:30: Warning: reference to free variable
    `proof-mode-for-script'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-menu.el
In proof-display-some-buffers:
generic/proof-menu.el:56:47: Warning: reference to free variable
    `proof-response-buffer'
generic/proof-menu.el:57:47: Warning: reference to free variable
    `proof-thms-buffer'
generic/proof-menu.el:58:47: Warning: reference to free variable
    `proof-trace-buffer'
generic/proof-menu.el:59:47: Warning: reference to free variable
    `proof-goals-buffer'
In proof-menu-define-keys:
generic/proof-menu.el:143:26: Warning: reference to free variable
    `proof-universal-keys'
In proof-menu-define-specific:
generic/proof-menu.el:175:28: Warning: reference to free variable
    `proof-assistant'
generic/proof-menu.el:202:22: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-assistant-menu-update:
generic/proof-menu.el:216:45: Warning: reference to free variable
    `proof-mode-for-script'
generic/proof-menu.el:217:6: Warning: `easy-menu-remove' is an obsolete
    function (as of 28.1); this was always a no-op in Emacs and can be safely
    removed.
generic/proof-menu.el:220:6: 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.
generic/proof-menu.el:220:20: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-menu.el:344:39: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-keep-response-history:
generic/proof-menu.el:346:8: Warning: docstring wider than 80 characters
In proof-quick-opts-vars:
generic/proof-menu.el:588:5: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-main-menu:
generic/proof-menu.el:711:9: Warning: reference to free variable
    `proof-general-name'
In proof-aux-menu:
generic/proof-menu.el:724:9: Warning: reference to free variable
    `proof-general-name'
In proof-menu-define-favourites-menu:
generic/proof-menu.el:740:16: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-def-favourite:
generic/proof-menu.el:769:38: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-save-favourites:
generic/proof-menu.el:794:4: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-del-favourite:
generic/proof-menu.el:801:31: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-read-favourite:
generic/proof-menu.el:819:44: Warning: reference to free variable
    `proof-assistant'
In proof-add-favourite:
generic/proof-menu.el:856:41: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-menu-define-settings-menu:
generic/proof-menu.el:864:8: Warning: docstring wider than 80 characters
generic/proof-menu.el:866:7: Warning: reference to free variable
    `proof-assistant-settings'
In proof-menu-entry-for-setting:
generic/proof-menu.el:905:45: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-settings-vars:
generic/proof-menu.el:930:21: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-menu.el:931:12: Warning: reference to free variable
    `proof-assistant-settings'
generic/proof-menu.el:932:4: Warning: reference to free variable
    `proof-assistant-additional-settings'
In proof-assistant-invisible-command-ifposs:
generic/proof-menu.el:969:21: Warning: reference to free variable
    `proof-nesting-depth'
In proof-maybe-askprefs:
generic/proof-menu.el:981:24: Warning: reference to free variable
    `proof-assistant-settings'
generic/proof-menu.el:986:13: Warning: assignment to free variable
    `proof-assistant-settings'
In proof-assistant-settings-cmd:
generic/proof-menu.el:992:29: Warning: reference to free variable
    `proof-assistant-settings'
generic/proof-menu.el:996:11: Warning: reference to free variable
    `proof-assistant-symbol'
In proof-assistant-settings-cmds:
generic/proof-menu.el:1001:22: Warning: reference to free variable
    `proof-assistant-settings'
generic/proof-menu.el:1008:44: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-menu.el:1013:1: Warning: defvar `proof-assistant-format-table'
    docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-script.el
In proof-colour-locked:
generic/proof-script.el:317:8: Warning: docstring wider than 80 characters
In proof-colour-locked-span:
generic/proof-script.el:324:8: Warning: docstring wider than 80 characters
In proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window:
generic/proof-script.el:525:8: Warning: docstring wider than 80 characters
In proof-setup-imenu:
generic/proof-script.el:2875:8: Warning: docstring wider than 80 characters
In end of data:
generic/proof-script.el:2801:13: Warning: the function
    `proof-electric-terminator' is not known to be defined.
generic/proof-script.el:745:40: Warning: the function `pg-span-context-menu'
    is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-shell.el
In proof-shell-mode:
generic/proof-shell.el:2035:14: Warning: `buffer-substring-filters' is an
    obsolete variable (as of 24.1); use `filter-buffer-substring-function'
    instead.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-site.el
In toplevel form:
generic/proof-site.el:238:1: Warning: defvar
    `proof-general-configured-provers' docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-splash.el
In proof-splash-message:
generic/proof-splash.el:285:47: Warning: reference to free variable
    `proof-assistant'
In proof-splash-set-frame-titles:
generic/proof-splash.el:305:49: Warning: reference to free variable
    `proof-assistant'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-syntax.el
In proof-replace-regexp-in-string:
generic/proof-syntax.el:68:8: Warning: docstring wider than 80 characters
In proof-re-search-forward:
generic/proof-syntax.el:73:11: Warning: docstring wider than 80 characters
In proof-re-search-backward:
generic/proof-syntax.el:78:11: Warning: docstring wider than 80 characters
In proof-re-search-forward-safe:
generic/proof-syntax.el:83:11: Warning: docstring wider than 80 characters
In proof-looking-at-syntactic-context:
generic/proof-syntax.el:154:8: Warning: reference to free variable
    `proof-assistant-symbol'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-toolbar.el
In proof-toolbar-setup:
generic/proof-toolbar.el:116:14: Warning: reference to free variable
    `proof-assistant-symbol'
generic/proof-toolbar.el:121:30: Warning: reference to free variable
    `proof-mode-for-script'
In proof-toolbar-undo-enable-p:
generic/proof-toolbar.el:166:13: Warning: reference to free variable
    `proof-script-buffer'
In proof-toolbar-delete-enable-p:
generic/proof-toolbar.el:176:13: Warning: reference to free variable
    `proof-script-buffer'
In proof-toolbar-next-enable-p:
generic/proof-toolbar.el:188:10: Warning: reference to free variable
    `proof-script-buffer'
In proof-toolbar-retract-enable-p:
generic/proof-toolbar.el:203:10: Warning: reference to free variable
    `proof-script-buffer'
In proof-toolbar-qed-enable-p:
generic/proof-toolbar.el:229:9: Warning: reference to free variable
    `proof-shell-proof-completed'
generic/proof-toolbar.el:230:10: Warning: reference to free variable
    `proof-script-buffer'
In proof-toolbar-interrupt-enable-p:
generic/proof-toolbar.el:273:44: Warning: reference to free variable
    `proof-shell-busy'
In proof-toolbar-scripting-menu:
generic/proof-toolbar.el:283:9: Warning: reference to free variable
    `proof-assistant-symbol'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-tree.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-unicode-tokens.el
In proof-unicode-tokens-init:
generic/proof-unicode-tokens.el:45:25: Warning: reference to free variable
    `proof-mode-for-script'
generic/proof-unicode-tokens.el:46:25: Warning: reference to free variable
    `proof-mode-for-response'
generic/proof-unicode-tokens.el:47:25: Warning: reference to free variable
    `proof-mode-for-goals'
In proof-unicode-tokens-mode-if-enabled:
generic/proof-unicode-tokens.el:67:19: Warning: reference to free variable
    `unicode-tokens-enable'
In proof-unicode-tokens-set-global:
generic/proof-unicode-tokens.el:78:28: Warning: reference to free variable
    `proof-mode-for-script'
In proof-unicode-tokens-reconfigure:
generic/proof-unicode-tokens.el:116:22: Warning: reference to free variable
    `unicode-tokens-enable'
generic/proof-unicode-tokens.el:118:31: Warning: reference to free variable
    `proof-mode-for-script'
In proof-unicode-tokens-configure-prover:
generic/proof-unicode-tokens.el:133:18: Warning: reference to free variable
    `unicode-tokens-enable'
In end of data:
generic/proof-unicode-tokens.el:141:6: Warning: the function
    `proof-shell-invisible-command-invisible-result' is not known to be
    defined.
generic/proof-unicode-tokens.el:140:15: Warning: the function
    `proof-shell-available-p' is not known to be defined.
generic/proof-unicode-tokens.el:139:15: Warning: the function
    `proof-shell-live-buffer' is not known to be defined.
generic/proof-unicode-tokens.el:95:10: Warning: the function
    `proof-unicode-tokens-support-available' is not known to be defined.
generic/proof-unicode-tokens.el:79:6: Warning: the function
    `proof-associated-buffers' is not known to be defined.
generic/proof-unicode-tokens.el:78:6: Warning: the function
    `proof-buffers-in-mode' is not known to be defined.
generic/proof-unicode-tokens.el:76:4: Warning: the function
    `proof-map-buffers' is not known to be defined.
generic/proof-unicode-tokens.el:67:9: Warning: the function `proof-ass' is not
    known to be defined.
generic/proof-unicode-tokens.el:56:18: Warning: the function `proof-ass-symv'
    is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-useropts.el
In toplevel form:
generic/proof-useropts.el:462:1: Warning: custom-declare-variable
    `proof-autosend-all' docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof-utils.el
In proof-get-window-for-buffer:
generic/proof-utils.el:293:69: Warning: reference to free variable
    `proof-script-buffer'
In proof-clean-buffer:
generic/proof-utils.el:346:24: Warning: reference to free variable
    `proof-response-buffer'
generic/proof-utils.el:347:19: Warning: assignment to free variable
    `pg-response-next-error'
In proof-minibuffer-message:
generic/proof-utils.el:781:28: Warning: reference to free variable
    `proof-assistant'
In end of data:
generic/proof-utils.el:122:8: Warning: the function `package-menu-execute' is
    not known to be defined.
generic/proof-utils.el:117:6: Warning: the function
    `package-menu-mark-upgrades' is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile generic/proof.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/bufhist.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/holes.el
In holes-replace-active-hole:
lib/holes.el:429:8: Warning: docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/local-vars-list.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/maths-menu.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/pg-dev.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/pg-fontsets.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/proof-compat.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/scomint.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/span.el
In span-write-warning:
lib/span.el:54:8: Warning: docstring wider than 80 characters
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/texi-docstring-magic.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/unicode-chars.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile lib/unicode-tokens.el
In toplevel form:
lib/unicode-tokens.el:199:14: Warning: Unused lexical variable `sym'
In unicode-tokens-symbs-to-props:
lib/unicode-tokens.el:590:8: Warning: docstring wider than 80 characters
In unicode-tokens-insert-control:
lib/unicode-tokens.el:736:8: Warning: docstring wider than 80 characters
In unicode-tokens-prev-token:
lib/unicode-tokens.el:819:8: Warning: docstring wider than 80 characters
In unicode-tokens-highlight-unicode-setkeywords:
lib/unicode-tokens.el:1056:8: Warning: docstring wider than 80 characters
In unicode-tokens-set-font-var-aux:
lib/unicode-tokens.el:1286:22: Warning: `font-lock-fontify-buffer' is for
    interactive use only; use `font-lock-ensure' or `font-lock-flush' instead.
In unicode-tokens-set-font-restart:
lib/unicode-tokens.el:1310:6: Warning: `font-lock-fontify-buffer' is for
    interactive use only; use `font-lock-ensure' or `font-lock-flush' instead.
In end of data:
lib/unicode-tokens.el:1229:8: Warning: the function
    `old-ns-respond-to-change-font' is not known to be defined.
lib/unicode-tokens.el:977:48: Warning: the function `unicode-chars-list-chars'
    is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/cct-lib.el
In cct-wait-for-second-stage:
ci/compile-tests/cct-lib.el:156:16: Warning: reference to free variable
    `coq--par-second-stage-delay-timer'
ci/compile-tests/cct-lib.el:157:16: Warning: reference to free variable
    `coq--par-second-stage-in-progress'
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/001-mini-project/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/002-require-no-dependencies/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/003-require-error/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/004-dependency-cycle/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/005-change-recompile/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/006-ready-dependee/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/007-slow-require/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/008-default-dir/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/compile-tests/009-failure-processing/runtest.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/simple-tests/test-coq-par-job-needs-compilation-quick.el
In end of data:
ci/simple-tests/test-coq-par-job-needs-compilation-quick.el:761:9: Warning:
    the function `should' might not be defined at runtime.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/simple-tests/test-coqtop-unavailable.el
In toplevel form:
ci/simple-tests/test-coqtop-unavailable.el:18:9: Warning: assignment to free
    variable `coq-prog-name'
ci/simple-tests/test-coqtop-unavailable.el:21:29: Warning: reference to free
    variable `coq-prog-name'
In end of data:
ci/simple-tests/test-coqtop-unavailable.el:24:4: Warning: the function
    `coq-prog-args' is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/simple-tests/test-omit-proofs.el
In wait-for-coq:
ci/simple-tests/test-omit-proofs.el:35:14: Warning: reference to free variable
    `proof-second-action-list-active'
ci/simple-tests/test-omit-proofs.el:36:21: Warning: reference to free variable
    `proof-action-list'
ci/simple-tests/test-omit-proofs.el:77:9: Warning: assignment to free variable
    `proof-omit-proofs-option'
ci/simple-tests/test-omit-proofs.el:78:9: Warning: assignment to free variable
    `proof-three-window-enable'
In end of data:
ci/simple-tests/test-omit-proofs.el:131:4: Warning: the function
    `proof-goto-point' is not known to be defined.
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/simple-tests/test-prelude-correct.el
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar (lambda (d) (expand-file-name (symbol-name d))) (quote (\. coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib ci/compile-tests ci/compile-tests/001-mini-project ci/compile-tests/002-require-no-dependencies ci/compile-tests/003-require-error ci/compile-tests/004-dependency-cycle ci/compile-tests/005-change-recompile ci/compile-tests/006-ready-dependee ci/compile-tests/007-slow-require ci/compile-tests/008-default-dir ci/compile-tests/009-failure-processing ci/simple-tests))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote noruntime) byte-compile-warning-types)) (setq byte-compile-error-on-warn nil))' -f batch-byte-compile ci/simple-tests/test-qrhl.el
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5'
****************************************************************
 Finished.
****************************************************************
(bash="`which bash`";					    \
 if [ -z "$bash" ]; then				    \
   echo "Could not find bash - bash paths not checked" >&2; \
   exit 0;						    \
 fi)
(perl="`which perl`";					    \
 if [ -z "$perl" ]; then				    \
   echo "Could not find perl - perl paths not checked" >&2; \
   exit 0;						    \
 fi;							    \
 for i in coq/coqtags; do			    	    \
   sed -i.orig "s|^#.*!.*/bin/perl.*$|#!$perl|" $i;      \
 done)
(cd doc; make EMACS=emacs )
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make doc
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" doc
make[3]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
texi2pdf PG-adapting.texi 
egrep: warning: egrep is obsolescent; using grep -E
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021) (preloaded format=pdfetex)
 restricted \write18 enabled.
entering extended mode
(./PG-adapting.texi (/usr/share/texlive/texmf-dist/tex/texinfo/texinfo.tex
Loading texinfo [version 2021-04-25.21]: pdf, fonts, glyphs, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, insertions,
(/usr/share/texlive/texmf-dist/tex/generic/epsf/epsf.tex
This is `epsf.tex' v2.7.4 <14 February 2011>
) localization, formatting, and turning on texinfo input format.) </builddir/bu
ild/BUILD/PG-4.5/doc/ProofGeneral-image.jpg> [1{/usr/share/texlive/texmf-var/fo
nts/map/pdftex/updmap/pdftex.map}] [2] (Introduction)
Writing index file PG-adapting.cp
Chapter 1 [1] [2] Cross reference values unknown; you must run TeX again.
Writing index file PG-adapting.vr
Overfull \hbox (13.29272pt too wide) in paragraph at lines 346--346
 []  @texttt (@textttsl sym-bol name file-extension @texttt [AUTOMODE-REGEXP] [
IGNORED-EXTENSIONS-LIST])[] 
[3] [4] Chapter 2 [5] [6] [7] Chapter 3 [8] [9]
Writing index file PG-adapting.fn
[10] [11] [12] [13]
Underfull \hbox (badness 10000) in paragraph at lines 1172--1179
 @textrm `@texttt proof-script-proof-end-regexp[][]@textrm '[], `@texttt proof-
script-definition-end-regexp[][]@textrm '[] and
[14] [15] [16] Chapter 4 [17] [18] [19] [20] [21] [22] [23]
Underfull \hbox (badness 10000) in paragraph at lines 1810--1812
 []@textrm See also `@texttt proof-shell-eager-annotation-start-length[][]@text
rm '[], `@texttt proof-shell-eager-
[24] [25] [26] Chapter 5 [27] [28] Chapter 6 [29] [30] Chapter 7 [31] [32]
Chapter 8 [33] [34] [35] Chapter 9 [36] Chapter 10 [37] [38] Chapter 11
[39] [40] Chapter 12 [41] [42] [43] [44] [45] [46] Chapter 13 [47] [48]
[49]
Underfull \hbox (badness 10000) in paragraph at lines 3146--3148
 []@textrm Automatically add `@texttt proof-terminal-string[][]@textrm '[] if n
ec-es-sary, ex-am-in-ing
[50] Chapter 14 [51] [52] [53] [54] [55] [56] [57]
Underfull \hbox (badness 10000) in paragraph at lines 3724--3728
 []@textrm Proof ter-mi-na-tor po-si-tions @textsl semis[] @textrm has the form
 re-turned by the func-tion
[58] [59]
Overfull \hbox (47.78485pt too wide) in paragraph at lines 3891--3891
 []  @texttt 'invisible[]                non-script com-mand (`proof-shell-invi
sible-command[][]'[])[] 
[60] [61] [62] [63]
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4170--4170
 [] @texttt 'loopback[]       A com-mand sent from the PA to be in-serted into 
the script[] 
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4192--4192
 [] @texttt 'loopback[]       A com-mand sent from the PA to be in-serted into 
the script[] 
[64] [65] [66] Appendix A [67] [68] [69] Appendix B [70] [71] [72] [73]
Overfull \hbox (85.29668pt too wide) in paragraph at lines 4772--4772
 []   @texttt proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught excep
tion \\|^Exception- "[] 
[74] (Function and Command Index) [75] [76]
No file PG-adapting.fns.
(Variable and User Option Index) [77] [78]
No file PG-adapting.vrs.
(Concept Index) [79] [80]
No file PG-adapting.cps.
[81] [82] (/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc [-1]) [-2]
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc)
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmb10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl1
0.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsltt10.pf
b></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb>
Output written on PG-adapting.pdf (86 pages, 372381 bytes).
Transcript written on PG-adapting.log.
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021) (preloaded format=pdfetex)
 restricted \write18 enabled.
entering extended mode
(./PG-adapting.texi (/usr/share/texlive/texmf-dist/tex/texinfo/texinfo.tex
Loading texinfo [version 2021-04-25.21]: pdf, fonts, glyphs, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, insertions,
(/usr/share/texlive/texmf-dist/tex/generic/epsf/epsf.tex
This is `epsf.tex' v2.7.4 <14 February 2011>
) localization, formatting, and turning on texinfo input format.) </builddir/bu
ild/BUILD/PG-4.5/doc/ProofGeneral-image.jpg> [1{/usr/share/texlive/texmf-var/fo
nts/map/pdftex/updmap/pdftex.map}] [2] (Introduction)
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.aux)
Writing index file PG-adapting.cp
Chapter 1 [1] [2]
Writing index file PG-adapting.vr
Overfull \hbox (13.29272pt too wide) in paragraph at lines 346--346
 []  @texttt (@textttsl sym-bol name file-extension @texttt [AUTOMODE-REGEXP] [
IGNORED-EXTENSIONS-LIST])[] 
[3] [4] Chapter 2 [5] [6] [7] Chapter 3 [8] [9]
Writing index file PG-adapting.fn
[10] [11] [12] [13]
Underfull \hbox (badness 10000) in paragraph at lines 1172--1179
 @textrm `@texttt proof-script-proof-end-regexp[][]@textrm '[], `@texttt proof-
script-definition-end-regexp[][]@textrm '[] and
[14] [15] [16] Chapter 4 [17] [18] [19] [20] [21] [22] [23]
Underfull \hbox (badness 10000) in paragraph at lines 1810--1812
 []@textrm See also `@texttt proof-shell-eager-annotation-start-length[][]@text
rm '[], `@texttt proof-shell-eager-
[24] [25] [26] Chapter 5 [27] [28] Chapter 6 [29] [30] Chapter 7 [31] [32]
Chapter 8 [33] [34] [35] Chapter 9 [36] Chapter 10 [37] [38] Chapter 11
[39] [40] Chapter 12 [41] [42] [43] [44] [45] [46] Chapter 13 [47] [48]
[49]
Underfull \hbox (badness 10000) in paragraph at lines 3146--3148
 []@textrm Automatically add `@texttt proof-terminal-string[][]@textrm '[] if n
ec-es-sary, ex-am-in-ing
[50] Chapter 14 [51] [52] [53] [54] [55] [56] [57]
Underfull \hbox (badness 10000) in paragraph at lines 3724--3728
 []@textrm Proof ter-mi-na-tor po-si-tions @textsl semis[] @textrm has the form
 re-turned by the func-tion
[58] [59]
Overfull \hbox (47.78485pt too wide) in paragraph at lines 3891--3891
 []  @texttt 'invisible[]                non-script com-mand (`proof-shell-invi
sible-command[][]'[])[] 
[60] [61] [62] [63]
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4170--4170
 [] @texttt 'loopback[]       A com-mand sent from the PA to be in-serted into 
the script[] 
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4192--4192
 [] @texttt 'loopback[]       A com-mand sent from the PA to be in-serted into 
the script[] 
[64] [65] [66] Appendix A [67] [68] [69] Appendix B [70] [71] [72] [73]
Overfull \hbox (85.29668pt too wide) in paragraph at lines 4772--4772
 []   @texttt proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught excep
tion \\|^Exception- "[] 
[74] (Function and Command Index) [75] [76]
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.fns)
(Variable and User Option Index) [77] [78]
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.vrs [79]) (Concept Index)
[80] (/builddir/build/BUILD/PG-4.5/doc/PG-adapting.cps) [81] [82]
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc [-1]) [-2]
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc)
(/builddir/build/BUILD/PG-4.5/doc/PG-adapting.toc) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmb10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsltt10.pfb></usr
/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share
/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/tex
mf-dist/fonts/type1/public/amsfonts/cm/cmtt9.pfb>
Output written on PG-adapting.pdf (86 pages, 414463 bytes).
Transcript written on PG-adapting.log.
makeinfo PG-adapting.texi 
PG-adapting.texi:273: warning: @inforef is obsolete.
PG-adapting.texi:670: warning: @inforef is obsolete.
PG-adapting.texi:733: warning: @inforef is obsolete.
PG-adapting.texi:1151: warning: @inforef is obsolete.
PG-adapting.texi:1152: warning: @inforef is obsolete.
PG-adapting.texi:2522: warning: @inforef is obsolete.
make[3]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" doc 
make[3]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
texi2pdf ProofGeneral.texi 
egrep: warning: egrep is obsolescent; using grep -E
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021) (preloaded format=pdfetex)
 restricted \write18 enabled.
entering extended mode
(./ProofGeneral.texi (/usr/share/texlive/texmf-dist/tex/texinfo/texinfo.tex
Loading texinfo [version 2021-04-25.21]: pdf, fonts, glyphs, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, insertions,
(/usr/share/texlive/texmf-dist/tex/generic/epsf/epsf.tex
This is `epsf.tex' v2.7.4 <14 February 2011>
) localization, formatting, and turning on texinfo input format.) </builddir/bu
ild/BUILD/PG-4.5/doc/ProofGeneral-image.jpg> [1{/usr/share/texlive/texmf-var/fo
nts/map/pdftex/updmap/pdftex.map}] [2] (Preface)
Cross reference values unknown; you must run TeX again.
Writing index file ProofGeneral.cp
[1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13]
Writing index file ProofGeneral.fn
Writing index file ProofGeneral.vr
Writing index file ProofGeneral.ky
[14] [15] [16] [17] [18] [19] Chapter 3 [20] [21] [22] [23] [24] [25]
Chapter 4 [26] [27] [28] [29] [30] Chapter 5 [31] [32] [33] [34] Chapter 6
[35] [36] Chapter 7 [37] [38] [39] Chapter 8 [40] [41] [42] [43] [44]
Underfull \hbox (badness 10000) in paragraph at lines 3669--3672
 []@textrm Using a pre-fix ar-gu-ment for `@texttt proof-goto-point[][]@textrm 
'[] (M-x @texttt proof-goto-point[]@textrm ) or
[45] [46] [47] [48] Chapter 9 [49] [50] [51] [52] Chapter 10 [53] [54] [55]
[56] [57] [58] [59] [60] [61] [62] [63]
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4984--4984
 []    @texttt di-rec-tory to be mapped to the log-i-cal path 'path'[] ('-I dir
 -as path').[] 
[64] [65] [66] [67] Chapter 11 [68] Chapter 12 [69] [70] Appendix A [71]
[72] [73] Appendix B [74] (References) [75] [76] (History of Proof General)
[77] [78] [79] [80] [81] (Function and Command Index) [82]
No file ProofGeneral.fns.
(Variable and User Option Index) [83] [84]
No file ProofGeneral.vrs.
(Keystroke Index) [85] [86]
No file ProofGeneral.kys.
(Concept Index) [87] [88]
No file ProofGeneral.cps.
[89] [90] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc [-1] [-2])
[-3] [-4] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc)
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmb10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl9.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsltt10.pfb></usr/share/t
exlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf
-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/
fonts/type1/public/amsfonts/cm/cmtt9.pfb>
Output written on ProofGeneral.pdf (96 pages, 474873 bytes).
Transcript written on ProofGeneral.log.
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021) (preloaded format=pdfetex)
 restricted \write18 enabled.
entering extended mode
(./ProofGeneral.texi (/usr/share/texlive/texmf-dist/tex/texinfo/texinfo.tex
Loading texinfo [version 2021-04-25.21]: pdf, fonts, glyphs, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, insertions,
(/usr/share/texlive/texmf-dist/tex/generic/epsf/epsf.tex
This is `epsf.tex' v2.7.4 <14 February 2011>
) localization, formatting, and turning on texinfo input format.) </builddir/bu
ild/BUILD/PG-4.5/doc/ProofGeneral-image.jpg> [1{/usr/share/texlive/texmf-var/fo
nts/map/pdftex/updmap/pdftex.map}] [2] (Preface)
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.aux)
Writing index file ProofGeneral.cp
[1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13]
Writing index file ProofGeneral.fn
Writing index file ProofGeneral.vr
Writing index file ProofGeneral.ky
[14] [15] [16] [17] [18] [19] Chapter 3 [20] [21] [22] [23] [24] [25]
Chapter 4 [26] [27] [28] [29] [30] Chapter 5 [31] [32] [33] [34] Chapter 6
[35] [36] Chapter 7 [37] [38] [39] Chapter 8 [40] [41] [42] [43] [44]
Underfull \hbox (badness 10000) in paragraph at lines 3669--3672
 []@textrm Using a pre-fix ar-gu-ment for `@texttt proof-goto-point[][]@textrm 
'[] (M-x @texttt proof-goto-point[]@textrm ) or
[45] [46] [47] [48] Chapter 9 [49] [50] [51] [52] Chapter 10 [53] [54] [55]
[56] [57] [58] [59] [60] [61] [62] [63]
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4984--4984
 []    @texttt di-rec-tory to be mapped to the log-i-cal path 'path'[] ('-I dir
 -as path').[] 
[64] [65] [66] [67] Chapter 11 [68] Chapter 12 [69] [70] Appendix A [71]
[72] [73] Appendix B [74] (References) [75] [76] (History of Proof General)
[77] [78] [79] [80] [81] (Function and Command Index) [82]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.fns)
(Variable and User Option Index) [83] [84]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.vrs) (Keystroke Index) [85]
[86] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.kys) (Concept Index)
[87] [88] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.cps [89]) [90]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc [-1] [-2]) [-3] [-4]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc)
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmb10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl9.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsltt10.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmtt9.pfb>
Output written on ProofGeneral.pdf (96 pages, 508224 bytes).
Transcript written on ProofGeneral.log.
This is pdfTeX, Version 3.141592653-2.6-1.40.22 (TeX Live 2021) (preloaded format=pdfetex)
 restricted \write18 enabled.
entering extended mode
(./ProofGeneral.texi (/usr/share/texlive/texmf-dist/tex/texinfo/texinfo.tex
Loading texinfo [version 2021-04-25.21]: pdf, fonts, glyphs, page headings,
tables, conditionals, indexing, sectioning, toc, environments, defuns, macros,
cross references, insertions,
(/usr/share/texlive/texmf-dist/tex/generic/epsf/epsf.tex
This is `epsf.tex' v2.7.4 <14 February 2011>
) localization, formatting, and turning on texinfo input format.) </builddir/bu
ild/BUILD/PG-4.5/doc/ProofGeneral-image.jpg> [1{/usr/share/texlive/texmf-var/fo
nts/map/pdftex/updmap/pdftex.map}] [2] (Preface)
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.aux)
Writing index file ProofGeneral.cp
[1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13]
Writing index file ProofGeneral.fn
Writing index file ProofGeneral.vr
Writing index file ProofGeneral.ky
[14] [15] [16] [17] [18] [19] Chapter 3 [20] [21] [22] [23] [24] [25]
Chapter 4 [26] [27] [28] [29] [30] Chapter 5 [31] [32] [33] [34] Chapter 6
[35] [36] Chapter 7 [37] [38] [39] Chapter 8 [40] [41] [42] [43] [44]
Underfull \hbox (badness 10000) in paragraph at lines 3669--3672
 []@textrm Using a pre-fix ar-gu-ment for `@texttt proof-goto-point[][]@textrm 
'[] (M-x @texttt proof-goto-point[]@textrm ) or
[45] [46] [47] [48] Chapter 9 [49] [50] [51] [52] Chapter 10 [53] [54] [55]
[56] [57] [58] [59] [60] [61] [62] [63]
Overfull \hbox (13.29272pt too wide) in paragraph at lines 4984--4984
 []    @texttt di-rec-tory to be mapped to the log-i-cal path 'path'[] ('-I dir
 -as path').[] 
[64] [65] [66] [67] Chapter 11 [68] Chapter 12 [69] [70] Appendix A [71]
[72] [73] Appendix B [74] (References) [75] [76] (History of Proof General)
[77] [78] [79] [80] [81] (Function and Command Index) [82]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.fns)
(Variable and User Option Index) [83] [84]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.vrs) (Keystroke Index) [85]
[86] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.kys) (Concept Index)
[87] [88] (/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.cps [89]) [90]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc [-1] [-2]) [-3] [-4]
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc)
(/builddir/build/BUILD/PG-4.5/doc/ProofGeneral.toc) )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmb10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmmi12.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/am
sfonts/cm/cmmi9.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/
cm/cmr10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr9.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsl9.pfb></usr/share/texl
ive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsltt10.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/cm/cmtt9.pfb>
Output written on ProofGeneral.pdf (96 pages, 508119 bytes).
Transcript written on ProofGeneral.log.
makeinfo ProofGeneral.texi 
ProofGeneral.texi:726: warning: @inforef is obsolete.
ProofGeneral.texi:1601: warning: @inforef is obsolete.
ProofGeneral.texi:2906: warning: @inforef is obsolete.
ProofGeneral.texi:3002: warning: @inforef is obsolete.
ProofGeneral.texi:3358: warning: @inforef is obsolete.
ProofGeneral.texi:4079: warning: @inforef is obsolete.
ProofGeneral.texi:4123: warning: @inforef is obsolete.
ProofGeneral.texi:4129: warning: @inforef is obsolete.
ProofGeneral.texi:4140: warning: @inforef is obsolete.
ProofGeneral.texi:4149: warning: @inforef is obsolete.
ProofGeneral.texi:4293: warning: @inforef is obsolete.
ProofGeneral.texi:4294: warning: @inforef is obsolete.
ProofGeneral.texi:4315: warning: @inforef is obsolete.
ProofGeneral.texi:4518: warning: @inforef is obsolete.
make[3]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.t2E5Lw
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64 '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64
++ dirname /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64
+ CFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection'
+ export CFLAGS
+ CXXFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection'
+ export CXXFLAGS
+ FFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection -I/usr/lib64/gfortran/modules'
+ export FFLAGS
+ FCFLAGS='-O2 -flto=auto -ffat-lto-objects -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -m64  -mtune=generic -fasynchronous-unwind-tables -fstack-clash-protection -fcf-protection -I/usr/lib64/gfortran/modules'
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed  -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd PG-4.5
+ make EMACS=emacs PREFIX=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr DEST_PREFIX=/usr DESKTOP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share BINDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/bin DOCDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral MANDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/man/man1 INFODIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/info ELISP_START=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/site-start.d ELISP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral DEST_ELISP=/usr/share/emacs/site-lisp/proofgeneral install install-doc
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/16x16/apps
cp etc/desktop/icons/16x16/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/16x16/apps
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/32x32/apps
cp etc/desktop/icons/32x32/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/32x32/apps
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/48x48/apps
cp etc/desktop/icons/48x48/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/48x48/apps
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/64x64/apps
cp etc/desktop/icons/64x64/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/64x64/apps
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/128x128/apps
cp etc/desktop/icons/128x128/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/128x128/apps
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications
cp etc/desktop/proofgeneral.desktop /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/mime-info
cp etc/desktop/mime-info/proofgeneral.mime /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/mime-info
cp etc/desktop/mime-info/proofgeneral.keys /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/mime-info
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/application-registry
cp etc/desktop/application-registry/proofgeneral.applications /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/application-registry
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral
for f in coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib images; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
for f in coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib; do cp -pf $f/*.el /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
for f in images; do cp -prf $f/* /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
for f in ; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
****************************************************************
 Byte compiling... 
****************************************************************
make elc
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5'
make[1]: Nothing to be done for 'elc'.
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5'
****************************************************************
 Finished.
****************************************************************
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral
for f in coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib images; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
for f in coq easycrypt pghaskell pgocaml pgshell phox qrhl generic lib; do cp -pf $f/*.elc /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
for f in ; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done
(bash="`which bash`";					    \
 if [ -z "$bash" ]; then				    \
   echo "Could not find bash - bash paths not checked" >&2; \
   exit 0;						    \
 fi)
(perl="`which perl`";					    \
 if [ -z "$perl" ]; then				    \
   echo "Could not find perl - perl paths not checked" >&2; \
   exit 0;						    \
 fi;							    \
 for i in coq/coqtags; do			    	    \
   sed -i.orig "s|^#.*!.*/bin/perl.*$|#!$perl|" $i;      \
 done)
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/bin
cp -pf coq/coqtags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/bin
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/site-start.d
echo ';;; pg-init.el --- setup for Proof General' > /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el
echo "(setq load-path (append load-path '(\"/usr/share/emacs/site-lisp/proofgeneral/generic\")))" >> /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el
echo "(require 'proof-site)" >> /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el
(cd doc; make EMACS=emacs info)
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" info
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make[2]: Nothing to be done for 'info'.
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" info 
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make[2]: Nothing to be done for 'info'.
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
(cd doc; make EMACS=emacs pdf)
make[1]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" pdf
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make[2]: Nothing to be done for 'pdf'.
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" pdf 
make[2]: Entering directory '/builddir/build/BUILD/PG-4.5/doc'
make[2]: Nothing to be done for 'pdf'.
make[2]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
make[1]: Leaving directory '/builddir/build/BUILD/PG-4.5/doc'
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/man/man1
cp -pf doc/proofgeneral.1 /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/man/man1
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/info
cp -pf doc/*.info /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/info
mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral
for f in AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README doc/*.pdf; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral; done
cp: cannot stat 'README': No such file or directory
for f in pgshell/*.pgsh phox/*.phx; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral/`dirname $f`; cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral/$f; done
+ rm /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral/COPYING /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/doc/proofgeneral/INSTALL
+ desktop-file-validate /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications/proofgeneral.desktop
/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu
/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu
/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu
+ mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/metainfo
+ install -pm 644 /builddir/build/SOURCES/io.github.proofgeneral.metainfo.xml /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/metainfo
+ appstreamcli validate --no-net /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/metainfo/io.github.proofgeneral.metainfo.xml
? Validation was successful: pedantic: 1
+ cp -p /builddir/build/SOURCES/proofgeneral /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/bin
+ install -Dpm 644 /builddir/build/SOURCES/proofgeneral-96x96.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/96x96/apps/proofgeneral.png
+ install -Dpm 644 /builddir/build/SOURCES/proofgeneral-256x256.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/icons/hicolor/256x256/apps/proofgeneral.png
+ /usr/bin/find-debuginfo -j2 --strict-build-id -m -i --build-id-seed 4.5-2.fc38 --unique-debug-suffix -4.5-2.fc38.x86_64 --unique-debug-src-base emacs-common-proofgeneral-4.5-2.fc38.x86_64 --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 110000000 -S debugsourcefiles.list /builddir/build/BUILD/PG-4.5
+ /usr/lib/rpm/check-buildroot
+ /usr/lib/rpm/redhat/brp-ldconfig
+ /usr/lib/rpm/brp-compress
+ /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/check-rpaths
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
*** WARNING: ./usr/share/emacs/site-lisp/proofgeneral/generic/pg-goals.el is executable but has no shebang, removing executable bit
+ /usr/lib/rpm/brp-remove-la-files
+ /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0
+ /usr/lib/rpm/redhat/brp-python-hardlink
Processing files: emacs-common-proofgeneral-4.5-2.fc38.noarch
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.wowHno
+ umask 022
+ cd /builddir/build/BUILD
+ cd PG-4.5
+ LICENSEDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/licenses/emacs-common-proofgeneral
+ export LC_ALL=C
+ LC_ALL=C
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/licenses/emacs-common-proofgeneral
+ cp -pr COPYING /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64/usr/share/licenses/emacs-common-proofgeneral
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: application() application(proofgeneral.desktop) emacs-common-proofgeneral = 4.5-2.fc38 metainfo() metainfo(io.github.proofgeneral.metainfo.xml)
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Requires: /usr/bin/perl /usr/bin/sh
Recommends: prooftree
Processing files: emacs-proofgeneral-4.5-2.fc38.noarch
Provides: emacs-proofgeneral = 4.5-2.fc38 emacs-proofgeneral-el = 4.5-2.fc38
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Obsoletes: emacs-proofgeneral-el < 4.4-11
Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64
Wrote: /builddir/build/RPMS/emacs-common-proofgeneral-4.5-2.fc38.noarch.rpm
Wrote: /builddir/build/RPMS/emacs-proofgeneral-4.5-2.fc38.noarch.rpm
Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.XR7x97
+ umask 022
+ cd /builddir/build/BUILD
+ cd PG-4.5
+ /usr/bin/rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-2.fc38.x86_64
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(rmbuild): /bin/sh -e /var/tmp/rpm-tmp.HxgycU
+ umask 022
+ cd /builddir/build/BUILD
+ rm -rf PG-4.5 PG-4.5.gemspec
+ RPM_EC=0
++ jobs -p
+ exit 0
Child return code was: 0