forked from SRI-CSL/PVS
-
Notifications
You must be signed in to change notification settings - Fork 0
/
INSTALL
76 lines (53 loc) · 2.82 KB
/
INSTALL
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
* Installing PVS
Note that it is generally not necessary to build PVS yourself, even if you
want to do your own development. Simply load your lisp files into a running
PVS.
From a tar file, simply untar the file, cd to the pvs-VERS directory, and
run ./install-sh you should then be able to run './pvs'. You can then copy
or link this script to a directory in your path, or add the PVS directory to
your path.
Source files are included in the tar file, but if you want the latest, get
them from Github.
* Building PVS
PVS is open source, get the latest sources using Git:
git clone https://github.com/SRI-CSL/PVS.git
The build process is described below, please feel free
to contribute your own experiences.
Note: most users do not need to build PVS, prebuilt images are already
available on the http://pvs.csl.sri.com/download.shtml page. Even
modified sources can easily be incorporated into a built image, using
~/.pvs.lisp (or simply using the load function). However, if you wish to
port to another lisp, or explore different kinds of optimizations, etc., you
will need to build it yourself. Hopefully it will not be too difficult.
In summary, the steps you need to take are:
* Obtain and install SBCL (open source) and/or Allegro (proprietary) Common Lisp
* Get the PVS sources
* Set the SBCLISP_HOME and/or ALLEGRO_HOME environment variable(s)
* Run configure and make
Obtaining and Installing Common Lisp
------------------------------------
PVS currently works with Allegro Common Lisp, which is proprietary ($$$),
and SBCL Common Lisp, which is open source. PVS is roughly twice as fast
with Allegro, so if you already have Allegro, or have extra money, it is
preferred. You can get Allegro from franz.com. PVS works best with current
Allegro versions, and probably won't work at all for versions before 6.0.
SBCL Lisp is free. Note that you can build it from source, but it's not
necessary (and apparently it is not easy).
Install as directed by these sites.
Get the PVS Sources
-------------------
Get them from the download page, create a directory, cd to it, and untar the
sources.
Set either the ALLEGRO_HOME or SBCLISP_HOME environment variable. If using
SBCL, you may need to chmod a+x <sbcl>/run-sbcl.sh
----------------------------------------------------------------
For Allegro, set ALLEGRO_HOME to the directory containing the license file
(devel.lic). SBCLISP_HOME is the directory containing run-sbcl.sh
Note: if you have multiple lisps, you can set all desired variables and the
make will create all images.
Run ./configure and make
Configure should be straightforward. Note you generally need to run it only
once, even if you are building for many platforms.
Make may cause some problems, we had some issues with getting the right GCC
versions, especially for Mac and Solaris. If you have problems and/or
solutions, please let us know