Email Gateway (Aug 18 2022 at 09:58): Email Gateway (Aug 18 2022 at 09:58):From: clefort <ipub@charter.net>
Hello,
Here is my attempt to remake Proofgeneral for Emacs:
24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME/
ProofGeneral-3.6pre050930 clintonlefort$ make clean
make pgscripts DEST_ELISP='$$HOME/ProofGeneral'
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 ~ /~ .\# /.\# .byte-compile
(cd doc; make clean)
make -f Makefile.doc DOCNAME=PG-adapting MAKE="make -f Makefile.doc"
clean
rm -f ProofGeneral.txt ProofGeneralPortrait.eps ProofGeneralPortrait.pdf
rm -f PG-adapting.{cp,fn,vr,tp,ky,pg}
rm -f PG-adapting.{fns,vrs,cps,aux,log,toc,kys,cp0}
rm -f *~
make -f Makefile.doc DOCNAME=ProofGeneral MAKE="make -f Makefile.doc"
clean
rm -f ProofGeneral.txt ProofGeneralPortrait.eps ProofGeneralPortrait.pdf
rm -f ProofGeneral.{cp,fn,vr,tp,ky,pg}
rm -f ProofGeneral.{fns,vrs,cps,aux,log,toc,kys,cp0}
rm -f *~
(cd x-symbol/lisp; make distclean)
rm -f ~ core .\# *.cps *.fns *.kys *.vr *.tp *.pg *.log *.aux *.toc
*.cp *.ky *.fn
rm -f *.elc *.dvi .info *.ps
24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME/
ProofGeneral-3.6pre050930 clintonlefort$
SECONDLY, IT DOES IT'S THING but gives me this message at the end:
24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME/
ProofGeneral-3.6pre050930 clintonlefort$ make compile
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
xemacs -batch -q -no-site-file -eval '(setq load-path (append (mapcar
(lambda (d) (concat "/Users/clintonlefort/Isabelle/Isabelle/
ISABELLE_HOME/ProofGeneral-3.6pre050930/" (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
make: xemacs: Command not found
make: [.byte-compile] Error 127 (ignored)
rm -f
Byte compiling X-Symbol...
(cd x-symbol/lisp; rm -f *.elc; make EMACS="xemacs -q -no-site-file")
xemacs -q -no-site-file -batch --eval '(setq load-path (append (list
"." "/usr/local/share/emacs/site-lisp/elib" "/usr/local/share/emacs/
site-lisp") load-path))' -f batch-byte-compile x-symbol-hooks.el
make[1]: xemacs: Command not found
make[1]: *** [x-symbol-hooks.elc] Error 127
make: *** [.byte-compile] Error 2
24-182-155-183:~/Isabelle/Isabelle/ISABELLE_HOME/
ProofGeneral-3.6pre050930 clintonlefort$
WHAT NOW?
CL
Last updated: May 03 2024 at 04:19 UTC