SRI-CSL / PVS

The People's Verification System
http://pvs.csl.sri.com
GNU General Public License v2.0
132 stars 32 forks source link

"Cannot open load file: no such file or directory 'lmenu'" #100

Open quinn-dougherty opened 1 month ago

quinn-dougherty commented 1 month ago

I built from source (a2940953d4f3c3abbf43799875e28e4044ddc424), and when I open the pvs emacs build I get this:

Debugger entered--Lisp error: (file-missing "Cannot open load file" "No such file or directory" "lmenu")
  require(lmenu)
  tcl-add-emacs-menu((keymap (menu-bar keymap "Tcl") (3 keymap (19 . switch-to-tcl) (24 . tcl-eval-region) (20 . inferior-tcl) (6 . tcl-load-file) (22 . tcl-eval-defun) (9 . tcl-help-on-word) (3 . comment-region) (2 . tcl-submit-bug-report)) (9 . tcl-indent-command) (127 . backward-delete-char-untabify) (27 keymap (24 . tcl-eval-defun) (59 . tcl-indent-for-comment) (17 . indent-tcl-exp) (8 . tcl-mark-defun) (5 . tcl-end-of-defun) (1 . tcl-beginning-of-defun)) (35 . tcl-electric-hash) (59 . tcl-electric-char) (93 . tcl-electric-char) (91 . tcl-electric-char) (125 . tcl-electric-brace) (123 . tcl-electric-char)))
  tcl-fill-mode-map()
  byte-code("\10\204\n\0\303 \20\304 \210\11\204\25\0\305\n!\21\306 \210\303\207" [tcl-mode-map inferior-tcl-mode-map comint-mode-map make-sparse-keymap tcl-fill-mode-map copy-keymap tcl-fill-inferior-map] 2)
  load("tcl" t nil)
  (let ((load-path pvs-original-load-path)) (load "tcl" t noninteractive))
  (or (let ((load-path pvs-original-load-path)) (load "tcl" t noninteractive)) (load "tcl" nil noninteractive))
  load-with-code-conversion("/home/qd/Projects/sri-summer-school/PVS/emacs/pvs-..." "/home/qd/Projects/sri-summer-school/PVS/emacs/pvs-..." nil nil)
  load("pvs-tcl" nil nil)
  load-with-code-conversion("/home/qd/Projects/sri-summer-school/PVS/emacs/pvs-..." "/home/qd/Projects/sri-summer-school/PVS/emacs/pvs-..." nil nil)
  load("pvs-load" nil nil nil)
  load-with-code-conversion("/home/qd/Projects/sri-summer-school/PVS/emacs/go-p..." "/home/qd/Projects/sri-summer-school/PVS/emacs/go-p..." nil t)
  #<subr command-line-1>(("-load" "/home/qd/Projects/sri-summer-school/PVS/emacs/go-p..."))
  apply(#<subr command-line-1> ("-load" "/home/qd/Projects/sri-summer-school/PVS/emacs/go-p..."))
  command-line-1(("-load" "/home/qd/Projects/sri-summer-school/PVS/emacs/go-p..."))
  command-line()
  normal-top-level()

When I open up a .pvs file, and try typechecking, I get Symbol's value as variable is void: pvs-in-evaluator

here:

;; Emacs does menus via keymaps.  Do it in a function in case we
;; later decide to add it to inferior Tcl mode as well.
(defun tcl-add-emacs-menu (map)
  (define-key map [menu-bar] (make-sparse-keymap "Tcl"))
  ;; This fails in Emacs 19.22 and earlier.
  (require 'lmenu)
  (let ((menu (make-lucid-menu-keymap "Tcl" tcl-xemacs-menu)))
    (define-key map [menu-bar tcl] (cons "Tcl" menu))
    ;; The following is intended to compute the key sequence
    ;; information for the menu.  It doesn't work.
    (x-popup-menu nil menu)))

I notice that melpa has imenus, but not lmenu.

I'm on NixOS, and here is the devshell used (note I needed to manually type sudo ln -s $(which chmod) /bin/chmod due to a previous bug)

output of ./configure:

┬─[qd@grindenstern:~/P/s/PVS]─[08:55:15 AM]─[G:master=]
╰─>$ ./configure
checking build system type... x86_64-pc-linux-gnu
checking pvspath... found "/home/qd/Projects/sri-summer-school/PVS/pvs.in"
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking for ld... ld
checking for ar... ar
checking for ranlib... ranlib
checking for emacs... emacs
checking for xemacs... no
checking for emacs version >= 19... found 29.3
checking for grep... grep
checking for etags... etags
checking for mkdir... mkdir
checking for a thread-safe mkdir -p... /nix/store/php4qidg2bxzmm79vpri025bqi0fa889-coreutils-9.5/bin/mkdir -p
checking for tar... tar
checking for rm... rm
checking for curl... curl
checking for git... git
checking for sbcl... sbcl
configure: creating ./config.status
config.status: creating Makefile
config.status: creating pvs
config.status: creating pvsio
config.status: creating proveit
config.status: creating provethem
config.status: creating pvs-get-patches
config.status: creating doc/api/Makefile
config.status: creating doc/user-guide/Makefile
config.status: creating doc/language/Makefile
config.status: creating doc/language/pvs-doc.el
config.status: creating doc/prover/Makefile
config.status: creating lib/registry.conf

make seems to raise no errors

I will note that it collides with my system emacs, but when I make it not do that (like by downdating the emacs that pvs builds to 28) there's another error (which seems worse)