forked from PrincetonUniversity/VST
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathBUILD_ORGANIZATION
119 lines (104 loc) · 5.2 KB
/
BUILD_ORGANIZATION
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
HOW TO BUILD:
0. Make sure you have the right version of Coq.
grep ^COQVERSION Makefile
will tell you which versions are compatible.
0a. Make sure you have the right version of CompCert.
VST 1.7 uses CompCert 2.7.1 for Coq 8.5pl2.
METHOD A [recommended]
This method bases the VST on a copy of certain CompCert specification
files distributed with VST, located in VST/compcert.
1. Execute this command: make
(or, if you have a multicore computer, make -j)
2. [optional, only if you're going to run "clightgen"]
Unpack CompCert in the location of your choice
(not under VST/), and in that directory,
make clightgen
CYGWIN note: Because Coq on cygwin has difficulty with absolute paths,
it's best if "compcert" and "VST" are unpacked as sibling directories
in the same parent directory, so the "../compcert" path works in step 2.
METHOD B [alternate]
This method bases the VST on the same specification files
that the CompCert compiler is built upon (in contrast to method A,
which uses verbatim copies of them).
1. Unpack CompCert in a sibling directory to VST;
in that directory, build CompCert according to the instructions
(typically: ./configure ia32-linux; make clightgen)
2. In the VST directory, create a file CONFIGURE containing exactly the text:
COMPCERT=../compcert
3. In the VST directory,
make
ORGANIZATION:
The Verified Software Toolchain is organized into separate subprojects,
each in a separate directory:
msl - Mechanized Software Library
examples - examples of how to use the msl
compcert - front end of the CompCert compiler, specification of C light
sepcomp - the theory and practice of how to specify shared-memory interaction
veric - program logic (and soundness proof) for Verifiable C
floyd - tactics for applying the separation logic
progs - sample programs, with their verifications
The dependencies are:
msl: # no dependency on other directories
examples: msl
compcert: # no dependency on other directories
sepcomp: compcert
veric: msl compcert sepcomp
floyd: msl sepcomp compcert veric
progs: msl sepcomp compcert veric floyd
In general, we Import using "-Q" (qualified) instead of "-R"
(recursive). This means modules need to be named using qualified names.
Thus, in "veric/expr.v" we write "Require Import msl.msl_standard"
instead of "Require Import msl_standard". To make this work, the loadpaths
need to be set up properly; the file ".loadpath" (built by "make .loadpath")
shows what -I includes to use.
USING PROOF GENERAL AND COQIDE:
To use either of these interactive development environments you will
need to have the right load path. This can be done by command-line
arguments to coqide or coqtop. The precise command-line arguments
to use when running CoqIDE or coqc are in the file .loadpath, which
is constructed automatically when you do "make". For example:
coqide `cat .loadpath` # will run coqide with the right options.
coqc `cat .loadpath` # will run coqc with the right options.
There are three methods in which to configure Proof General.
1) On Linux systems, use the provided vst/pg script, as follows:
./pg
This script is adapted from the CompCert project. It starts
emacs+Proof General with the load path arguments specified in
the generated .loadpath file.
2) On other systems, such as Windows, it may be necessary to specify the
load path by hand in your .emacs file, as follows:
(setq coq-prog-args
'("-I" "<your-vst-path>/msl" "-as" "msl"
"-I" "<your-vst-path>/sepcomp" "-as" "sepcomp"
"-I" "<your-vst-path>/veric" "-as" "veric"
"-I" "<your-vst-path>/floyd" "-as" "floyd"
"-I" "<your-vst-path>/progs" "-as" "progs"
"-R" "<your-vst-path>/compcert" "-as" "compcert"))
3) The (stable) development prerelease of ProofGeneral v4.3pre131011
can read the _CoqProject file in the base of the VST directory. To
enable the feature set the emacs variable coq-use-project-file.
You should now be able to open emacs normally and step into any
file in VST.
NEW DIRECTORIES:
If you add a new directory, you will probably want to augment the loadpath
so that qualified names work right. For example:
coqc `cat .loadpath` -Q new -as new new/myfile.v
The Makefile automatically creates the .loadpath file
with the subdirectories that it knows about.
EXTERNAL COMPCERT:
The VST imports from the CompCert verified C compiler, the definition
of C light syntax and operational semantics. For the convenience of
VST users, the vst/compcert directory is a copy (with permission) of
the front-end portions of compcert. We use compcert's own Makefile to
build it. However, our "Makefile.clight" modifies CompCert's
makefile, so as to build only the front end.
You may choose to ignore the vst/compcert directory and have
the VST import from a build of compcert that you have installed in
another directory, for example, ../compcert.
To do this, create a file CONFIGURE containing a definition such as,
COMPCERT=../compcert
Make sure that you have the right version of CompCert! Check
the file vst/compcert/VERSION to be sure.
Warning: On cygwin, the definition COMPCERT=../compcert
works fine, but an absolute pathname such as COMPCERT=/home/user/compcert
does not work, as coqdep breaks for some reason.