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/).
The Bedwyr distribution is organized as follows:
|doc/||Documentation – you’re reading it|
|contrib/||Auxiliary files – e.g. Emacs and Vim support|
|examples/||Examples – reading them helps|
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:
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
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
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
--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.
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
test target runs all the previous tests, and serves as a
correctness and performance test.