samowre
commented
1 year ago Hi Clément,
I think there may be something wrong with your Emacs installation. Do you get any errors when you just run Emacs by itself?
I say this because PVS does not directly use site-lisp; it seems you have a newer Emacs trying to use an old /usr/share/emacs.
Also, if you have the PVSEMACS environment variable set, make sure it is correct - you shouldn't need to set it if you can just run "emacs" at the command line.
If you still have problems, please let me know what platform you're using, and let me know the results of "emacs --version" (or "M-x emacs-version" inside of Emacs.
Thanks, Sam
Clément Blaudeau @.***> wrote:
Dear PVS developpers, While trying to install the latest version (or any recent snapshot), I have an error when running ./install-sh : !!! Something went wrong - see the end of byte-compile.log The byte-compile.log file shows :
Byte compilation currently generates lots of warnings (because of compatibility issues with older Emacs versions)\n Loading /usr/share/emacs/site-lisp/site-start.d/asy-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/autoconf-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/cmake-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/desktop-entry-mode-init.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/mercurial-site-start.el (source)... Loading /usr/share/emacs/site-lisp/site-start.d/rpmdev-init.el (source)... PVS: byte compilation starting
In pvs-kind-of-buffer: pvs-utils.el:80:12: Warning: reference to free variable ‘pvs-prelude’ pvs-utils.el:90:23: Warning: reference to free variable ‘pvs-buffer-kind’
In end of data: pvs-utils.el:2018:20: Warning: the function ‘decf’ is not known to be defined. pvs-utils.el:1879:30: Warning: the function ‘ilisp-value’ is not known to be defined. pvs-utils.el:1860:6: Warning: the function ‘princ-nl’ is not known to be defined. pvs-utils.el:1843:8: Warning: the function ‘switch-to-lisp’ is not known to be defined. pvs-utils.el:1824:17: Warning: the function ‘pvs-formula-origin’ is not known to be defined. pvs-utils.el:1818:4: Warning: the function ‘typecheck’ is not known to be defined. pvs-utils.el:1817:4: Warning: the function ‘find-pvs-file’ is not known to be defined. pvs-utils.el:1816:4: Warning: the function ‘pvs-remove-bin-files’ is not known to be defined. pvs-utils.el:1812:6: Warning: the function ‘pvs-send’ is not known to be defined. pvs-utils.el:1810:18: Warning: the function ‘prove-pvs-file’ is not known to be defined. pvs-utils.el:1809:18: Warning: the function ‘prove-theory’ is not known to be defined. pvs-utils.el:1807:23: Warning: the function ‘comint-send’ is not known to be defined. pvs-utils.el:1806:42: Warning: the function ‘ilisp-process’ is not known to be defined. pvs-utils.el:1799:21: Warning: the function ‘ilisp-send’ is not known to be defined. pvs-utils.el:1796:18: Warning: the function ‘prove-importchain’ is not known to be defined. pvs-utils.el:1783:4: Warning: the function ‘set-rewrite-depth’ is not known to be defined. pvs-utils.el:1506:10: Warning: the function ‘pushnew’ is not known to be defined. pvs-utils.el:1335:27: Warning: the function ‘endp’ is not known to be defined. pvs-utils.el:990:29: Warning: the function ‘context-files’ is not known to be defined. pvs-utils.el:811:4: Warning: the function ‘pvs-bury-output’ is not known to be defined. pvs-utils.el:776:15: Warning: the function ‘comint-remove-whitespace’ is not known to be defined. pvs-utils.el:621:4: Warning: the function ‘save-some-pvs-files’ is not known to be defined. pvs-utils.el:347:17: Warning: the function ‘pvs-send-and-wait’ is not known to be defined. Loading /usr/share/emacs/28.2/lisp/international/uni-name.el (source)... pvs-ltx: 1282 rules (+ 0 conflicts)! Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilcompat.elc... Loading ilisp/ilcompat... Loading /home/cblaudeau/pvsdir/emacs/ilisp/completer.elc... Loading ilisp/completer... Loading /home/cblaudeau/pvsdir/emacs/ilisp/comint-ipc.elc... Loading ilisp/comint-ipc... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-def.elc... Loading ilisp/ilisp-def... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-sym.elc... Loading ilisp/ilisp-sym... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-inp.elc... Loading ilisp/ilisp-inp... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-ind.elc... Loading ilisp/ilisp-ind... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-prc.elc... Loading ilisp/ilisp-prc... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-val.elc... Loading ilisp/ilisp-val... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-out.elc... Loading ilisp/ilisp-out... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-mov.elc... Loading ilisp/ilisp-mov... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-key.elc... Loading ilisp/ilisp-key... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-prn.elc... Loading` ilisp/ilisp-prn... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-low.elc... Loading ilisp/ilisp-low... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-doc.elc... Loading ilisp/ilisp-doc... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-ext.elc... Loading ilisp/ilisp-ext... Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-mod.elc...
I figured that loading ilisp-mod was failing, which is indeed the case. Trying to load it directly in emacs, I get :
Wrote /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-mod.elc Loading /home/cblaudeau/pvsdir/emacs/ilisp/ilisp-mod.elc... ilisp-byte-code-to-list: Wrong type argument: sequencep, #
I narrowed it down to the line 69: (ilisp-set-doc 'lisp-mode ilisp-documentation)
If I try to run ./pvs nevertheless, I get the following error :
Debugger entered--Lisp error: (wrong-type-argument sequencep #
) append(# nil) ilisp-byte-code-to-list(# ) ilisp-set-doc(lisp-mode "Major mode for interacting with an inferior Lisp p...") byte-code("\301\302\10\"\210\301\303\10\"\207" [ilisp-documentation ilisp-set-doc ilisp-mode lisp-mode] 3) load("ilisp-mod" nil nil) load-with-code-conversion("/home/cblaudeau/pvsdir/emacs/ilisp/ilisp.el" "/home/cblaudeau/pvsdir/emacs/ilisp/ilisp.el" nil nil) load("ilisp" nil nil) byte-code("\305\306!\210\307\310\311\10#\210\307\312\311\10#\210\307\313\311\10#\210\307\314\311\10#\210\307\315\311\10#\210\307\316\311\10#\210\307\317\311\10#\210\307\320\311\10..." [noninteractive emacs-major-version emacs-minor-version pvs-original-load-path load-path make-variable-buffer-local pvs-buffer-kind load "ilisp" nil "pvs-ilisp" "pvs-mode" "pvs-view" "pvs-file-list" "pvs-browser" "pvs-utils" "pvs-cmds" (error) "pvs-prelude-files-and-regions" "pvs-print" "pvs-proofstate" "pvs-prover" "pvs-abbreviations" boundp 20 19 29 "pvs-menu" "pvs-tcl" "pvs-prover-helps" "pvs-eval" "pvs-pvsio" "pvs-prover-manip" "manip-debug-utils" "prooflite" "newcomment" t put comment-region pvs-command editing global-set-key "\3;"] 4) load("pvs-load" nil nil nil) load-with-code-conversion("/home/cblaudeau/pvsdir/e..." "/home/cblaudeau/Documents/pvsdir/e..." nil t) command-line-1(("-load" "/home/cblaudeau/pvsdir/emacs/go-pvs.el")) command-line() normal-top-level() Commenting the line 69 makes the ./install-sh go through, and .pvs runs normally. However, as soon as I quit it and rerun it, I get the error above.
Am I doing something wrong ? Thank you for your help
— Reply to this email directly, view it on GitHub, or unsubscribe. You are receiving this because you are subscribed to this thread.
clementblaudeau
jamesjer
jedbrown
Dear PVS developpers, While trying to install the latest version (or any recent snapshot), I have an error when running
./install-sh:!!! Something went wrong - see the end of byte-compile.logThebyte-compile.logfile shows :I figured that loading
ilisp-modwas failing, which is indeed the case. Trying to load it directly in emacs, I get :I narrowed it down to the line 69:
(ilisp-set-doc 'lisp-mode ilisp-documentation)If I try to run
./pvsnevertheless, I get the following error :Commenting the line 69 makes the
./install-shgo through, and .pvs runs normally. However, as soon as I quit it and rerun it, I get the error above.Am I doing something wrong ? Thank you for your help