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.
|
|
Hi 👋, thanks for looking into this. Have you gotten a chance to make progress or would scripting around Clément's solution be the recommended short-term workaround? |
|
Hi Jeb,
Sorry, I was away for a while, then got sick. I'm looking into this now,
and hopefully will have either a fix or more questions for you by
tomorrow.
By the way, I ran into all these warnings after getting a Docker image
working with Fedora 37, but PVS still seems to run OK for me.
Best regards,
Sam
Jed Brown ***@***.***> wrote:
… Hi 👋, thanks for looking into this. Have you gotten a chance to make progress or would scripting around
Clément's solution be the recommended short-term workaround?
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
|
Thanks for looking into this. Do you have a recommendation for emacs 29 or 30? I could revert to an older version if needed, though would need to keep it isolated since my configuration ( |
|
Hi Jed,
I've run with Emacs 25.3, 28, 29, 30, and 31 (the latter were built from
the Emacs repository). I couldn't get 24 or earlier built on my Ubuntu
laptop, so I can't say whether those will work. The latest did require
some changes to PVS Emacs code, because defadvice went from deprecated
to error. I still need to push those fixes out, after I do a few more
changes.
Please send me your log of ./install-sh, and I'll make sure it works for
you.
Thanks,
Sam
Jed Brown ***@***.***> wrote:
… Thanks for looking into this. Do you have a recommendation for emacs 29 or 30? I could revert to an
older version if needed, though would need to keep it isolated since my configuration (.emacs, etc.)
tracks current versions.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
|
Thanks, sorry about my slow reply. This is on latest $ ./install-sh
Setting PVSPATH in the "pvs", "pvsio", "proveit", and "provethem"
shell scripts to /home/jed/src/pvs
If this is not the right path, edit the scripts before using them.
\nByte compiling emacs files using /home/jed/bin/emacs: GNU Emacs 30.0.50
if this is not the right Emacs, set PVSEMACS
otherwise the byte compiled files will cause an error
see byte-compile.log for details (mostly warnings)
!!! Something went wrong - see the end of byte-compile.log
$ PVSEMACS=/bin/emacs ./install-sh
Setting PVSPATH in the "pvs", "pvsio", "proveit", and "provethem"
shell scripts to /home/jed/src/pvs
If this is not the right path, edit the scripts before using them.
\nByte compiling emacs files using /bin/emacs: GNU Emacs 29.4
if this is not the right Emacs, set PVSEMACS
otherwise the byte compiled files will cause an error
see byte-compile.log for details (mostly warnings)
!!! Something went wrong - see the end of byte-compile.log |
|
Hi Jed,
Could you send me byte-compile.log so I can see what the error actually
is?
Thanks,
Sam
Jed Brown ***@***.***> wrote:
… Thanks, sorry about my slow reply. This is on latest master (17d4f50).
$ ./install-sh
Setting PVSPATH in the "pvs", "pvsio", "proveit", and "provethem"
shell scripts to /home/jed/src/pvs
If this is not the right path, edit the scripts before using them.
\nByte compiling emacs files using /home/jed/bin/emacs: GNU Emacs 30.0.50
if this is not the right Emacs, set PVSEMACS
otherwise the byte compiled files will cause an error
see byte-compile.log for details (mostly warnings)
!!! Something went wrong - see the end of byte-compile.log
$ PVSEMACS=/bin/emacs ./install-sh
Setting PVSPATH in the "pvs", "pvsio", "proveit", and "provethem"
shell scripts to /home/jed/src/pvs
If this is not the right path, edit the scripts before using them.
\nByte compiling emacs files using /bin/emacs: GNU Emacs 29.4
if this is not the right Emacs, set PVSEMACS
otherwise the byte compiled files will cause an error
see byte-compile.log for details (mostly warnings)
!!! Something went wrong - see the end of byte-compile.log
byte-compile.log
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
|
Yeah, it's attached in the comment above. Feel free to move this to email if you prefer. |
|
Hi Jed,
Sorry for not seeing that you had already included the log file.
I hope you don't mind doing a few experiments so I can try to solve this
problem once and for all.
The main problem that I see is that make is not creating the file
pvs-prelude-files-and-regions.el
You should be able to run the following (which is what make should be
doing) from your PVS installation:
./pvs -batch -q -l emacs/pvs-set-prelude-info.el -f set-prelude-files-and-regions
If that succeeds, you should have a new, nonempty emacs/pvs-files-and-regions.el file.
Please let me know what you're seeing if it fails.
If it succeeds, ./install-sh should now work with warnings in the log
file, but no errors.
If it fails, try copying the file below to your <PVS>/emacs/ directory, and
run ./install-sh again.
Thanks for your patience,
Sam
Jed Brown ***@***.***> wrote:
… Yeah, it's attached in the comment above. Feel free to move this to email if you prefer.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
|
This is in the repo in which I tried applying the patch discussed above. $ ./pvs -batch -q -l emacs/pvs-set-prelude-info.el -f set-prelude-files-and-regions
No executable available in /home/jed/src/pvs/bin/ix86_64-Linux
$ tree bin/ix86_64-Linux
bin/ix86_64-Linux
├── runtime
├── yices1 -> ../../yices/ix86_64-Linux/yices-1.0.40/bin/yices
└── yices2 -> ../../yices/ix86_64-Linux/yices-2.6.4/bin/yices
2 directories, 2 filesOr if I start over $ ./install-sh
Setting PVSPATH in the "pvs", "pvsio", "proveit", and "provethem"
shell scripts to /home/jed/src/pvs
If this is not the right path, edit the scripts before using them.
chmod: cannot access 'pvs': No such file or directory
chmod: cannot access 'pvsio': No such file or directory
chmod: cannot access 'proveit': No such file or directory
chmod: cannot access 'provethem': No such file or directory
./install-sh: line 14: pvs: No such file or directory
mv: cannot stat 'tmp.1609412': No such file or directory
./install-sh: line 16: pvsio: No such file or directory
mv: cannot stat 'tmp.1609412': No such file or directory
./install-sh: line 18: proveit: No such file or directory
mv: cannot stat 'tmp.1609412': No such file or directory
./install-sh: line 20: provethem: No such file or directory
mv: cannot stat 'tmp.1609412': No such file or directory
chmod: cannot access 'pvs': No such file or directory
chmod: cannot access 'pvsio': No such file or directory
chmod: cannot access 'proveit': No such file or directory
chmod: cannot access 'provethem': No such file or directory
\nByte compiling emacs files using /home/jed/bin/emacs: GNU Emacs 30.0.50
if this is not the right Emacs, set PVSEMACS
otherwise the byte compiled files will cause an error
see byte-compile.log for details (mostly warnings)
!!! Something went wrong - see the end of byte-compile.logIn this case, |
|
My mistake above, as I forgot to re-run $ /pvs -batch -q -l emacs/pvs-set-prelude-info.el -f set-prelude-files-and-regions
No executable available in /home/jed/src/pvs/bin/ix86-Linuxwith that directory not existing. |
|
Hi Jed,
For some reason the make isn't generating the Lisp image, and this is the
real problem. Could you please try (from the terminal in your <PVS>
directory):
% stdbuf -o 0 sbcl 2>&1 | tee pvs-asd.log
This will start SBCL, and capture the results in the pvs-asd.log file
Assuming it produces a "*" prompt, run
(load "pvs.asd")
followed by
(asdf:operate :program-op :pvs)
This should lead to lots of output, but somewhere in there should be an
error. Please send the log file to me.
Thanks,
Sam
Jed Brown ***@***.***> wrote:
… My mistake above, as I forgot to re-run ./configure after cleaning (it creates the ./pvs executable). In any
case, I get the same error and
$ /pvs -batch -q -l emacs/pvs-set-prelude-info.el -f set-prelude-files-and-regions
No executable available in /home/jed/src/pvs/bin/ix86-Linux
with that directory not existing.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you commented.
|
|
I initially had an error It looks like |
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: