ruhler / smten

Compiler and runtime of the Smten language for functional programming and orchestration of SMT queries
http://ruhler.github.io/smten
Other
19 stars 8 forks source link

Smten (Developer) README

Richard Uhler ruhler@csail.mit.edu June 2014

Non-Developer Smten Installation

If you do not wish to modify the smten implementation, it is easier to build and install smten using distributed cabal packages. See tutorials/T1-GettingStarted.txt for how to do this.

This document describes how to build the distributed cabal packages, which is only needed if you desire to modify the smten implementation.

Configuring Smten for Development Build

Before building smten using the makefile, you must configure the build for your system. This is done by creating the file "tclmk/local.tcl" containing information about your system.

The following variables should be set in tclmk/local.tcl: ::env(PATH) - The PATH to use for executables ::env(LD_LIBRARY_PATH) - the ld library path ::GHC - the path the the ghc executable to use

For example, tclmk/local.tcl might look like:

========================================= set ::env(PATH) "/bin:/usr/bin:/home/ruhler/local/bin" set ::env(LD_LIBRARY_PATH) "/home/ruhler/local/lib" set ::GHC "/home/ruhler/local/bin/ghc"

Yices1, Yices2, STP and Z3

The tests for Smten currently require yices1, yices2, STP, and Z3 to be installed. See the documentation in tutorial/T3-SMTBackends.txt for information on how to install them.

Building Smten

Once smten is configured for build and the required SMT solvers are installed, it can be built by running make. The following targets are supported:

all:: Build all the smten packages locally and run the test suites for them. For the location of the generated cabal distribution packages, run: + find build -name "smten*.tar.gz"

userinstall:: Build all the smten packages locally, run the test suites, and then install the packages into the current users account.

userinstall2:: Install the packages into the current users account without first building them locally. This requires you have already built the packages locally.

clean:: Clean up the locally generated cabal packages.

fullclean:: Remove the entire local 'home' directory, including any packages already installed locally which smten depends on.

Documentation

The 'doc' directory contains mostly out-of-date documents. The most relevant documents now are:

doc/todo.txt:: contains a brief list of known issues and planned work to do. doc/history.txt:: contains the release history of smten.

For user documentation, consult the generated haddock documentation after building the packages locally at build/home/.cabal/share/doc/index.html or build/smten-/dist/doc/html/smten-/index.html for the individual packages. There are also some tutorials on using Smten in the 'tutorials' directory.