unable to start PVS 7.1.x on OSX

[kiniry]

Hey Sam,

I wanted to migrate to PVS 7 today, but the pre-built sbcl binary fails with the following messages in *pvs*, so the front-end comes crashing down.

Starting pvs-sbclisp --noinform --no-userinit ...
Setting tmp dir to value of environment variable TMPDIR:
  /var/folders/xs/qk526nsd6hg6vjg9njg3fnc80000gp/T/

debugger invoked on a TYPE-ERROR:
  The value (:HOME ".cache" "common-lisp" :IMPLEMENTATION)
  is not of type
    (OR (VECTOR CHARACTER) (VECTOR NIL) BASE-STRING PATHNAME FILE-STREAM).

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

(no restarts: If you didn't do this on purpose, please report it as a bug.)

(PATHNAME-DIRECTORY (:HOME ".cache" "common-lisp" :IMPLEMENTATION)) [tl,external]
0] 
0] 

This failure happens even when I move my ~/.cache elsewhere.

[samowre]

Hey Joe,

Hope you're doing well.

Could you type "bac" at the "0]" prompt, and send me the resulting backtrace?

Thanks, Sam

Joseph Kiniry @.***> wrote:

Hey Sam,

I wanted to migrate to PVS 7 today, but the pre-built sbcl binary fails with the following messages in pvs, so the front-end comes crashing down.

Starting pvs-sbclisp --noinform --no-userinit ... Setting tmp dir to value of environment variable TMPDIR: /var/folders/xs/qk526nsd6hg6vjg9njg3fnc80000gp/T/

debugger invoked on a TYPE-ERROR: The value (:HOME ".cache" "common-lisp" :IMPLEMENTATION) is not of type (OR (VECTOR CHARACTER) (VECTOR NIL) BASE-STRING PATHNAME FILE-STREAM).

Type HELP for debugger help, or (SB-EXT:EXIT) to exit from SBCL.

(no restarts: If you didn't do this on purpose, please report it as a bug.)

(PATHNAME-DIRECTORY (:HOME ".cache" "common-lisp" :IMPLEMENTATION)) [tl,external] 0] 0]

This failure happens even when I move my ~/.cache elsewhere.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub, or unsubscribe.

[kiniry]

Hi Sam,

Hope you are doing well too. Perhaps I'll even get to come down and see you all before the end of this year. 🤞

Here is more context. I ran the binary directly as the *pvs* buffer interaction is hung at the failure.

Galois-2020:pvs-7.1.0> uname -a
Darwin Galois-2020.local 19.6.0 Darwin Kernel Version 19.6.0: Tue Jan 12 22:13:05 PST 2021; root:xnu-6153.141.16~1/RELEASE_X86_64 x86_64

(PATHNAME-DIRECTORY (:HOME ".cache" "common-lisp" :IMPLEMENTATION)) [tl,external]
0] bac

Backtrace for: #<SB-THREAD:THREAD "main thread" RUNNING {100CF0EA03}>
0: (PATHNAME-DIRECTORY (:HOME ".cache" "common-lisp" :IMPLEMENTATION)) [tl,external]
1: (FIX-USER-NAME-IN-DIRECTORY #<unavailable argument> #<unavailable argument>)
2: ((SB-C::TOP-LEVEL-FORM (IF (AND (BOUNDP (QUOTE *USER-CACHE*)) *USER-CACHE*) (PROGN (SETQ *USER-CACHE* (FIX-USER-NAME-IN-DIRECTORY *USER-CACHE*))) NIL)) #<unavailable lambda list>) [toplevel]
3: (SB-FASL::LOAD-FASL-GROUP #S(SB-FASL::FASL-INPUT :STREAM #<SB-SYS:FD-STREAM for "file /usr/local/pvs-7.1.0/src/asdf-patch.ppcs" {100D1A1F63}> :TABLE #(292 SET *PACKAGE* "ASDF" #<PACKAGE "ASDF/OPERATION"> OPERATION :CREATE #<PACKAGE "SB-KERNEL"> SB-KERNEL:FIND-CLASSOID-CELL :STANDARD :TOPLEVEL #<PACKAGE "SB-C"> ...) :STACK #(0 #<FUNCTION #1=(SB-C::TOP-LEVEL-FORM (IF (AND # *USER-CACHE*) (PROGN #) NIL)) {100D1AD24B}> #1# NIL (FUNCTION NIL (VALUES NULL &OPTIONAL)) NIL #(#S(SB-C::COMPILED-DEBUG-FUN :NAME #1# :KIND :TOPLEVEL :VARS NIL :BLOCKS NIL :TLF-NUMBER 4 :ARGUMENTS NIL :RETURNS :STANDARD :RETURN-PC 17 :OLD-FP 77 :NFP NIL :START-PC 63 :ELSEWHERE-PC 296 ...)) NIL "top level form" #<SB-KERNEL:LAYOUT for SB-C::COMPILED-DEBUG-INFO {1000082B83}> NIL 77 ...) :DEPRECATED-STUFF NIL :SKIP-UNTIL NIL) NIL)
4: (SB-FASL::LOAD-AS-FASL #<SB-SYS:FD-STREAM for "file /usr/local/pvs-7.1.0/src/asdf-patch.ppcs" {100D1A1F63}> NIL NIL)
5: (SB-DEBUG::TRACE-CALL #<SB-DEBUG::TRACE-INFO SB-FASL::LOAD-AS-FASL> #<FUNCTION SB-FASL::LOAD-AS-FASL> #<SB-SYS:FD-STREAM for "file /usr/local/pvs-7.1.0/src/asdf-patch.ppcs" {100D1A1F63}> NIL NIL)
6: ((FLET SB-FASL::LOAD-STREAM :IN LOAD) #<SB-SYS:FD-STREAM for "file /usr/local/pvs-7.1.0/src/asdf-patch.ppcs" {100D1A1F63}> T)
7: (LOAD #P"/usr/local/pvs-7.1.0/src/asdf-patch.ppcs" :VERBOSE NIL :PRINT NIL :IF-DOES-NOT-EXIST T :EXTERNAL-FORMAT :DEFAULT)
8: (PVS::PVS-INIT #<unavailable argument> #<unavailable argument> #<unavailable argument>)
9: (COMMON-LISP-USER::STARTUP-PVS)
10: ((FLET #:WITHOUT-INTERRUPTS-BODY-85 :IN SB-EXT:SAVE-LISP-AND-DIE))
11: ((LABELS SB-IMPL::RESTART-LISP :IN SB-EXT:SAVE-LISP-AND-DIE))

[kai-e]

Has anyone found a solution to this problem? I experience exactly the same, the buffer *pvs* shows

Starting pvs-sbclisp --noinform --no-userinit ...
environment variable TMPDIR is not a writable directory:
  /var/folders/ns/khj0j3s92fq3nhz23jh_pg_r0000gq/T/

That directory is clearly writable.

This problem occurs with pvs and sbcl from here (github) and sbcl compiled with the sbcl binary from homebrew, both on Intel and on ARM macs.