[isabelle] make-clean ProofGeneral/remake





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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.