diff --git a/BUILD_ORGANIZATION.md b/BUILD_ORGANIZATION.md index 3eb2d44921..8fff030611 100644 --- a/BUILD_ORGANIZATION.md +++ b/BUILD_ORGANIZATION.md @@ -15,9 +15,7 @@ Otherwise please check: 2. Make sure you have the right version of CompCert. VST 2.6 uses CompCert 3.7 for Coq 8.11 -## Install Methods - -### Install via opam +## Install Method 1: use opam If you install VST via opam, opam will automatically install a suitable version of CompCert, Flocq and other dependencies. @@ -28,8 +26,15 @@ opam install coq-vst-64 ``` You can install both the 32 bit and the 64 bit versions of VST and CompCert in parallel. They will be installed in different folders. - -Please note that some opam supplied versions of CompCert use a version of +Please note that the 64 bit variants will be installed in non standard +locations and must be included explcitly with -Q or -R options: +``` +/lib/coq-variants/vst64/vst/ +/lib/coq-variants/compcert64/compcert/ +/variants/compcert64/bin/ +/variants/compcert64/lib/ +``` +Please also note that some opam supplied versions of CompCert use a version of Flocq distributed with CompCert. This is problematic if you want to verify numerical code which uses tools like CoqInterval or Gappa which also use Flocq. The proofs these tools do might then not be compatible with VST @@ -64,21 +69,23 @@ AND/OR opam install coq-compcert-64.3.7~platform-flocq~open-source coq-vst ``` -### Manual make with opam / coq-platform supplied CompCert +## Install Method 2: manual make with opam / coq-platform supplied CompCert For a manual make please follow this procedure: 1. Make sure CompCert and Flocq Coq `.vo` files are installed in ``` - /lib/coq/user-contrib/Flocq - /lib/coq/user-contrib/compcert + /lib/coq/user-contrib/Flocq + /lib/coq/user-contrib/compcert AND/OR - /lib/coq/user-contrib/compcert64 + /lib/coq-variants/compcert64/compcert ``` 2. Make sure CompCert clightgen is installed in ``` - /bin + /bin + AND/OR + /variants/compcert64/bin ``` 3. Execute this command: @@ -87,66 +94,47 @@ For a manual make please follow this procedure: OR make BITSIZE=64 ``` - (or, if you have a multicore computer, `make -j`) - -Please note that in this case you should *not* have a file `CONFIGURE` in -the VST root folder as you might for the next method. - -### Manual make with bundled CompCert - -VST includes two bundled variants of CompCert, which in some releases of -VST might include changes to support new features of VST. The bundled -variants are in the VST root folder under -``` -/compcert -/compcert_new -``` -Please note that by default VST uses a platform supplied CompCert and -not the bundled CompCert. In case you want to use one of the bundled -CompCert variants, please use these options: -``` -COMPCERT_INST_PATH=/compcert -``` -OR -``` -COMPCERT_INST_PATH=/compcert_new -COMPCERT_NEW -``` -The COMPCERT_NEW flag sets a few additional makefile options required to -build the variant in `/compcert_new` and must be set if this -folder is specified for `COMPCERT_INST_PATH`. - -You can set the additional options `BITSIZE` and `ARCH`. The supported -variants are: -``` -ARCH=x86 BITSIZE=32 (default) -ARCH=x86 BITSIZE=64 -ARCH=aarch64 BITSIZE=64 -ARCH=powerpc BITSIZE=32 -``` -Both variables can be set either on the make command line or in a file named -`CONFIGURE` in the VST source root folder which is read by the VST makefile. - -### Manual make with private build of CompCert and/or advanced options - -If you want to use a different CompCert than the default opam supplied -CompCert, you can configure the CompCert path by setting: -``` -COMPCERT=mycompcert -OR -COMPCERT_INST_PATH=/home/me/mycompcert -``` -`COMPCERT` names a Coq module path under `lib/coq/user-contrib`. -`COMPCERT_INST_PATH` names an arbitrary CompCert path, e.g. a local GIT build. - -Both variables can be set either on the make command line or in a file named -`CONFIGURE` in the VST source root folder which is read by the VST makefile. - -In addition you can define the variables `BITSIZE` and `ARCH`. If neither -`COMPCERT` nor `COMPCERT_INST_PATH` are set, `BITSIZE` can be used to -choose between `COMPCERT=compcert` and `COMPCERT=compcert64`. In any case -it is checked if `BITSIZE` and `ARCH` match the configurazion information -found in `compcert-config` in the specified CompCert folder. + (or, if you have a multicore computer, `make -j`). You may add the + target `floyd` to just build VSTs core without examples and tests. + +Please note that if you give options via teh make command line, you do +*not* have a file `CONFIGURE` in the VST root folder. + +## Install Method 3: advanced manual make, e.g. with bundled CompCert + +All options described in this section can be given in 3 ways: +- on the command line of make via `