Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Trouble recompiling ProogGeneral

view this post on Zulip Email Gateway (Aug 18 2022 at 09:59):

From: clefort <ipub@charter.net>
Hello, again,

Again, when I make clean and make compile in proofgeneral folder it
gives me the message that

Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/
ProofGeneral-3.6/x-symbol/lisp/x-symbol-hooks.el:
!! Symbol's function definition is void ((set-fontset-font))
Done
make[1]: *** [x-symbol-hooks.elc] Error 1
make: *** [.byte-compile] Error 2
24-182-155-183:~/ISABELLE_HOME/clintonlefort/Proofgeneral/
ProofGeneral-3.6 clintonlefort$

Below is the terminal data.

24-182-155-183:~/ISABELLE_HOME/clintonlefort/Proofgeneral/
ProofGeneral-3.6 clintonlefort$ make compile EMACS=emacs

Byte compiling...

rm -f acl2/acl2.elc acl2/x-symbol-acl2.elc coq/coq-abbrev.elc coq/coq-
autotest.elc coq/coq-indent.elc coq/coq-syntax.elc coq/coq.elc coq/x-
symbol-coq.elc demoisa/demoisa-easy.elc demoisa/demoisa.elc generic/
pg-assoc.elc generic/pg-autotest.elc generic/pg-goals.elc generic/pg-
pbrpm.elc generic/pg-pgip-old.elc generic/pg-pgip.elc generic/pg-
resolve.elc generic/pg-response.elc generic/pg-thymodes.elc generic/
pg-user.elc generic/pg-xhtml.elc generic/pg-xml.elc generic/proof-
autoloads.elc generic/proof-config.elc generic/proof-depends.elc
generic/proof-easy-config.elc generic/proof-indent.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-system.elc generic/proof-toolbar.elc
generic/proof-utils.elc generic/proof-x-symbol.elc generic/proof.elc
hol98/hol98.elc hol98/x-symbol-hol98.elc isa/interface-setup.elc isa/
isa-syntax.elc isa/isa.elc isa/isabelle-system.elc isa/thy-mode.elc
isa/x-symbol-isa.elc isa/x-symbol-isabelle.elc isar/isar-autotest.elc
isar/isar-keywords.elc isar/isar-mmm.elc isar/isar-syntax.elc isar/
isar.elc isar/x-symbol-isar.elc lclam/lclam.elc lego/lego-syntax.elc
lego/lego.elc lego/x-symbol-lego.elc lib/holes-load.elc lib/holes.elc
lib/proof-compat.elc lib/span-extent.elc lib/span-overlay.elc lib/
span.elc lib/texi-docstring-magic.elc lib/xml-fixed.elc mmm/mmm-
auto.elc mmm/mmm-class.elc mmm/mmm-cmds.elc mmm/mmm-compat.elc mmm/
mmm-mason.elc mmm/mmm-mode.elc mmm/mmm-region.elc mmm/mmm-rpm.elc mmm/
mmm-sample.elc mmm/mmm-univ.elc mmm/mmm-utils.elc mmm/mmm-vars.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-
tags.elc phox/phox.elc phox/x-symbol-phox.elc plastic/plastic-
syntax.elc plastic/plastic.elc twelf/twelf-font.elc twelf/twelf-
old.elc twelf/twelf.elc twelf/x-symbol-twelf.elc x-symbol/lisp/
_pkg.elc x-symbol/lisp/auto-autoloads.elc x-symbol/lisp/custom-
load.elc x-symbol/lisp/x-symbol-bib.elc x-symbol/lisp/x-symbol-
emacs.elc x-symbol/lisp/x-symbol-hooks.elc x-symbol/lisp/x-symbol-
image.elc x-symbol/lisp/x-symbol-macs.elc x-symbol/lisp/x-symbol-
mule.elc x-symbol/lisp/x-symbol-nomule.elc x-symbol/lisp/x-symbol-
sgml.elc x-symbol/lisp/x-symbol-tex.elc x-symbol/lisp/x-symbol-
texi.elc x-symbol/lisp/x-symbol-vars.elc x-symbol/lisp/x-symbol-
xmacs.elc x-symbol/lisp/x-symbol.elc
emacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar
(lambda (d) (concat "/Users/clintonlefort/ISABELLE_HOME/clintonlefort/
ProofGeneral/ProofGeneral-3.6/" (symbol-name d))) (quote (acl2 coq
demoisa generic hol98 isa isar lclam lego lib mmm phox plastic twelf
x-symbol/lisp))) load-path))' -f batch-byte-compile acl2/acl2.el acl2/
x-symbol-acl2.el coq/coq-abbrev.el coq/coq-autotest.el coq/coq-
indent.el coq/coq-syntax.el coq/coq.el coq/x-symbol-coq.el demoisa/
demoisa-easy.el demoisa/demoisa.el generic/pg-assoc.el generic/pg-
autotest.el generic/pg-goals.el generic/pg-pbrpm.el generic/pg-pgip-
old.el generic/pg-pgip.el generic/pg-resolve.el generic/pg-
response.el generic/pg-thymodes.el generic/pg-user.el generic/pg-
xhtml.el generic/pg-xml.el generic/proof-autoloads.el generic/proof-
config.el generic/proof-depends.el generic/proof-easy-config.el
generic/proof-indent.el generic/proof-menu.el generic/proof-mmm.el
generic/proof-script.el generic/proof-shell.el generic/proof-site.el
generic/proof-splash.el generic/proof-syntax.el generic/proof-
system.el generic/proof-toolbar.el generic/proof-utils.el generic/
proof-x-symbol.el generic/proof.el hol98/hol98.el hol98/x-symbol-
hol98.el isa/interface-setup.el isa/isa-syntax.el isa/isa.el isa/
isabelle-system.el isa/thy-mode.el isa/x-symbol-isa.el isa/x-symbol-
isabelle.el isar/isar-autotest.el isar/isar-keywords.el isar/isar-
mmm.el isar/isar-syntax.el isar/isar.el isar/x-symbol-isar.el lclam/
lclam.el lego/lego-syntax.el lego/lego.el lego/x-symbol-lego.el lib/
holes-load.el lib/holes.el lib/proof-compat.el lib/span-extent.el lib/
span-overlay.el lib/span.el lib/texi-docstring-magic.el lib/xml-
fixed.el mmm/mmm-auto.el mmm/mmm-class.el mmm/mmm-cmds.el mmm/mmm-
compat.el mmm/mmm-mason.el mmm/mmm-mode.el mmm/mmm-region.el mmm/mmm-
rpm.el mmm/mmm-sample.el mmm/mmm-univ.el mmm/mmm-utils.el mmm/mmm-
vars.el phox/phox-extraction.el phox/phox-font.el phox/phox-fun.el
phox/phox-lang.el phox/phox-outline.el phox/phox-pbrpm.el phox/phox-
tags.el phox/phox.el phox/x-symbol-phox.el plastic/plastic-syntax.el
plastic/plastic.el twelf/twelf-font.el twelf/twelf-old.el twelf/
twelf.el twelf/x-symbol-twelf.el x-symbol/lisp/_pkg.el x-symbol/lisp/
auto-autoloads.el x-symbol/lisp/custom-load.el x-symbol/lisp/x-symbol-
bib.el x-symbol/lisp/x-symbol-emacs.el x-symbol/lisp/x-symbol-
hooks.el x-symbol/lisp/x-symbol-image.el x-symbol/lisp/x-symbol-
macs.el x-symbol/lisp/x-symbol-mule.el x-symbol/lisp/x-symbol-
nomule.el x-symbol/lisp/x-symbol-sgml.el x-symbol/lisp/x-symbol-
tex.el x-symbol/lisp/x-symbol-texi.el x-symbol/lisp/x-symbol-vars.el
x-symbol/lisp/x-symbol-xmacs.el x-symbol/lisp/x-symbol.el

