Installation error (Fedora 37, Emacs 28.2) #92
Comments
|
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, #<subr lisp-mode>
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 #<subr lisp-mode>)
append(#<subr lisp-mode> nil)
ilisp-byte-code-to-list(#<subr lisp-mode>)
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.
|
|
Hi Sam, PVSEMACS is not set. I'm on Fedora 37, Should I try reinstalling emacs ? |
|
I had to make a number of changes to the Emacs files to avoid this and other issues when Emacs 28 was released. Those changes are included in the Fedora pvs-sbcl package. If you want to see what I did, take a look at this patch: https://src.fedoraproject.org/rpms/pvs-sbcl/blob/rawhide/f/pvs-emacs.patch. I wasn't sure if any of those changes would break Emacs versions < 28, which is why I haven't opened any pull requests yet. |
|
I'm also hitting this with emacs-29 and emacs-30. The patch linked above is now 404 because the package has been removed from Fedora. I salvaged the patch file from this commit. |
|
I've managed to get it (half) working on Fedora by :
Debugger entered--Lisp error: (void-variable common-lisp)
byte-code("..." [removed] 25)
load("ilisp-cl" nil nil)
byte-code("..." [removed] 4)
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;" ad-add-advice kill-emacs (pvs-batch-control (protect) t (advice lambda nil (exit-pvs-process))) before ad-activate] 5)
load("pvs-load" nil nil nil)
load-with-code-conversion("/home/user/pvsdir/emac..." "/home/user/pvsdir/emac..." nil t)
command-line-1(("-load" "/home/user/pvsdir/emacs/go-pvs.el"))
command-line()
normal-top-level()Re-installing pvs allows me to run it once, so I have to basically reinstall it every time... |
|
Hi Jed,
I was away yesterday, and just got back last night - I'll try to recreate
your environment today and get back to you when I know something.
Thanks for your patience,
Sam
Jed Brown ***@***.***> wrote:
… I'm also hitting this with emacs-29 and emacs-30. The patch linked above is now 404 because the
package has been removed from Fedora. I salvaged the patch file from this commit.
Unfortunately, I see lots of failed hunks (which seems odd since the file hasn't changed) when trying to
build on Arch (cf. #91) so probably need to go through them one at a time. It would be helpful for the
maintainers to specify which Emacs versions are supported (which would also clarify when support for
legacy versions can be removed).
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.logThe
byte-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
The text was updated successfully, but these errors were encountered: