PVS on M1 Mac

[yl182]

Hello,

I am a student working on a project using PVS on an M1-chip Mac. It looks like PVS and the PVS extension from VSCode marketplace is not able to do typechecking. Would it be possible that this issue can be resolved and PVS can be compatible with M1-chip Macs in the next few weeks or months?

Thank so much in advance.

[kai-e]

Why won't I share how far I've come with this today. I hadn't tried recently because I failed for a long time to get PVS build with SBCL even on an Intel Mac. Rather than a complete recipe for success, it's not quite there yet but I'd like to share what I have so others can chime in. It does look like we're almost there!

Preparation

I have Xcode, its cmd line utils, Emacs for Mac OS X, and homebrew installed.

From memory I did (at least):

$ brew install llvm sbcl emacs

follow the Caveats at the end.

Clone the PVS and SBCL git repos (say, into ~/src).

Build SBCL

Build and install that SBCL. I used

$ cd ~/src/sbcl
$ sh make.sh --prefix=/Users/kaie/opt/sbcl --dynamic-space-size=4Gb

(Iirc the --prefix didn't work with ~/opt/sbcl.) Currently that succeeds with

//checking for leftover cold-init symbols
Found 5:
(#:*!DELAYED-DEFMETHOD-ARGS* #:!EARLY-GF-NAME #:!BOOTSTRAP-SET-SLOT
 #:!BOOTSTRAP-SLOT-INDEX #:!HAIRY-DATA-VECTOR-REFFER-INIT)
Found 5 fdefns named by uninterned symbols:
(#<SB-KERNEL:FDEFN #:TOKENS> #<SB-KERNEL:FDEFN #:!EARLY-GF-NAME>
 #<SB-KERNEL:FDEFN #:!BOOTSTRAP-SET-SLOT>
 #<SB-KERNEL:FDEFN #:!BOOTSTRAP-SLOT-INDEX>
 #<SB-KERNEL:FDEFN #:!HAIRY-DATA-VECTOR-REFFER-INIT>)

near the end. Let's hope that that's not fatal.

Install quicklisp.

Install PVS dependencies (found via trial and error).

$ sbcl
* (ql:quickload "BABEL")
[...]
* (ql:quickload "CLACK")
[...]
* (ql:quickload "WEBSOCKET-DRIVER")
[...install hangs at the end?...C-c and go again with the rest...]
* (ql:quickload "HUNCHENTOOT")
[...]
* (ql:quickload "ANAPHORA")
[...]
* (ql:quickload "LPARALLEL")
[...]
* (exit)

Build PVS

(Showing a little gotcha.)

$ sh install.sh
$ cd ../PVS
$ make clean && ./configure && make
[...]
Makefile:77: *** "SBCL_HOME/run-sbcl.sh not found".  Stop.
$ env | grep SBCL
SBCLISP_HOME=/Users/kaie/src/sbcl
SBCL_HOME=/Users/kaie/opt/sbcl/lib/sbcl
$ export SBCL_HOME=$SBCLISP_HOME

(Perhaps the sbcl install step above was useless because it did not make available that precious run-sbcl.sh also missing from the brew-installed version. After this sbcl won't work in this directory but PVS compiles.)

$ make
[...]
***** make-in-platform /Users/kaie/src/PVS/src/utils/ file_utils 2
debugger invoked on a SIMPLE-ERROR in thread
#<THREAD "main thread" RUNNING {70052B0A73}>:
  Failure in make -C /Users/kaie/src/PVS/src/utils//arm-MacOSX:
output:
clang  -g -O2 -Wall -pedantic -std=gnu99 -mtune=native -mcpu=apple-a14 -c ../file_utils.c -o file_utils.o
clang  -g -O2 -Wall -pedantic -std=gnu99 -mtune=native -mcpu=apple-a14 -c ../utils_table.c -o utils_table.o
/opt/homebrew/Cellar/llvm/14.0.6_1/bin/ld64.lld -dylib -flat_namespace -undefined suppress -arch arm64 -platform_version macos 11.0.0 12.0 -o file_utils.dylib file_utils.o utils_table.o
error output:
make[1]: /opt/homebrew/Cellar/llvm/14.0.6_1/bin/ld64.lld: No such file or directory
make[1]: *** [file_utils.dylib] Error 1

Even after confirming that we're using the brew-installed llvm and

$ export LDFLAGS="-L/opt/homebrew/opt/llvm/lib"
$ export CPPFLAGS="-I/opt/homebrew/opt/llvm/include"

the same error persists. Why? Because ./configure asks gcc for its version and gcc is from apple's cmd line tools! It detects the wrong version, 14.0.6_1 in my case. I do have 16.0.0 installed via homebrew. So in let's cheat with something like

$ pushd
$ cd /opt/homebrew/Cellar/llvm
$ ln -s 16.0.0 14.0.6_1
$ popd
$ make

Test

$ export PVSEMACS=/Applications/Emacs.app/Contents/MacOS/Emacs # for a windowed PVS
$ ./pvs -q # could append `-load-after ~/.emacs`

This runs and looks almost healthy. I test by M-x cc to where I have .pvs files and M-x ff to open one. I seem to be able to parse and typecheck, but proving fails.

In *PVS Error*:

Cannot find library finite_sets

In *pvs*:

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

debugger invoked on a SB-KERNEL::UNDEFINED-ALIEN-FUNCTION-ERROR @300000374 in thread
#<THREAD "main thread" RUNNING {700EDE0003}>:
  The alien function "bdd___BDD_bdd_init" is undefined.
[...]

After a M-x rest-pvs the buffer *PVS Error* changes to

Could not find lib-path for finite_sets/

The value of pvs-library-path is nil.

[kai-e]

This now builds (for me). It would be great if others could test out my PVS build instructions for ARM-based Macs so we catch problems before this can, maybe, make it into the official distribution.

[yl182]

Worked for me! Thanks for this update.