Loading /usr/libexec/emacs/21.2/powerpc-apple-darwin8.0/fns-21.2.1.el
(source)...
Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/
ProofGeneral-3.6/acl2/acl2.elc
Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/
ProofGeneral-3.6/acl2/x-symbol-acl2.elc
Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/
ProofGeneral-3.6/coq/coq-abbrev.elc
Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/
ProofGeneral-3.6/coq/coq-autotest.elc

While compiling the end of the data in file /Users/clintonlefort/
ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq-
indent.el:
** The function proof-indent-pad-eol' is not known to be defined. Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/ ProofGeneral-3.6/coq/coq-indent.elc While compiling toplevel forms in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq- syntax.el: ** reference to free variable coq-prog-name Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/ ProofGeneral-3.6/coq/coq-syntax.elc While compiling proofstack in file /Users/clintonlefort/ISABELLE_HOME/ clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** function proofstack defined multiple times in this file ** function proofstack defined multiple times in this file While compiling toplevel forms in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** assignment to free variable tags-always-exact ** function coq-PrintHint defined multiple times in this file While compiling toplevel forms in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** reference to free variable coq-keymap ** reference to free variable coq-translate-to-v8 While compiling coq-mode-config in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** assignment to free variable comment-quote-nested ** assignment to free variable outline-heading-end-regexp ** reference to free variable tag-table-alist ** assignment to free variable tag-table-alist ** reference to free variable coq-require-command-regexp While compiling coq-maybe-compile-buffer in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** reference to free variable coq-auto-compile-vos ** reference to free variable buffer ** reference to free variable compile-command While compiling coq-process-file in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** reference to free variable coq-auto-compile-vos While compiling coq-preprocessing in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** reference to free variable coq-time-commands ** reference to free variable string ** assignment to free variable string While compiling the end of the data in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/coq.el: ** The following functions might not be defined at runtime: span- property, set-span-property ** The following functions are not known to be defined: holes-replace-string-by-holes-backward, holes-set-point-next- hole-destroy, symbol-near-point Wrote /Users/clintonlefort/ISABELLE_HOME/clintonlefort/ProofGeneral/ ProofGeneral-3.6/coq/coq.elc While compiling coq-match-subscript in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/x- symbol-coq.el: ** assignment to free variable x-symbol-coq-subscript-type While compiling the end of the data in file /Users/clintonlefort/ ISABELLE_HOME/clintonlefort/ProofGeneral/ProofGeneral-3.6/coq/x- symbol-coq.el: ** The function x-symbol-make-grammar' is not known to be defined.
Wrote /Users/clintonlefort/ISABELLE_HOME/cli
[message truncated]

Last updated: May 03 2024 at 08:18 UTC