Installation error (Fedora 37, Emacs 28.2)

[clementblaudeau]

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

[samowre]

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]

Hi Sam, Thank you for you answer. I don't see any errors when running emacs alone (emacs --debug-init does not output anything). The result of M-x emacs-version is

GNU Emacs 28.2 (build 1, x86_64-redhat-linux-gnu, GTK+ Version 3.24.36, cairo version 1.17.6) of 2023-01-28

PVSEMACS is not set. I'm on Fedora 37, uname -a gives :

Linux [username] 6.1.12-200.fc37.x86_64 #1 SMP PREEMPT_DYNAMIC Wed Feb 15 04:35:34 UTC 2023 x86_64 x86_64 x86_64 GNU/Linux

Should I try reinstalling emacs ? Thank you for your help

[jamesjer]

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.

[jedbrown]

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).

[clementblaudeau]

I've managed to get it (half) working on Fedora by :

1. Adding the -q option in the install.sh file (line 39)
2. Using the patch pvs-emacs.zip (re-attached here as indeed the link is dead) by running patch -p1 --dry-run < ../pvs-emacs.patch (remove --dry-run if everything works). However, this is only "half-working" as pvs works only once. After I close and restard pvs I get the error :

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...

[samowre]

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.

[jedbrown]

Hi :wave:, 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?

[samowre]

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.

[jedbrown]

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.

[samowre]

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.

[jedbrown]

Thanks, sorry about my slow reply. This is on latest master (17d4f506453c2401254b690b978f73c1a379fb4f).

$ ./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

[samowre]

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.

[jedbrown]

Yeah, it's attached in the comment above. Feel free to move this to email if you prefer.

[samowre]

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.

[jedbrown]

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 files

Or if I start over git clean -fxd ., I get

$ ./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.log

byte-compile.log

In this case, ./pvs does not exist.

[jedbrown]

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.

[samowre]

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.

[jedbrown]

I initially had an error Package ASDF does not exist., but search indicated I should create ~/.sbclrc and put (require 'asdf) there, which got me to an error about BABEL missing. I installed cl-babel from my package manager, then (ql:quickload :clack) and same for websocket-driver, hunchentoot, anaphora, lparallel, and cl-json. Then I got the following log:

pvs-asd.log

It looks like packages.lisp has this dependency logic and maybe it was missed because I hadn't set up ~/.sbclrc ahead of time.