Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 1019


Synopsis:        install 4.1 error
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Sun Dec  9 21:50:00 2007
Originator:      David Naumann
Organization:    cs.stevens.edu
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
    This message is in MIME format.  The first part should be readable text,
    while the remaining parts are likely unreadable without MIME-aware tools.
  
  --0-1441380438-1197264212=:7125
  Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
  
  Hi,
  
  I installed PVS 4.1 on an Intel Mac and got an error when I ran the pvs 
  script.  It appears that bin/relocate ran successfully, since it sets
  PVSPATH=/Users/naumann/pvs41
  
  At the unix prompt I executed
  /Users/naumann/pvs41/pvs -emacs /usr/local/Emacs.app/Contents/MacOS/Emacs"
  and emacs runs but I get a *backtrace* buffer instead of PVS.  See below.
  
  I expected this to work since I've been happily using PVS 4.0 with the 
  same invocation except for the directory:
  /Users/naumann/pvs4/pvs -emacs /usr/local/Emacs.app/Contents/MacOS/Emacs"
  
  Here's the backtrace.  My mailer trashed the byte-code stuff so I've also 
  attached it to this message.
  
  Debugger entered--Lisp error: (void-function memql)
     memql(("\\.pvs\\'" . pvs-mode) (("\\.cl$" . lisp-mode) ("\\.lisp$" . 
  lisp-mode) ("\\.text\\'" . text-mode) ("\\.txt\\'" . text-mode) 
  ("\\.java\\'" . java-mode) ("\\.sal\\'" . sal-mode) ("\\.c\\'" . c-mode) 
  ("\\.h\\'" . c++-mode) ("\\.tex\\'" . LaTeX-mode) ("\\.bbl\\'" . 
  LaTeX-mode) ("\\.bib\\'" . bibtex-mode) ("\\.el\\'" . emacs-lisp-mode) 
  ("\\.scm\\'" . scheme-mode) ("\\.lisp\\'" . lisp-mode) ("\\.pl\\'" . 
  perl-mode) ("\\.cc\\'" . c++-mode) ("\\.hh\\'" . c++-mode) ("\\.C\\'" . 
  c++-mode) ("\\.H\\'" . c++-mode) ("[Mm]akefile" . makefile-mode) 
  ("\\.texinfo\\'" . texinfo-mode) ("\\.texi\\'" . texinfo-mode) ("\\.s\\'" 
  . asm-mode) ("ChangeLog\\'" . change-log-mode) ("change.log\\'" . 
  change-log-mode) ("changelo\\'" . change-log-mode) ("ChangeLog.[0-9]+\\'" 
  . change-log-mode) ("\\$CHANGE_LOG\\$\\.TXT" . change-log-mode) 
  ("\\.TeX\\'" . TeX-mode) ("\\.sty\\'" . LaTeX-mode) ("\\.tcl\\'" . 
  tcl-mode) ("\\.lsp\\'" . lisp-mode) ("\\.awk\\'" . awk-mode) 
  ("\\.prolog\\'" . prolog-mode) ("\\.tar\\'" . tar-mode) ("^/tmp/Re" . 
  text-mode) ("/Message[0-9]*\\'" . text-mode) ("\\.y\\'" . c-mode) 
  ("\\.lex\\'" . c-mode) ("\\.scm.[0-9]*\\'" . scheme-mode) 
  ("[]>:/]\\..*emacs\\'" . emacs-lisp-mode) ("[:/]_emacs\\'" . 
  emacs-lisp-mode) ("\\.ml\\'" . lisp-mode)))
     byte-code("..........trashed by mailer......................
     load("pvs-load" nil nil nil)
     eval-buffer(#<buffer  *load*> nil "/Users/naumann/pvs41/emacs/go-pvs.el" 
  nil t)  ; Reading at buffer position 2780
     load-with-code-conversion("/Users/naumann/pvs41/emacs/go-pvs.el" 
  "/Users/naumann/pvs41/emacs/go-pvs.el" nil t)
     load("/Users/naumann/pvs41/emacs/go-pvs.el" nil t)
     command-line-1(("-load" "/Users/naumann/pvs41/emacs/go-pvs.el"))
     command-line()
     normal-top-level()
  
  
  Here's the emacs/OS info:
  
  GNU Emacs 22.0.50.1 (i386-apple-darwin8.7.1) of 2006-08-19 on petit.local
  
  Darwin host-730h-24.dhcp.stevens-tech.edu 8.11.1 Darwin Kernel Version 
  8.11.1: Wed Oct 10 18:23:28 PDT 2007; root:xnu-792.25.20~1/RELEASE_I386 i386 
 i386
  
  
  --0-1441380438-1197264212=:7125
  Content-Type: APPLICATION/octet-stream; name=tempXXX
  Content-Transfer-Encoding: BASE64
  Content-ID: <Pine.NEB.4.64.0712100023320.7125@eylenbosch.cs.stevens-tech.edu>
  Content-Description: 
  Content-Disposition: attachment; filename=tempXXX
  
  RGVidWdnZXIgZW50ZXJlZC0tTGlzcCBlcnJvcjogKHZvaWQtZnVuY3Rpb24g
  bWVtcWwpCiAgbWVtcWwoKCJcXC5wdnNcXCciIC4gcHZzLW1vZGUpICgoIlxc
  LmNsJCIgLiBsaXNwLW1vZGUpICgiXFwubGlzcCQiIC4gbGlzcC1tb2RlKSAo
  IlxcLnRleHRcXCciIC4gdGV4dC1tb2RlKSAoIlxcLnR4dFxcJyIgLiB0ZXh0
  LW1vZGUpICgiXFwuamF2YVxcJyIgLiBqYXZhLW1vZGUpICgiXFwuc2FsXFwn
  IiAuIHNhbC1tb2RlKSAoIlxcLmNcXCciIC4gYy1tb2RlKSAoIlxcLmhcXCci
  IC4gYysrLW1vZGUpICgiXFwudGV4XFwnIiAuIExhVGVYLW1vZGUpICgiXFwu
  YmJsXFwnIiAuIExhVGVYLW1vZGUpICgiXFwuYmliXFwnIiAuIGJpYnRleC1t
  b2RlKSAoIlxcLmVsXFwnIiAuIGVtYWNzLWxpc3AtbW9kZSkgKCJcXC5zY21c
  XCciIC4gc2NoZW1lLW1vZGUpICgiXFwubGlzcFxcJyIgLiBsaXNwLW1vZGUp
  ICgiXFwucGxcXCciIC4gcGVybC1tb2RlKSAoIlxcLmNjXFwnIiAuIGMrKy1t
  b2RlKSAoIlxcLmhoXFwnIiAuIGMrKy1tb2RlKSAoIlxcLkNcXCciIC4gYysr
  LW1vZGUpICgiXFwuSFxcJyIgLiBjKystbW9kZSkgKCJbTW1dYWtlZmlsZSIg
  LiBtYWtlZmlsZS1tb2RlKSAoIlxcLnRleGluZm9cXCciIC4gdGV4aW5mby1t
  b2RlKSAoIlxcLnRleGlcXCciIC4gdGV4aW5mby1tb2RlKSAoIlxcLnNcXCci
  IC4gYXNtLW1vZGUpICgiQ2hhbmdlTG9nXFwnIiAuIGNoYW5nZS1sb2ctbW9k
  ZSkgKCJjaGFuZ2UubG9nXFwnIiAuIGNoYW5nZS1sb2ctbW9kZSkgKCJjaGFu
  Z2Vsb1xcJyIgLiBjaGFuZ2UtbG9nLW1vZGUpICgiQ2hhbmdlTG9nLlswLTld
  K1xcJyIgLiBjaGFuZ2UtbG9nLW1vZGUpICgiXFwkQ0hBTkdFX0xPR1xcJFxc
  LlRYVCIgLiBjaGFuZ2UtbG9nLW1vZGUpICgiXFwuVGVYXFwnIiAuIFRlWC1t
  b2RlKSAoIlxcLnN0eVxcJyIgLiBMYVRlWC1tb2RlKSAoIlxcLnRjbFxcJyIg
  LiB0Y2wtbW9kZSkgKCJcXC5sc3BcXCciIC4gbGlzcC1tb2RlKSAoIlxcLmF3
  a1xcJyIgLiBhd2stbW9kZSkgKCJcXC5wcm9sb2dcXCciIC4gcHJvbG9nLW1v
  ZGUpICgiXFwudGFyXFwnIiAuIHRhci1tb2RlKSAoIl4vdG1wL1JlIiAuIHRl
  eHQtbW9kZSkgKCIvTWVzc2FnZVswLTldKlxcJyIgLiB0ZXh0LW1vZGUpICgi
  XFwueVxcJyIgLiBjLW1vZGUpICgiXFwubGV4XFwnIiAuIGMtbW9kZSkgKCJc
  XC5zY20uWzAtOV0qXFwnIiAuIHNjaGVtZS1tb2RlKSAoIltdPjovXVxcLi4q
  ZW1hY3NcXCciIC4gZW1hY3MtbGlzcC1tb2RlKSAoIls6L11fZW1hY3NcXCci
  IC4gZW1hY3MtbGlzcC1tb2RlKSAoIlxcLm1sXFwnIiAuIGxpc3AtbW9kZSkp
  KQogIGJ5dGUtY29kZSgiw4UYw4YICVwiwoMOAAnCiMKCEgAICUIRKcOHGMOG
  CAlcIsKDIQAJwojCgiUACAlCESnDiBjDhggJXCLCgzQACcKIwoI4AAgJQhEp
  w4kYw4YICVwiwoNHAAnCiMKCSwAICUIRKcOKGMOGCFxuXCLCg1oAXG7CiMKC
  XgAIXG5CEinDiwtCE8OMw4shwoRuAMONw4vDjlwiwojDhAtCE8OMw4QhwoR9
  AMONw4TDj1wiwohcZsKEfQLDkCAUw5FcZsOSw5MjwojDkVxmw5TDlSPCiMOR
  XGbDlsOXI8KIw5FcZsOYw5kjwojDkVxmw5rDmyPCiMORXGbDnMOdI8KIw5Fc
  ZsOew58jwojDkVxmw6DDoSPCiMORXGbDosOjI8KIw5FcZsOkw6UjwojDkVxm
  w6bDpyPCiMORXGbDqMOpI8KIw5FcZsOqw6sjwojDkVxmw6zDrSPCiMORXGbD
  rsOvI8KIw5FcZsOww68jwojDkVxmw7HDryPCiMORXGbDssOzI8KIw5FcZsO0
  w7UjwojDkVxmw7bDtyPCiMORXGbDuMO5I8KIw5FcZsO6w7sjwojDkVxmw7zD
  vSPCiMORXGbDvsO/I8KIw5FcZsKBQADCgUEAI8KIw5FcZsKBQgDCgUMAI8KI
  w5FcZsKBRADCgUUAI8KIw5FcZsKBRgDCgUcAI8KIw5FcZsKBSADCgUkAI8KI
  w5FcZsKBSgDCgUsAI8KIw5FcZsKBTADCgU0AI8KIw5FcZsKBTgDCgU8AI8KI
  w5FcZsKBUADCgVEAI8KIw5FcZsKBUgDCgVMAI8KIw5FcZsKBVADCgVUAI8KI
  w5FcZsKBVgDCgVcAI8KIw5FcZsKBWADCgVkAI8KIw5FcZsKBWgDCgVsAI8KI
  w5FcZsKBXFwAwoFdACPCiMORXGbCgV4AwoFfACPCiMORXGbCgWAAwoFhACPC
  iMORXGbCgWIAwoFjACPCiMORXGbCgWQAwoFlACPCiMORXGbCgWYAwoFnACPC
  iMORXGbCgWgAwoFpACPCiMORXGbCgWoAwoFrACPCiMORXGbCgWwAwoFtACPC
  iMORXGbCgW4AwoFvACPCiMORXGbCgXAAwoFxACPCiMORXGbCgXIAwoFzACPC
  iMORXGbCgXQAwoF1ACPCiMORXGbCgXYAwoF3ACPCiMORXGbCgXgAwoFRACPC
  iMORXGbCgXkAwoFTACPCiMORXGbCgXoAwoF7ACPCiMKBfADCgX0AwoF+ACBc
  IsKDZQLDkVxmwoF/AMKBwoAAI8KIwoJ9AsKBfADCgcKBAMKBfgAgXCLCg30C
  w5FcZsKBwoIAwoHCgAAjwojDj8KHIiBbeCBhdXRvLW1vZGUtYWxpc3QgY29t
  cGxldGlvbi1pZ25vcmVkLWV4dGVuc2lvbnMgY3VycmVudC1sb2FkLWxpc3Qg
  cHZzLW1vZGUtbWFwICgiXFwucHZzXFwnIiAuIHB2cy1tb2RlKSBtZW1xbCAo
  IlxcLnBwZVxcJyIgLiBwdnMtbW9kZSkgKCJcXC50Y2NzXFwnIiAuIHB2cy1t
  b2RlKSAoInB2cy1zdHJhdGVnaWVzXFwnIiAuIGxpc3AtbW9kZSkgIi5wcmYi
  ICpwdnMtbWVudS10eXBlKiBkZWZhdWx0LWJvdW5kcCBzZXQtZGVmYXVsdCBz
  aW1wbGUgbmlsIG1ha2Utc3BhcnNlLWtleW1hcCBkZWZpbmUta2V5ICIDAWYi
  IGFsbHR0LXB2cy1maWxlICIDAXQiIGFsbHR0LXRoZW9yeSAiAwFpIiBhbGx0
  dC1pbXBvcnRjaGFpbiAiAwFwIiBhbGx0dC1wcm9vZiAiAwkiIGluc3RhbGwt
  cHJvb2YgIgNzIiBpbnN0YWxsLWFuZC1zdGVwLXByb29mICIDeCIgaW5zdGFs
  bC1hbmQteC1zdGVwLXByb29mICIDXGZmIiBsYXRleC1wdnMtZmlsZSAiA1xm
  dCIgbGF0ZXgtdGhlb3J5ICIDXGZpIiBsYXRleC1pbXBvcnRjaGFpbiAiA1xm
  cCIgbGF0ZXgtcHJvb2YgIgNcZnYiIGxhdGV4LXRoZW9yeS12aWV3ICIDXGZQ
  IiBsYXRleC1wcm9vZi12aWV3ICIDXGZzIiBsYXRleC1zZXQtbGluZWxlbmd0
  aCAiA3AiIHByb3ZlICIDEHAiICIDEBAiIC4uLl0gNCkKICBsb2FkKCJwdnMt
  bW9kZSIgbmlsIG5pbCkKICBieXRlLWNvZGUoIsOGCEIQw4fDhiHChA8Aw4jD
  hsOJXCLCiMOKw4shwojDisOMIcKIw4kRw43DjiHChCQAw4/DjsOQXCLCiMON
  w5EhwoQuAMORw5JNwojDk8OUw5VcbiPCiMOTw5bDlVxuI8KIw5PDl8OVXG4j
  wojDk8OYw5VcbiPCiMOTw5nDlVxuI8KIw5PDmsOVXG4jwojDk8Obw5VcbiPC
  iMOTw5zDlVxuI8KIw5XDncOewo/CiMOTw5/DlVxuI8KIw5PDoMOVXG4jwojD
  k8Ohw5VcbiPCiMOiw6PDpCBcIsKDwpUAw6XDgyHCg8KVAAvDplnChMK1AAvD
  p1XCg8KVAFxmw6hZwoTCtQDDosOpw6QgXCLCg8K7AMOlw4MhwoPCuwALw6ZZ
  woTCtQALw6dVwoPCuwBcZsOqWcKDwrsAw5PDq8OVXG4jwojDk8Osw5VcbiPC
  iMOTw63DlVxuI8KIw5PDrsOVXG4jwojDk8Ovw5VcbiPCiMOww7HDssOzI8KI
  w7TDtcOxXCLCiMO2CEIQw4fDtiHChMOtAMOIw7bDlVwiwojDt8O4IcKDDQHD
  ucO6w7vDvMO3w70hXCJcIsKJHRY2DkBAw74NDkBBXCJCFkApw7DDv8OywoFB
  ACPChyIgW2N1cnJlbnQtbG9hZC1saXN0IGNvbWludC1sb2cgbm9uaW50ZXJh
  Y3RpdmUgZW1hY3MtbWFqb3ItdmVyc2lvbiBlbWFjcy1taW5vci12ZXJzaW9u
  IGRpcnMgc3RhcnQtcHZzIGRlZmF1bHQtYm91bmRwIHNldC1kZWZhdWx0IHQg
  cmVxdWlyZSBjbCBjb21pbnQgZmJvdW5kcCBmdWxsLWNvcHktc3BhcnNlLWtl
  eW1hcCBkZWZhbGlhcyAjWyhrbSkgIgg6woMPAMOBCEAhw4EIQSFCwocIwoci
  IFtrbSBmdWxsLWNvcHktc3BhcnNlLWtleW1hcF0gMyAiUmVjdXJzaXZlbHkg
  Y29weSB0aGUgc3BhcnNlIGtleW1hcCBLTS4iXSBjb21pbnQtbWVtIG1lbWJl
  ciBsb2FkICJpbGlzcCIgbmlsICJwdnMtaWxpc3AiICJwdnMtbW9kZSIgInB2
  cy12aWV3IiAicHZzLWZpbGUtbGlzdCIgInB2cy1icm93c2VyIiAicHZzLXV0
  aWxzIiAicHZzLWNtZHMiIChsb2FkICJwdnMtcHJlbHVkZS1maWxlcy1hbmQt
  cmVnaW9ucyIgbmlsIG5vbmludGVyYWN0aXZlKSAoKGVycm9yKSkgInB2cy1w
  cmludCIgInB2cy1wcm92ZXIiICJwdnMtYWJicmV2aWF0aW9ucyIgc3RyaW5n
  LW1hdGNoICJHTlUgRW1hY3MiIGVtYWNzLXZlcnNpb24gYm91bmRwIDIwIDE5
  IDI5ICJYRW1hY3MiIDEyICJwdnMtbWVudSIgInB2cy10Y2wiICJwdnMtcHJv
  dmVyLWhlbHBzIiAicHZzLWV2YWwiICJwdnMtcHZzaW8iIHB1dCBjb21tZW50
  LXJlZ2lvbiAuLi5dIDcpCiAgbG9hZCgicHZzLWxvYWQiIG5pbCBuaWwgbmls
  KQogIGV2YWwtYnVmZmVyKCM8YnVmZmVyICAqbG9hZCo+IG5pbCAiL1VzZXJz
  L25hdW1hbm4vcHZzNDEvZW1hY3MvZ28tcHZzLmVsIiBuaWwgdCkgIDsgUmVh
  ZGluZyBhdCBidWZmZXIgcG9zaXRpb24gMjc4MAogIGxvYWQtd2l0aC1jb2Rl
  LWNvbnZlcnNpb24oIi9Vc2Vycy9uYXVtYW5uL3B2czQxL2VtYWNzL2dvLXB2
  cy5lbCIgIi9Vc2Vycy9uYXVtYW5uL3B2czQxL2VtYWNzL2dvLXB2cy5lbCIg
  bmlsIHQpCiAgbG9hZCgiL1VzZXJzL25hdW1hbm4vcHZzNDEvZW1hY3MvZ28t
  cHZzLmVsIiBuaWwgdCkKICBjb21tYW5kLWxpbmUtMSgoIi1sb2FkIiAiL1Vz
  ZXJzL25hdW1hbm4vcHZzNDEvZW1hY3MvZ28tcHZzLmVsIikpCiAgY29tbWFu
  ZC1saW5lKCkKICBub3JtYWwtdG9wLWxldmVsKCkK
  
  --0-1441380438-1197264212=:7125--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools