Mock Version: 1.2.17 ENTER ['do'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], logger=gid=135uid=1001chrootPath='/var/lib/mock/epel-7-x86_64-mockbuilder-4932/root'timeout=0printOutput=Falseshell=Falseenv={'TERM': 'vt100', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"'}user='mockbuild') Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'] with env {'TERM': 'vt100', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"'} and shell False warning: Could not canonicalize hostname: copr-builder-194381103.novalocal Building target platforms: x86_64 Building for target x86_64 Wrote: /builddir/build/SRPMS/emacs-common-proofgeneral-4.2-5.el7.centos.src.rpm Child return code was: 0 ENTER ['do'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'], logger=gid=135uid=1001chrootPath='/var/lib/mock/epel-7-x86_64-mockbuilder-4932/root'private_network=Truetimeout=0printOutput=Falseshell=Falseenv={'TERM': 'vt100', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"'}user='mockbuild') Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target x86_64 --nodeps /builddir/build/SPECS/emacs-common-proofgeneral.spec'] with env {'TERM': 'vt100', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'LANG': 'en_US.UTF-8', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PROMPT_COMMAND': 'printf "\x1b]0;\x07"'} and shell False Building target platforms: x86_64 Building for target x86_64 Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.hrz3SB + umask 022 + cd /builddir/build/BUILD + cd /builddir/build/BUILD + rm -rf ProofGeneral-4.2 + /usr/bin/gzip -dc /builddir/build/SOURCES/ProofGeneral-4.2.tgz + /usr/bin/tar -xf - + STATUS=0 + '[' 0 -ne 0 ']' + cd ProofGeneral-4.2 + /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w . Patch #0 (pg-4.2-Makefile.patch): + echo 'Patch #0 (pg-4.2-Makefile.patch):' + /usr/bin/cat /builddir/build/SOURCES/pg-4.2-Makefile.patch + /usr/bin/patch -p0 --fuzz=0 patching file Makefile Patch #1 (pg-4.2-desktop.patch): + echo 'Patch #1 (pg-4.2-desktop.patch):' + /usr/bin/cat /builddir/build/SOURCES/pg-4.2-desktop.patch + /usr/bin/patch -p0 --fuzz=0 patching file ./etc/desktop/proofgeneral.desktop Patch #2 (pg-4.2-texinfo.patch): + echo 'Patch #2 (pg-4.2-texinfo.patch):' + /usr/bin/patch -p0 --fuzz=0 + /usr/bin/cat /builddir/build/SOURCES/pg-4.2-texinfo.patch patching file ./doc/PG-adapting.texi patching file ./doc/ProofGeneral.texi + mkdir web + cp -p /builddir/build/SOURCES/ProofGeneralPortrait.eps.gz web + cd doc + epstopdf -f -o=ProofGeneralPortrait.pdf + zcat ProofGeneralPortrait.eps.gz + cd .. + sed -i 's/image{ProofGeneral}/image{ProofGeneralPortrait}/' doc/PG-adapting.texi doc/ProofGeneral.texi + sed -i 's/ (setq byte-compile-error-on-warn t)//' Makefile + exit 0 Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.SRKLj3 + umask 022 + cd /builddir/build/BUILD + cd ProofGeneral-4.2 + chmod 755 isar/isartags + xargs rm -f + find . -name .cvsignore + for f in phox/square-root-2.phx + mv phox/square-root-2.phx phox/square-root-2.phx.old + iconv -f iso-8859-1 -t utf8 phox/square-root-2.phx.old + touch -r phox/square-root-2.phx.old phox/square-root-2.phx + rm phox/square-root-2.phx.old + make clean rm -f acl2/acl2.elc ccc/ccc.elc coq/coq-abbrev.elc coq/coq-autotest.elc coq/coq-db.elc coq/coq-indent.elc coq/coq-local-vars.elc coq/coq-mmm.elc coq/coq-smie-lexer.elc coq/coq-syntax.elc coq/coq-unicode-tokens.elc coq/coq.elc hol98/hol98.elc isar/interface-setup.elc isar/isabelle-system.elc isar/isar-autotest.elc isar/isar-find-theorems.elc isar/isar-keywords.elc isar/isar-mmm.elc isar/isar-profiling.elc isar/isar-syntax.elc isar/isar-unicode-tokens.elc isar/isar.elc lego/lego-syntax.elc lego/lego.elc hol-light/hol-light-autotest.elc hol-light/hol-light-unicode-tokens.elc hol-light/hol-light.elc phox/phox-extraction.elc phox/phox-font.elc phox/phox-fun.elc phox/phox-lang.elc phox/phox-outline.elc phox/phox-pbrpm.elc phox/phox-sym-lock.elc phox/phox-tags.elc phox/phox.elc pgshell/pgshell.elc pgocaml/pgocaml.elc pghaskell/pghashell.elc pghaskell/pghaskell.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-mmm.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 contrib/mmm/mmm-auto.elc contrib/mmm/mmm-class.elc contrib/mmm/mmm-cmds.elc contrib/mmm/mmm-compat.elc contrib/mmm/mmm-cweb.elc contrib/mmm/mmm-mason.elc contrib/mmm/mmm-mode.elc contrib/mmm/mmm-region.elc contrib/mmm/mmm-rpm.elc contrib/mmm/mmm-sample.elc contrib/mmm/mmm-univ.elc contrib/mmm/mmm-utils.elc contrib/mmm/mmm-vars.elc *~ */*~ .\#* */.\#* */.autotest.log */.profile.log (cd doc; make clean) make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" clean make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/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 rm -f *~ make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" clean make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/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 rm -f *~ make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' + make EMACS=emacs compile bashscripts perlscripts doc **************************************************************** Byte compiling... **************************************************************** make elc make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2' emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile acl2/acl2.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/acl2/acl2.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile ccc/ccc.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/ccc/ccc.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-abbrev.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-abbrev.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-autotest.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-autotest.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-db.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-db.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-indent.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-indent.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-local-vars.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-local-vars.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-mmm.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-mmm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-smie-lexer.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-smie-lexer.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-syntax.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-syntax.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq-unicode-tokens.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq-unicode-tokens.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile coq/coq.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/coq/coq.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile hol98/hol98.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/hol98/hol98.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/interface-setup.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/interface-setup.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isabelle-system.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isabelle-system.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-autotest.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-autotest.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-find-theorems.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-find-theorems.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-keywords.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-keywords.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-mmm.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-mmm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-profiling.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-profiling.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-syntax.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-syntax.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar-unicode-tokens.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar-unicode-tokens.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile isar/isar.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-unicode-tokens.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-auxmodes.el") => (load "proof-unicode-tokens.el") Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/isar/isar.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lego/lego-syntax.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lego/lego-syntax.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lego/lego.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/lego/lego.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile hol-light/hol-light-autotest.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/hol-light/hol-light-autotest.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile hol-light/hol-light-unicode-tokens.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/hol-light/hol-light-unicode-tokens.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile hol-light/hol-light.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/hol-light/hol-light.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-extraction.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-extraction.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-font.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-font.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-fun.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-fun.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-lang.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-lang.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-outline.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-outline.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-pbrpm.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-pbrpm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-sym-lock.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-sym-lock.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox-tags.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox-tags.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile phox/phox.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/phox/phox.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile pgshell/pgshell.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/pgshell/pgshell.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile pgocaml/pgocaml.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/pgocaml/pgocaml.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile pghaskell/pghashell.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/pghaskell/pghashell.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile pghaskell/pghaskell.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/pghaskell/pghaskell.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-assoc.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-assoc.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-autotest.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-autotest.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-custom.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-custom.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-goals.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-goals.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-movie.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-movie.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-pamacs.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-pamacs.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-pbrpm.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-pbrpm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-pgip.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-pgip.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-response.el In proof-multiple-frames-enable: generic/pg-response.el:104:23:Warning: `special-display-regexps' is an obsolete variable (as of 24.3); use `display-buffer-alist' instead. generic/pg-response.el:106:28:Warning: `special-display-regexps' is an obsolete variable (as of 24.3); use `display-buffer-alist' instead. generic/pg-response.el:106:28:Warning: `special-display-regexps' is an obsolete variable (as of 24.3); use `display-buffer-alist' instead. Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-response.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-user.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-user.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-vars.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-vars.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/pg-xml.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/pg-xml.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-autoloads.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-autoloads.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-auxmodes.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-auxmodes.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-config.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-config.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-depends.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-depends.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-easy-config.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-easy-config.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-faces.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-faces.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-indent.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-indent.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-maths-menu.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-maths-menu.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-menu.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-menu.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-mmm.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-mmm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-script.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-script.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-shell.el Warning: Eager macro-expansion skipped due to cycle: … => (load "proof-tree.el") => (macroexpand-all …) => (macroexpand (eval-when …)) => (load "proof-shell.el") => (load "proof-tree.el") Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-shell.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-site.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-site.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-splash.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-splash.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-syntax.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-syntax.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-toolbar.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-toolbar.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-tree.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-tree.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-unicode-tokens.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-unicode-tokens.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-useropts.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-useropts.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof-utils.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof-utils.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile generic/proof.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/generic/proof.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/bufhist.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/bufhist.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/holes.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/holes.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/local-vars-list.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/local-vars-list.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/maths-menu.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/maths-menu.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/pg-dev.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/pg-dev.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/pg-fontsets.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/pg-fontsets.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/proof-compat.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/proof-compat.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/scomint.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/scomint.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/span.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/span.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/texi-docstring-magic.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/texi-docstring-magic.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/unicode-chars.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/unicode-chars.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile lib/unicode-tokens.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/lib/unicode-tokens.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-auto.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-auto.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-class.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-class.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-cmds.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-cmds.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-compat.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-compat.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-cweb.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-cweb.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-mason.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-mason.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-mode.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-mode.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-region.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-region.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-rpm.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-rpm.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-sample.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-sample.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-univ.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-univ.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-utils.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-utils.elc emacs --batch --no-site-file -q -eval '(setq load-path (append (mapcar (lambda (d) (concat "/builddir/build/BUILD/ProofGeneral-4.2/" (symbol-name d))) (quote (acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm))) load-path))' -eval '(progn (require (quote bytecomp)) (require (quote mouse)) (require (quote tool-bar)) (require (quote fontset)) (setq byte-compile-warnings (remove (quote cl-functions) (remove (quote noruntime) byte-compile-warning-types))))' -f batch-byte-compile contrib/mmm/mmm-vars.el Wrote /builddir/build/BUILD/ProofGeneral-4.2/contrib/mmm/mmm-vars.elc make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2' **************************************************************** Finished. **************************************************************** (cd doc; make EMACS=emacs ) make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make doc make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" doc make[3]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' texi2pdf PG-adapting.texi This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./PG-adapting.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) <./ProofGener alPortrait.pdf> [1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map} ] [2] [3] (Introduction) Chapter 1 [1] [2] Cross reference values unknown; you must run TeX again. Overfull \hbox (13.29272pt too wide) in paragraph at lines 350--350 [] @texttt (@textttsl sym-bol name file-extension @texttt [AUTOMODE-REGEXP] [ IGNORED-EXTENSIONS-LIST])[] [3] Underfull \hbox (badness 10000) in paragraph at lines 368--369 @texttt (phox "PhoX" "phx") (hol-light "HOL Light" "ml") (pgshell "PG-Shell" " pgsh") [4] Chapter 2 [5] [6] [7] Chapter 3 [8] Underfull \hbox (badness 10000) in paragraph at lines 684--688 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 699--703 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 710--714 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 728--732 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or [9] Underfull \hbox (badness 10000) in paragraph at lines 795--799 @textrm tion in-vokes @texttt <@textrm PA-syntactic-context@texttt > @textrm i f that is de-fined, oth-er-wise it calls [10] [11] [12] [13] [14] [15] Chapter 4 [16] Underfull \hbox (badness 10000) in paragraph at lines 1357--1362 []@textrm If non-nil, when-ever a com-mand is sent to the prover us-ing [17] [18] [19] [20] [21] Overfull \hbox (38.55739pt too wide) in paragraph at lines 1724--1726 []@textrm See also `@texttt proof-shell-eager-annotation-start-length[][]@text rm '[], `@texttt proof-shell-eager-annotation-end[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 1732--1736 []@textrm Must be set to the max-i-mum length of the text that may match [22] Underfull \hbox (badness 10000) in paragraph at lines 1799--1802 []@textrm Note: this should match a string which is bounded by matches on Underfull \hbox (badness 10000) in paragraph at lines 1814--1817 []@textrm This should match a string which is bounded by matches on [23] Underfull \hbox (badness 10000) in paragraph at lines 1866--1870 []@textrm with X Y Z, A B C sep-a-rated by white-space or some-how else (see Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 []@textrm In prac-tice, this func-tion is likely to in-spect the pre-vi-ous (g lobal) vari- Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 @textrm able `@texttt proof-included-files-list[][]@textrm '[] and the match d ata trig-gered by [24] Overfull \hbox (11.36751pt too wide) in paragraph at lines 2005--2011 []@textrm Errors and in-ter-rupts are recog-nised in the func-tion `@texttt pr oof-shell-handle-immediate-output[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 2021--2024 []@textrm The sym-bol will be com-pared against stan-dard ones, see doc-u-men- ta-tion of Chapter 5 [25] [26] Chapter 6 [27] [28] Chapter 7 [29] [30] Chapter 8 [31] [32] [33] Chapter 9 [34] Chapter 10 [35] [36] Chapter 11 [37] [38] Chapter 12 [39] [40] [41] [42] [43] Underfull \hbox (badness 10000) in paragraph at lines 2795--2800 []@textrm Schedule goal up-dates when ex-is-ten-tial vari-ables have changed a nd call [44] Chapter 13 [45] [46] [47] Underfull \hbox (badness 10000) in paragraph at lines 3059--3061 []@textrm Automatically add `@texttt proof-terminal-string[][]@textrm '[] if n ec-es-sary, ex-am-in-ing [48] Chapter 14 [49] [50] [51] [52] [53] [54] [55] Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 []@textrm The op-tional ar-gu-ment @textsl forcedac-tion[] @textrm over-rides the user op-tion Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 @textrm `@texttt proof-auto-action-when-deactivating-scripting[][]@textrm '[] and pre-vents ques-tion-ing Underfull \hbox (badness 10000) in paragraph at lines 3638--3642 []@textrm Proof ter-mi-na-tor po-si-tions @textsl semis[] @textrm has the form re-turned by the func-tion [56] Underfull \hbox (badness 10000) in paragraph at lines 3679--3682 []@textrm Before the re-trac-tion is cal-cu-lated, we en-force the file-level pro-to-col with [57] Underfull \hbox (badness 10000) in paragraph at lines 3794--3800 @textrm tract items `@texttt proof-done-retracting[][]@textrm '[], but there a re more pos-si-bil-i-ties (e.g. Overfull \hbox (47.78485pt too wide) in paragraph at lines 3805--3805 [] @texttt 'invisible[] non-script com-mand (`proof-shell-invi sible-command[][]'[])[] [58] [59] [60] Overfull \hbox (13.29272pt too wide) in paragraph at lines 4055--4055 [] @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 4077--4077 [] @texttt 'loopback[] A com-mand sent from the PA to be in-serted into the script[] [61] Underfull \hbox (badness 8019) in paragraph at lines 4150--4153 []@textrm If goals out-put is found, the last match-ing in-stance, pos-si-bly bounded by [62] Underfull \hbox (badness 10000) in paragraph at lines 4198--4201 @textrm ing `@texttt proof-shell-eager-annotation-start[][]@textrm '[] and end s with text match-ing [63] Appendix A [64] [65] Appendix B [66] [67] [68] [69] Overfull \hbox (85.29668pt too wide) in paragraph at lines 4633--4633 [] @texttt proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught excep tion \\|^Exception- "[] [70] (Function and Command Index) [71] [72] (Variable and User Option Index) [73] [74] (Concept Index) [75] [76] [77] [78] (./PG-adapting.toc [-1]) [-2] (./PG-adapting.toc) (./PG-adapting.toc) ) (see the transcript file for additional information) Output written on PG-adapting.pdf (83 pages, 668232 bytes). Transcript written on PG-adapting.log. This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./PG-adapting.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) (./PG-adapting.aux) <./ProofGeneralPortrait.pdf> [1{/usr/share/texlive/texmf/fo nts/map/pdftex/updmap/pdftex.map}] [2] [3] (Introduction) Chapter 1 [1] [2] Overfull \hbox (13.29272pt too wide) in paragraph at lines 350--350 [] @texttt (@textttsl sym-bol name file-extension @texttt [AUTOMODE-REGEXP] [ IGNORED-EXTENSIONS-LIST])[] [3] Underfull \hbox (badness 10000) in paragraph at lines 368--369 @texttt (phox "PhoX" "phx") (hol-light "HOL Light" "ml") (pgshell "PG-Shell" " pgsh") [4] Chapter 2 [5] [6] [7] Chapter 3 [8] Underfull \hbox (badness 10000) in paragraph at lines 684--688 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 699--703 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 710--714 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 728--732 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or [9] Underfull \hbox (badness 10000) in paragraph at lines 795--799 @textrm tion in-vokes @texttt <@textrm PA-syntactic-context@texttt > @textrm i f that is de-fined, oth-er-wise it calls [10] [11] [12] [13] [14] [15] Chapter 4 [16] Underfull \hbox (badness 10000) in paragraph at lines 1357--1362 []@textrm If non-nil, when-ever a com-mand is sent to the prover us-ing [17] [18] [19] [20] [21] Overfull \hbox (38.55739pt too wide) in paragraph at lines 1724--1726 []@textrm See also `@texttt proof-shell-eager-annotation-start-length[][]@text rm '[], `@texttt proof-shell-eager-annotation-end[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 1732--1736 []@textrm Must be set to the max-i-mum length of the text that may match [22] Underfull \hbox (badness 10000) in paragraph at lines 1799--1802 []@textrm Note: this should match a string which is bounded by matches on Underfull \hbox (badness 10000) in paragraph at lines 1814--1817 []@textrm This should match a string which is bounded by matches on [23] Underfull \hbox (badness 10000) in paragraph at lines 1866--1870 []@textrm with X Y Z, A B C sep-a-rated by white-space or some-how else (see Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 []@textrm In prac-tice, this func-tion is likely to in-spect the pre-vi-ous (g lobal) vari- Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 @textrm able `@texttt proof-included-files-list[][]@textrm '[] and the match d ata trig-gered by [24] Overfull \hbox (11.36751pt too wide) in paragraph at lines 2005--2011 []@textrm Errors and in-ter-rupts are recog-nised in the func-tion `@texttt pr oof-shell-handle-immediate-output[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 2021--2024 []@textrm The sym-bol will be com-pared against stan-dard ones, see doc-u-men- ta-tion of Chapter 5 [25] [26] Chapter 6 [27] [28] Chapter 7 [29] [30] Chapter 8 [31] [32] [33] Chapter 9 [34] Chapter 10 [35] [36] Chapter 11 [37] [38] Chapter 12 [39] [40] [41] [42] [43] Underfull \hbox (badness 10000) in paragraph at lines 2795--2800 []@textrm Schedule goal up-dates when ex-is-ten-tial vari-ables have changed a nd call [44] Chapter 13 [45] [46] [47] Underfull \hbox (badness 10000) in paragraph at lines 3059--3061 []@textrm Automatically add `@texttt proof-terminal-string[][]@textrm '[] if n ec-es-sary, ex-am-in-ing [48] Chapter 14 [49] [50] [51] [52] [53] [54] [55] Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 []@textrm The op-tional ar-gu-ment @textsl forcedac-tion[] @textrm over-rides the user op-tion Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 @textrm `@texttt proof-auto-action-when-deactivating-scripting[][]@textrm '[] and pre-vents ques-tion-ing Underfull \hbox (badness 10000) in paragraph at lines 3638--3642 []@textrm Proof ter-mi-na-tor po-si-tions @textsl semis[] @textrm has the form re-turned by the func-tion [56] Underfull \hbox (badness 10000) in paragraph at lines 3679--3682 []@textrm Before the re-trac-tion is cal-cu-lated, we en-force the file-level pro-to-col with [57] Underfull \hbox (badness 10000) in paragraph at lines 3794--3800 @textrm tract items `@texttt proof-done-retracting[][]@textrm '[], but there a re more pos-si-bil-i-ties (e.g. Overfull \hbox (47.78485pt too wide) in paragraph at lines 3805--3805 [] @texttt 'invisible[] non-script com-mand (`proof-shell-invi sible-command[][]'[])[] [58] [59] [60] Overfull \hbox (13.29272pt too wide) in paragraph at lines 4055--4055 [] @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 4077--4077 [] @texttt 'loopback[] A com-mand sent from the PA to be in-serted into the script[] [61] Underfull \hbox (badness 8019) in paragraph at lines 4150--4153 []@textrm If goals out-put is found, the last match-ing in-stance, pos-si-bly bounded by [62] Underfull \hbox (badness 10000) in paragraph at lines 4198--4201 @textrm ing `@texttt proof-shell-eager-annotation-start[][]@textrm '[] and end s with text match-ing [63] Appendix A [64] [65] Appendix B [66] [67] [68] [69] Overfull \hbox (85.29668pt too wide) in paragraph at lines 4633--4633 [] @texttt proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught excep tion \\|^Exception- "[] [70] (Function and Command Index) [71] [72] (./PG-adapting.fns) (Variable and User Option Index) [73] [74] (./PG-adapting.vrs [75]) (Concept Index) [76] (./PG-adapting.cps) [77] [78] (./PG-adapting.toc [-1]) [-2] (./PG-adapting.toc) (./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 (83 pages, 710827 bytes). Transcript written on PG-adapting.log. This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./PG-adapting.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) (./PG-adapting.aux) <./ProofGeneralPortrait.pdf> [1{/usr/share/texlive/texmf/fo nts/map/pdftex/updmap/pdftex.map}] [2] [3] (Introduction) Chapter 1 [1] [2] Overfull \hbox (13.29272pt too wide) in paragraph at lines 350--350 [] @texttt (@textttsl sym-bol name file-extension @texttt [AUTOMODE-REGEXP] [ IGNORED-EXTENSIONS-LIST])[] [3] Underfull \hbox (badness 10000) in paragraph at lines 368--369 @texttt (phox "PhoX" "phx") (hol-light "HOL Light" "ml") (pgshell "PG-Shell" " pgsh") [4] Chapter 2 [5] [6] [7] Chapter 3 [8] Underfull \hbox (badness 10000) in paragraph at lines 684--688 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 684--688 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 699--703 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 699--703 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 710--714 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 710--714 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or Underfull \hbox (badness 10000) in paragraph at lines 728--732 []@textrm To con-fig-ure com-mand recog-ni-tion prop-erly, you must set at lea st one of Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm these: `@texttt proof-script-sexp-commands[][]@textrm '[], `@texttt pr oof-script-command-end-regexp[][]@textrm '[], Underfull \hbox (badness 10000) in paragraph at lines 728--732 @textrm `@texttt proof-script-command-start-regexp[][]@textrm '[], `@texttt pr oof-terminal-string[][]@textrm '[], or [9] Underfull \hbox (badness 10000) in paragraph at lines 795--799 @textrm tion in-vokes @texttt <@textrm PA-syntactic-context@texttt > @textrm i f that is de-fined, oth-er-wise it calls [10] [11] [12] [13] [14] [15] Chapter 4 [16] Underfull \hbox (badness 10000) in paragraph at lines 1357--1362 []@textrm If non-nil, when-ever a com-mand is sent to the prover us-ing [17] [18] [19] [20] [21] Overfull \hbox (38.55739pt too wide) in paragraph at lines 1724--1726 []@textrm See also `@texttt proof-shell-eager-annotation-start-length[][]@text rm '[], `@texttt proof-shell-eager-annotation-end[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 1732--1736 []@textrm Must be set to the max-i-mum length of the text that may match [22] Underfull \hbox (badness 10000) in paragraph at lines 1799--1802 []@textrm Note: this should match a string which is bounded by matches on Underfull \hbox (badness 10000) in paragraph at lines 1814--1817 []@textrm This should match a string which is bounded by matches on [23] Underfull \hbox (badness 10000) in paragraph at lines 1866--1870 []@textrm with X Y Z, A B C sep-a-rated by white-space or some-how else (see Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 []@textrm In prac-tice, this func-tion is likely to in-spect the pre-vi-ous (g lobal) vari- Underfull \hbox (badness 10000) in paragraph at lines 1927--1930 @textrm able `@texttt proof-included-files-list[][]@textrm '[] and the match d ata trig-gered by [24] Overfull \hbox (11.36751pt too wide) in paragraph at lines 2005--2011 []@textrm Errors and in-ter-rupts are recog-nised in the func-tion `@texttt pr oof-shell-handle-immediate-output[][]@textrm '[]. Underfull \hbox (badness 10000) in paragraph at lines 2021--2024 []@textrm The sym-bol will be com-pared against stan-dard ones, see doc-u-men- ta-tion of Chapter 5 [25] [26] Chapter 6 [27] [28] Chapter 7 [29] [30] Chapter 8 [31] [32] [33] Chapter 9 [34] Chapter 10 [35] [36] Chapter 11 [37] [38] Chapter 12 [39] [40] [41] [42] [43] Underfull \hbox (badness 10000) in paragraph at lines 2795--2800 []@textrm Schedule goal up-dates when ex-is-ten-tial vari-ables have changed a nd call [44] Chapter 13 [45] [46] [47] Underfull \hbox (badness 10000) in paragraph at lines 3059--3061 []@textrm Automatically add `@texttt proof-terminal-string[][]@textrm '[] if n ec-es-sary, ex-am-in-ing [48] Chapter 14 [49] [50] [51] [52] [53] [54] [55] Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 []@textrm The op-tional ar-gu-ment @textsl forcedac-tion[] @textrm over-rides the user op-tion Underfull \hbox (badness 10000) in paragraph at lines 3598--3603 @textrm `@texttt proof-auto-action-when-deactivating-scripting[][]@textrm '[] and pre-vents ques-tion-ing Underfull \hbox (badness 10000) in paragraph at lines 3638--3642 []@textrm Proof ter-mi-na-tor po-si-tions @textsl semis[] @textrm has the form re-turned by the func-tion [56] Underfull \hbox (badness 10000) in paragraph at lines 3679--3682 []@textrm Before the re-trac-tion is cal-cu-lated, we en-force the file-level pro-to-col with [57] Underfull \hbox (badness 10000) in paragraph at lines 3794--3800 @textrm tract items `@texttt proof-done-retracting[][]@textrm '[], but there a re more pos-si-bil-i-ties (e.g. Overfull \hbox (47.78485pt too wide) in paragraph at lines 3805--3805 [] @texttt 'invisible[] non-script com-mand (`proof-shell-invi sible-command[][]'[])[] [58] [59] [60] Overfull \hbox (13.29272pt too wide) in paragraph at lines 4055--4055 [] @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 4077--4077 [] @texttt 'loopback[] A com-mand sent from the PA to be in-serted into the script[] [61] Underfull \hbox (badness 8019) in paragraph at lines 4150--4153 []@textrm If goals out-put is found, the last match-ing in-stance, pos-si-bly bounded by [62] Underfull \hbox (badness 10000) in paragraph at lines 4198--4201 @textrm ing `@texttt proof-shell-eager-annotation-start[][]@textrm '[] and end s with text match-ing [63] Appendix A [64] [65] Appendix B [66] [67] [68] [69] Overfull \hbox (85.29668pt too wide) in paragraph at lines 4633--4633 [] @texttt proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught excep tion \\|^Exception- "[] [70] (Function and Command Index) [71] [72] (./PG-adapting.fns) (Variable and User Option Index) [73] [74] (./PG-adapting.vrs [75]) (Concept Index) [76] (./PG-adapting.cps) [77] [78] (./PG-adapting.toc [-1]) [-2] (./PG-adapting.toc) (./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 (83 pages, 710827 bytes). Transcript written on PG-adapting.log. makeinfo PG-adapting.texi make[3]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" doc make[3]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' texi2pdf ProofGeneral.texi This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./ProofGeneral.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) <./ProofGener alPortrait.pdf> [1{/usr/share/texlive/texmf/fonts/map/pdftex/updmap/pdftex.map} ] [2] [3] (Preface) Cross reference values unknown; you must run TeX again. [1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] Underfull \hbox (badness 10000) in paragraph at lines 1666--1670 []@textsl warning[]@textrm : this com-mand risks spoil-ing syn-chro-niza-tion if the test [18] Chapter 3 [19] [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] Chapter 8 [39] [40] [41] [42] [43] [44] Underfull \hbox (badness 10000) in paragraph at lines 3597--3600 []@textrm This op-tion is com-pat-i-ble with `@texttt proof-prog-name-ask[][]@ textrm '[]. No ef-fect if [45] [46] [47] Chapter 9 [48] [49] [50] Chapter 10 [51] [52] Chapter 11 [53] [54] [55] [56] [57] Underfull \hbox (badness 10000) in paragraph at lines 4512--4514 []@textrm After the sub-sti-tu-tion the com-mand can be changed in the mini-bu f-fer if Underfull \hbox (badness 10000) in paragraph at lines 4522--4524 []@textrm This op-tion can be set/reset via menu `@texttt Coq -> Settings -> C onfirm External [58] [59] [60] Chapter 12 [61] [62] [63] [64] Chapter 13 [65] [66] Chapter 14 [67] [68] Appendix A [69] [70] [71] Appendix B [72] (References) [73] [74] (History of Proof General) [75] [76] [77] [78] [79] (Function and Command Index) [80] (Variable and User Option Index) [81] [82] (Keystroke Index) [83] [84] (Concept Index) [85] [86] [87] [88] (./ProofGeneral.toc [-1] [-2]) [-3] [-4] (./ProofGeneral.toc) (./ProofGeneral.toc) ) (see the transcript file for additional information){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-t1.enc} Output written on ProofGeneral.pdf (95 pages, 762658 bytes). Transcript written on ProofGeneral.log. This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./ProofGeneral.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) (./ProofGeneral.aux) <./ProofGeneralPortrait.pdf> [1{/usr/share/texlive/texmf/f onts/map/pdftex/updmap/pdftex.map}] [2] [3] (Preface) [1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] Underfull \hbox (badness 10000) in paragraph at lines 1666--1670 []@textsl warning[]@textrm : this com-mand risks spoil-ing syn-chro-niza-tion if the test [18] Chapter 3 [19] [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] Chapter 8 [39] [40] [41] [42] [43] [44] Underfull \hbox (badness 10000) in paragraph at lines 3597--3600 []@textrm This op-tion is com-pat-i-ble with `@texttt proof-prog-name-ask[][]@ textrm '[]. No ef-fect if [45] [46] [47] Chapter 9 [48] [49] [50] Chapter 10 [51] [52] Chapter 11 [53] [54] [55] [56] [57] Underfull \hbox (badness 10000) in paragraph at lines 4512--4514 []@textrm After the sub-sti-tu-tion the com-mand can be changed in the mini-bu f-fer if Underfull \hbox (badness 10000) in paragraph at lines 4522--4524 []@textrm This op-tion can be set/reset via menu `@texttt Coq -> Settings -> C onfirm External [58] [59] [60] Chapter 12 [61] [62] [63] [64] Chapter 13 [65] [66] Chapter 14 [67] [68] Appendix A [69] [70] [71] Appendix B [72] (References) [73] [74] (History of Proof General) [75] [76] [77] [78] [79] (Function and Command Index) [80] (./ProofGeneral.fns) (Variable and User Option Index) [81] [82] (./ProofGeneral.vrs) (Keystroke Index) [83] [84] (./ProofGeneral.kys) (Concept Index) [85] [86] (./ProofGeneral.cps [87]) [88] (./ProofGeneral.toc [-1] [-2]) [-3] [-4] (./ProofGeneral.toc) (./ProofGeneral.toc) ) (see the transcript file for additional information){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-t1.enc} Output written on ProofGeneral.pdf (95 pages, 799044 bytes). Transcript written on ProofGeneral.log. This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./ProofGeneral.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) (./ProofGeneral.aux) <./ProofGeneralPortrait.pdf> [1{/usr/share/texlive/texmf/f onts/map/pdftex/updmap/pdftex.map}] [2] [3] (Preface) [1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] Underfull \hbox (badness 10000) in paragraph at lines 1666--1670 []@textsl warning[]@textrm : this com-mand risks spoil-ing syn-chro-niza-tion if the test [18] Chapter 3 [19] [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] Chapter 8 [39] [40] [41] [42] [43] [44] Underfull \hbox (badness 10000) in paragraph at lines 3597--3600 []@textrm This op-tion is com-pat-i-ble with `@texttt proof-prog-name-ask[][]@ textrm '[]. No ef-fect if [45] [46] [47] Chapter 9 [48] [49] [50] Chapter 10 [51] [52] Chapter 11 [53] [54] [55] [56] [57] Underfull \hbox (badness 10000) in paragraph at lines 4512--4514 []@textrm After the sub-sti-tu-tion the com-mand can be changed in the mini-bu f-fer if Underfull \hbox (badness 10000) in paragraph at lines 4522--4524 []@textrm This op-tion can be set/reset via menu `@texttt Coq -> Settings -> C onfirm External [58] [59] [60] Chapter 12 [61] [62] [63] [64] Chapter 13 [65] [66] Chapter 14 [67] [68] Appendix A [69] [70] [71] Appendix B [72] (References) [73] [74] (History of Proof General) [75] [76] [77] [78] [79] (Function and Command Index) [80] (./ProofGeneral.fns) (Variable and User Option Index) [81] [82] (./ProofGeneral.vrs) (Keystroke Index) [83] [84] (./ProofGeneral.kys) (Concept Index) [85] [86] (./ProofGeneral.cps [87]) [88] (./ProofGeneral.toc [-1] [-2]) [-3] [-4] (./ProofGeneral.toc) (./ProofGeneral.toc) ) (see the transcript file for additional information){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-t1.enc} Output written on ProofGeneral.pdf (95 pages, 799036 bytes). Transcript written on ProofGeneral.log. This is pdfTeX, Version 3.1415926-2.5-1.40.14 (TeX Live 2013) restricted \write18 enabled. entering extended mode (./ProofGeneral.texi (/usr/share/texlive/texmf-local/texmf-compat/tex/texinfo/texinfo.tex Loading texinfo [version 2013-02-01.11]: pdf, fonts, markup, 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.) (./ProofGeneral.aux) <./ProofGeneralPortrait.pdf> [1{/usr/share/texlive/texmf/f onts/map/pdftex/updmap/pdftex.map}] [2] [3] (Preface) [1] [2] Chapter 1 [3] [4] [5] [6] [7] Chapter 2 [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] Underfull \hbox (badness 10000) in paragraph at lines 1666--1670 []@textsl warning[]@textrm : this com-mand risks spoil-ing syn-chro-niza-tion if the test [18] Chapter 3 [19] [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] Chapter 8 [39] [40] [41] [42] [43] [44] Underfull \hbox (badness 10000) in paragraph at lines 3597--3600 []@textrm This op-tion is com-pat-i-ble with `@texttt proof-prog-name-ask[][]@ textrm '[]. No ef-fect if [45] [46] [47] Chapter 9 [48] [49] [50] Chapter 10 [51] [52] Chapter 11 [53] [54] [55] [56] [57] Underfull \hbox (badness 10000) in paragraph at lines 4512--4514 []@textrm After the sub-sti-tu-tion the com-mand can be changed in the mini-bu f-fer if Underfull \hbox (badness 10000) in paragraph at lines 4522--4524 []@textrm This op-tion can be set/reset via menu `@texttt Coq -> Settings -> C onfirm External [58] [59] [60] Chapter 12 [61] [62] [63] [64] Chapter 13 [65] [66] Chapter 14 [67] [68] Appendix A [69] [70] [71] Appendix B [72] (References) [73] [74] (History of Proof General) [75] [76] [77] [78] [79] (Function and Command Index) [80] (./ProofGeneral.fns) (Variable and User Option Index) [81] [82] (./ProofGeneral.vrs) (Keystroke Index) [83] [84] (./ProofGeneral.kys) (Concept Index) [85] [86] (./ProofGeneral.cps [87]) [88] (./ProofGeneral.toc [-1] [-2]) [-3] [-4] (./ProofGeneral.toc) (./ProofGeneral.toc) ) (see the transcript file for additional information){/usr/share/texlive/texmf-d ist/fonts/enc/dvips/cm-super/cm-super-t1.enc} Output written on ProofGeneral.pdf (95 pages, 799036 bytes). Transcript written on ProofGeneral.log. makeinfo ProofGeneral.texi make[3]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' + sed -r -e 's|^EMACS_LISPDIR=.*$|EMACS_LISPDIR=/usr/share/emacs/site-lisp|' -e 's|^PACKAGE=.*$|PACKAGE=proofgeneral|' -e 's|^(PGHOMEDEFAULT=).*|\1/usr/share/emacs/site-lisp/proofgeneral|' bin/proofgeneral + touch -r bin/proofgeneral .tmp + mv -f .tmp bin/proofgeneral + mkdir emacs ++ find . -maxdepth 1 -mindepth 1 '!' -name emacs + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./Makefile emacs/./Makefile + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./web emacs/./web + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./README emacs/./README + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./contrib emacs/./contrib + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./AUTHORS emacs/./AUTHORS + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./obsolete emacs/./obsolete + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./INSTALL emacs/./INSTALL + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./etc emacs/./etc + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./lego emacs/./lego + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./twelf emacs/./twelf + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./hol98 emacs/./hol98 + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./phox emacs/./phox + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./COMPATIBILITY emacs/./COMPATIBILITY + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./COPYING emacs/./COPYING + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./pgshell emacs/./pgshell + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./BUGS emacs/./BUGS + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./generic emacs/./generic + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./FAQ emacs/./FAQ + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./pghaskell emacs/./pghaskell + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./pgocaml emacs/./pgocaml + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./hol-light emacs/./hol-light + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./images emacs/./images + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./isar emacs/./isar + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./lib emacs/./lib + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./CHANGES emacs/./CHANGES + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./doc emacs/./doc + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./coq emacs/./coq + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./ccc emacs/./ccc + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./REGISTER emacs/./REGISTER + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./acl2 emacs/./acl2 + for f in '`find . -maxdepth 1 -mindepth 1 ! -name emacs`' + cp -pr ./bin emacs/./bin + exit 0 Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.NSoYXJ + umask 022 + cd /builddir/build/BUILD + '[' /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 '!=' / ']' + rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 ++ dirname /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 + mkdir -p /builddir/build/BUILDROOT + mkdir /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 + cd ProofGeneral-4.2 ++ find emacs/ -maxdepth 1 -mindepth 1 + cp -pr emacs/bin emacs/acl2 emacs/REGISTER emacs/ccc emacs/coq emacs/doc emacs/CHANGES emacs/lib emacs/isar emacs/images emacs/hol-light emacs/pgocaml emacs/pghaskell emacs/FAQ emacs/generic emacs/BUGS emacs/pgshell emacs/COPYING emacs/COMPATIBILITY emacs/phox emacs/hol98 emacs/twelf emacs/lego emacs/etc emacs/INSTALL emacs/obsolete emacs/AUTHORS emacs/contrib emacs/README emacs/web emacs/Makefile . + make EMACS=emacs PREFIX=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr DEST_PREFIX=/usr DESKTOP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share BINDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin DOCDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral MANDIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/man/man1 INFODIR=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/info ELISP_START=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/site-start.d ELISP=/builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral DEST_ELISP=/usr/share/emacs/site-lisp/proofgeneral install install-doc mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/16x16 cp etc/desktop/icons/16x16/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/16x16 mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/32x32 cp etc/desktop/icons/32x32/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/32x32 mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/48x48 cp etc/desktop/icons/48x48/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/icons/hicolor/48x48 mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/pixmaps cp etc/desktop/icons/48x48/proofgeneral.png /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/pixmaps mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications cp etc/desktop/proofgeneral.desktop /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/mime-info cp etc/desktop/mime-info/proofgeneral.mime /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/mime-info cp etc/desktop/mime-info/proofgeneral.keys /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/mime-info mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/application-registry cp etc/desktop/application-registry/proofgeneral.applications /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/application-registry mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral for f in acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm images; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm; do cp -pf $f/*.el /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in images; do cp -prf $f/* /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in isar/interface isar/isartags; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done **************************************************************** Byte compiling... **************************************************************** make elc make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2' make[1]: Nothing to be done for `elc'. make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2' **************************************************************** Finished. **************************************************************** mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral for f in acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm images; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell generic lib contrib/mmm; do cp -pf $f/*.elc /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done for f in isar/interface isar/isartags; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/proofgeneral/$f; done mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin cp -pf bin/proofgeneral lego/legotags coq/coqtags isar/isartags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/site-start.d echo ';;; pg-init.el --- setup for Proof General' > /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el echo "(setq load-path (append load-path '(\"/usr/share/emacs/site-lisp/proofgeneral/generic\")))" >> /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el echo "(require 'proof-site)" >> /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/emacs/site-lisp/site-start.d/pg-init.el (cd doc; make EMACS=emacs info) make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" info make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[2]: Nothing to be done for `info'. make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" info make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[2]: Nothing to be done for `info'. make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' (cd doc; make EMACS=emacs pdf) make[1]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc" pdf make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[2]: Nothing to be done for `pdf'. make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc" pdf make[2]: Entering directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[2]: Nothing to be done for `pdf'. make[2]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' make[1]: Leaving directory `/builddir/build/BUILD/ProofGeneral-4.2/doc' mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/man/man1 cp -pf doc/proofgeneral.1 /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/man/man1 mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/info cp -pf doc/*.info /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/info mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral for f in AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER doc/*.pdf; do cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral; done for f in acl2/*.acl2 hol98/*.sml isar/*.thy lclam/*.lcm lego/*.l pgshell/*.pgsh phox/*.phx plastic/*.lf twelf/*.elf; do mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral/`dirname $f`; cp -pf $f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral/$f; done cp: cannot stat 'lclam/*.lcm': No such file or directory cp: cannot stat 'plastic/*.lf': No such file or directory + rm -f /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/info/dir + rmdir /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral/lclam /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/doc/proofgeneral/plastic + chmod a+x /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin/coqtags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin/isartags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin/legotags /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/bin/proofgeneral + desktop-file-validate /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications/proofgeneral.desktop /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/applications/proofgeneral.desktop: hint: value "Development;IDE;Utility;TextEditor;Education;Science;Math;" for key "Categories" in group "Desktop Entry" contains more than one main category; application might appear more than once in the application menu + mkdir -p /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/appdata + install -pm 644 /builddir/build/SOURCES/proofgeneral.appdata.xml /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64/usr/share/appdata + /usr/lib/rpm/find-debuginfo.sh --strict-build-id -m --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 110000000 /builddir/build/BUILD/ProofGeneral-4.2 /usr/lib/rpm/sepdebugcrcfix: Updated 0 CRC32s, 0 CRC32s did match. + /usr/lib/rpm/check-buildroot + /usr/lib/rpm/redhat/brp-compress + /usr/lib/rpm/redhat/brp-strip-static-archive /usr/bin/strip + /usr/lib/rpm/brp-python-bytecompile /usr/bin/python 1 + /usr/lib/rpm/redhat/brp-python-hardlink + /usr/lib/rpm/redhat/brp-java-repack-jars Processing files: emacs-common-proofgeneral-4.2-5.el7.centos.noarch Provides: appdata() appdata(proofgeneral.appdata.xml) application() application(proofgeneral.desktop) emacs-common-proofgeneral = 4.2-5.el7.centos Requires(interp): /bin/sh /bin/sh /bin/sh /bin/sh Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Requires(post): /bin/sh Requires(preun): /bin/sh Requires(postun): /bin/sh Requires(posttrans): /bin/sh Requires: /bin/sh /usr/bin/perl Processing files: emacs-proofgeneral-4.2-5.el7.centos.noarch Provides: emacs-proofgeneral = 4.2-5.el7.centos Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Requires: /usr/bin/env /usr/bin/perl Processing files: emacs-proofgeneral-el-4.2-5.el7.centos.noarch Provides: emacs-proofgeneral-el = 4.2-5.el7.centos Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1 Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 Wrote: /builddir/build/RPMS/emacs-common-proofgeneral-4.2-5.el7.centos.noarch.rpm Wrote: /builddir/build/RPMS/emacs-proofgeneral-4.2-5.el7.centos.noarch.rpm Wrote: /builddir/build/RPMS/emacs-proofgeneral-el-4.2-5.el7.centos.noarch.rpm Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.npqJAX + umask 022 + cd /builddir/build/BUILD + cd ProofGeneral-4.2 + /usr/bin/rm -rf /builddir/build/BUILDROOT/emacs-common-proofgeneral-4.2-5.el7.centos.x86_64 + exit 0 Child return code was: 0