Installation

Prerequisites and Configuration

The Decision Procedure Toolkit (DPT) may be downloaded from SourceForge.net.^* It is written in Objective Caml, and you will need to install the following tools before you can build it:

Objective Caml

The makefile uses the native-code versions of the OCaml tools, so when you build OCaml you will need to make world.opt. See the OCaml INSTALL file for more information. Alternatively, you can edit Config.makefile to select byte-code versions of the OCaml tools.

We use version 3.10.1 of Objective Caml. Version 3.09 will also build the system, but gives some errors when building the documentation. We use the godi package manger to install OCaml, but it is not necessary to do so.

ocamldsort

The makefile uses this tool, which is not part of the OCaml distribution, to sort dependencies.

We use version 0.14.1 of ocamldsort, but other versions may also work. You can use the godi package manager to install ocamldsort, as we do, but it is not required.

camlp5

The makefile uses this tool, which is not part of the OCaml distribution, for macro preprocessing .ml and .mli files. We use camlp5 only in ways where it and camlp4 (which is part of the standard distribution) should behave the same, but camlp4 currently has some problems processing .mli files when used in conjunction with the ocamldoc documentation generation tool. If you do not wish to use to build documentation you can use camlp4 instead, just change the reference to camlp5o in Config.makefile to camlp4o.

We use version 5.07 of camlp5, but other versions may also work. You can use the godi package manager to install camlp5, as we do, but it is not required.

Configurable build options may be set in Config.makefile, though you may not need to alter anything. Preparing a release uses Perl, lynx, and nsgmls. You probably have these tools on your system, but you can select alternatives in Release.makefile if you do not.

Building

You can use make to build the following targets:

opt

Native code versions of the DPT executables.

byte

Byte code versions of the DPT executables.

top

An OCaml interpreter with the DPT components integrated.

doc

Documentation.

all

All of the above.

default

By default make builds the opt and doc targets.

release

Does some minor validation against coding guide lines and attaches acknowledgment notices to documentation for hosting on SourceForge.net

The first time you build (the documentation), the system will build an index of the OCaml standard library in “doc/out/stdlib.dump” for cross referencing. This process may generate some error messages as the OCaml standard library is not processed cleanly by the ocamldoc indexing tool. These error messages (shown below) can be safely ignored, and you should not see them again unless you delete the index file.

File ".../std-lib/outcometree.mli", line 94, characters 54-75:
Unbound type constructor Asttypes.private_flag
1 error(s) encountered
make: [.../public/doc/out/stdlib.dump] Error 1 (ignored)

The make system understands the following options:

FAST=1

Build the DPT executables configured for maximum execution speed. Among other things, this option turns off the extensive run-time assertion checking that DPT performs when built with the default configuration.

DEBUG=1

Enable the OCaml debugger and stack traces. This entails a performance overhead.

PROFILE=1

Build the DPT executables with options that support profiling, but are otherwise similar to the options used when FAST=1. This entails a performance overhead.

^*Other names and brands may be claimed as the property of others.

Hosted by the ^* web site.
^*Other names and brands may be claimed as the property of others.