Mock Version: 3.0 Mock Version: 3.0 Mock Version: 3.0 ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target noarch --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], chrootPath='/var/lib/mock/f37-build-side-32-misc-devel-239183-14080/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=864000uid=996gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target noarch --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;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False warning: line 66: Possible unexpanded macro in: Requires: emacs(bin) >= %{_emacs_version} Building target platforms: noarch Building for target noarch setting SOURCE_DATE_EPOCH=1668816000 Wrote: /builddir/build/SRPMS/emacs-common-proofgeneral-4.5-3.fc37.src.rpm RPM build warnings: line 66: 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 noarch --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], chrootPath='/var/lib/mock/f37-build-side-32-misc-devel-239183-14080/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=timeout=864000uid=996gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False) Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target noarch --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;\\007"', 'PS1': ' \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False Building target platforms: noarch Building for target noarch setting SOURCE_DATE_EPOCH=1668816000 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.t5FtQf + 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 + /usr/lib/rpm/rpmuncompress /builddir/build/SOURCES/pg-4.5-emacs-warning.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.C6brJT + 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 -fasynchronous-unwind-tables -fstack-clash-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 -fasynchronous-unwind-tables -fstack-clash-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 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib/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 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib/gfortran/modules' + export FCFLAGS + 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 ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib: + 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.2/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 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 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.) [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) 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.) [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-dist/fonts/type1/public/amsfonts/cm/cmsltt10.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 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.) [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) 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.) [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) 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.) [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) 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.kpDrST + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch '!=' / ']' + rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch ++ dirname /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch + 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 -fasynchronous-unwind-tables -fstack-clash-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 -fasynchronous-unwind-tables -fstack-clash-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 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib/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 -fasynchronous-unwind-tables -fstack-clash-protection -I/usr/lib/gfortran/modules' + export FCFLAGS + 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 ' + export LDFLAGS + LT_SYS_LIBRARY_PATH=/usr/lib: + 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-3.fc37.noarch/usr DEST_PREFIX=/usr DESKTOP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share BINDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/bin DOCDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/doc/proofgeneral MANDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/man/man1 INFODIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/info ELISP_START=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/emacs/site-lisp/site-start.d ELISP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/share/icons/hicolor/16x16/apps cp etc/desktop/icons/16x16/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/16x16/apps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/32x32/apps cp etc/desktop/icons/32x32/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/32x32/apps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/48x48/apps cp etc/desktop/icons/48x48/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/48x48/apps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/64x64/apps cp etc/desktop/icons/64x64/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/64x64/apps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/128x128/apps cp etc/desktop/icons/128x128/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/icons/hicolor/128x128/apps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/applications cp etc/desktop/proofgeneral.desktop /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/applications mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/mime-info cp etc/desktop/mime-info/proofgeneral.mime /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/mime-info cp etc/desktop/mime-info/proofgeneral.keys /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/mime-info mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/application-registry cp etc/desktop/application-registry/proofgeneral.applications /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/application-registry mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in images; do cp -prf $f/* /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in ; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in ; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/bin cp -pf coq/coqtags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/bin mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/emacs/site-lisp/site-start.d echo ';;; pg-init.el --- setup for Proof General' > /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/share/emacs/site-lisp/site-start.d/pg-init.el echo "(require 'proof-site)" >> /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/share/man/man1 cp -pf doc/proofgeneral.1 /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/man/man1 mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/info cp -pf doc/*.info /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/info mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/usr/share/doc/proofgeneral/`dirname $f`; cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/doc/proofgeneral/$f; done + rm /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/doc/proofgeneral/COPYING /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/doc/proofgeneral/INSTALL + desktop-file-validate /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/applications/proofgeneral.desktop /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/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-3.fc37.noarch/usr/share/metainfo + install -pm 644 /builddir/build/SOURCES/io.github.proofgeneral.metainfo.xml /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/metainfo + appstreamcli validate --no-net /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/bin + install -Dpm 644 /builddir/build/SOURCES/proofgeneral-96x96.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/share/icons/hicolor/256x256/apps/proofgeneral.png + /usr/bin/find-debuginfo -j8 --strict-build-id -m -i --build-id-seed 4.5-3.fc37 --unique-debug-suffix -4.5-3.fc37.noarch --unique-debug-src-base emacs-common-proofgeneral-4.5-3.fc37.noarch --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 -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-3.fc37.noarch Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.4AiCYp + umask 022 + cd /builddir/build/BUILD + cd PG-4.5 + LICENSEDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/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-3.fc37.noarch/usr/share/licenses/emacs-common-proofgeneral + cp -pr COPYING /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch/usr/share/licenses/emacs-common-proofgeneral + RPM_EC=0 ++ jobs -p + exit 0 Provides: application() application(proofgeneral.desktop) emacs-common-proofgeneral = 4.5-3.fc37 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-3.fc37.noarch Provides: emacs-proofgeneral = 4.5-3.fc37 emacs-proofgeneral-el = 4.5-3.fc37 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-3.fc37.noarch Wrote: /builddir/build/RPMS/emacs-common-proofgeneral-4.5-3.fc37.noarch.rpm Wrote: /builddir/build/RPMS/emacs-proofgeneral-4.5-3.fc37.noarch.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.4kPCdw + umask 022 + cd /builddir/build/BUILD + cd PG-4.5 + /usr/bin/rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.5-3.fc37.noarch + RPM_EC=0 ++ jobs -p + exit 0 Executing(rmbuild): /bin/sh -e /var/tmp/rpm-tmp.GFvAcs + 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