Previous Up Next

2  Getting Bedwyr

Different means of getting Bedwyr are listed on Slimmer’s INRIA Gforge project site: http://slimmer.gforge.inria.fr/bedwyr/#download. You can either download tarballs, get any development version using SVN, or use Slimmer’s unofficial Apt repository – instructions are provided on the project page. The development of Bedwyr is meant to be an open source project. If you are keen to work on the source code and/or examples, please contact one of the “Project Admins” of the project (as listed at https://gforge.inria.fr/projects/slimmer/).

2.1  Distribution layout

The Bedwyr distribution is organized as follows:

src/  Source code
doc/  Documentation – you’re reading it
contrib/  Auxiliary files – e.g. Emacs and Vim support
examples/  Examples – reading them helps

2.2  Build

Bedwyr’s main build dependency is on the OCaml compiler suite. You also need some standard tools you probably already have, especially the GNU build system (a.k.a. the autotools, especially autoconf and GNU make), bash, tar, gzip, bzip2, etc. Most of these are looked for by the configuration step.

Then, the procedure is quite simple:

 $ make

You’ll get a link to the Bedwyr executable as ./bedwyr. You can also use the expanded form to choose your building options:

 $ autoconf
 $ ./configure <configure-options>
 $ make <make-targets>

The available options and targets are listed with

 $ ./configure --help
 $ make help

By default, Bedwyr is built using the bytecode compiler ocamlc, since compilation with it is much faster. If you don’t want this (no frequent recompilation, no need for debugging), you can generate more efficient native-code instead with ocamlopt by passing the option --enable-nativecode to ./configure.

You can also enable the documentation generation by using --enable-doc and then make doc. This userguide, the quick-start guide the ocamldoc documentation will be generated in doc/.

Last, --with-xmlm/--without-xmlm will add/remove a dependency on the xmlm OCaml library, needed to produce XML output. By default, the library is not required, and the feature is included if and only if the library is found.

2.3  Test

Individual components can be tested for bugs with individual targets:

 $ make test_ndcore
 $ make test_batyping
 $ make test_input
 $ make test_prover

This longer test runs the complete program on a set of example files:

 $ make test_bedwyr

The test target runs all the previous tests, and serves as a correctness and performance test.


Previous Up Next