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:
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
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.
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.
The makefile uses this tool, which is not part of the OCaml
distribution, for macro preprocessing
.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
.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
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
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
Release.makefile if you do not.
You can use
make to build the following targets:
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. This entails a performance overhead.
*Other names and brands may be claimed as the property of others.Copyright © 2007 Intel Corporation