-- ___ ___ ___ __________ ________ __________ -- / / / / / / /___ ___/ / ____ \ / ____ / -- / / / / / / / / / /___/ / / /___/ / -- / / / / / / / / / __ __/ / ____ / -- / /___/ / / /______ / / / / \ \ / / / / -- /_________/ /_________/ /__/ /__/ \__\ /__/ /__/ -- -- Functional program transformation environment, Version 3.0 -- No copyrights yet 1997-1999; 2006. README for the ULTRA program transformation system version 3.0 (2006-09-02) 1. License and (lack of) warranty 2. Release Notes 3. Installation Requirements 4. Installation of HTk 5. Installation of Programatica 6. Installation 7. Usage 8. Clauses 9. Precompilation (so ULTRA starts faster) 10. Contact --------------------------------------------------------------------------- 1. License and (lack of) warranty The ULTRA program transformation system is provided as free software. For details see the file COPYING. Note that there is no warranty of any kind for the ULTRA system; use it at your own risk! --------------------------------------------------------------------------- 2. Release Notes Version 3.0 of the ULTRA system is a major rewrite. The most important changes include: - The source code was ported from Gofer to Haskell. - The GUI was re-implemented with the HTk toolkit. - The custom parser and typechecker were replaced with an interface to the Programatica tools. - As a result, the ULTRA system can now handle almost the full Haskell language as its object language. - Also, there is support for the Haskell module system (including mutually recursive modules). - Theory files are now plain Haskell modules, and can be loaded in any Haskell implementation. Notable deficiencies you should be aware of: - Explicit type declarations are not supported. They will be ignored when unfolding a function. Neither is the monomorphism restriction. - The Programatica front-end is quite slow. - The HTk text editor widget does not allow disabling text selection, so when you mark multiple terms, the result is quite ugly. --------------------------------------------------------------------------- 3. Installation Requirements You need the following software to run ULTRA: - The libraries that the GHC run-time depends on. I believe this is just the GNU MP library (libgmp). - Tcl (version 8.4.9) and the Tk toolkit (version 8.4.9). http://www.tcl.tk/ - The Tix extension of Tk (version 8.1.4). http://tix.sourceforge.net/ - Some Haskell standard libraries that can be used by Programatica. http://www.cse.ogi.edu/~hallgren/Programatica/download/HierarchicalLibs.tar.gz You need the following software to build ULTRA from source: - GHC, the Glasgow Haskell Compiler, version 6.2.2. We have tested on both PowerPC and x86 architectures. Later versions might work, but this is untested. http://www.haskell.org/ghc/ - HTk, version 1.00. We have used a checkout from the CVS branch ghc-6-02, dated 2006-03-09. http://www.informatik.uni-bremen.de/htk/ - The Programatica tools. We have used a checkout from the CVS HEAD branch, dated 2006-04-23. http://www.cse.ogi.edu/PacSoft/projects/programatica/ - The build tool make. We have used GNU Make 3.80. http://www.gnu.org/software/make/ - A C pre-processor (cpp). We have used the one from the GNU Compiler Collection, version 3.3.5. http://gcc.gnu.org/ - Haddock, the Haskell documentation tool, version 0.6 (only required to build the HTML API documentation). http://www.haskell.org/haddock/ --------------------------------------------------------------------------- 4. Installation of HTk You need to install HTk if you want to build ULTRA from source. You can simply use the binary release version 1.00 that is available on the HTk homepage. http://www.informatik.uni-bremen.de/htk/download/INSTALL.BINARY.html Note that installing HTk is not required for using binaries of ULTRA. However, there is a major bug: If you open a file picker dialog (say, to load a theory file), and then close it via the window manager, the entire GUI will crash irrecoverably. We have a patch for this bug, but it requires building HTk from source. This is because the HTk authors at the University of Bremen have ceased development, and have not acted on the bug report we sent them. Note that the HEAD branch of HTk CVS only works with GHC 6.4. We have not tested this. Let us know if it works. For GHC 6.2, you need the CVS branch ghc-6-02. http://www.informatik.uni-bremen.de/uniform/wb/cvs/index.html You need to apply the following patch: patches/HTk-FileDialog.diff fixes a crash bug in the HTk file dialog (version 1.00 with GHC 6.2.2) First, check out HTk from the CVS repository: $ cvs -z3 -d:pserver:cvsread@cvs-agbkb.informatik.uni-bremen.de:/repository co -rghc-6-02 uni Then, apply the patch: $ cd uni $ patch -p1 < $ULTRADIR/patches/HTk-FileDialog.diff Then, configure and compile HTk: $ ./configure --prefix=$HOME/ultra/htk-1.00-ghc6.2.2 --enable-HTk --disable-Het $ make boot $ make packages Now you can create a tarball with the binaries necessary to link against HTk: $ make prepareexports $ make exports If you want, you can create the HTML API documentation for HTk with Haddock: $ make haddock You can extract the tarball created with "make exports" anywhere, and then run the contained script "install" to fix up the path names: $ ./install --------------------------------------------------------------------------- 5. Installation of Programatica Unfortunately, in order to build ULTRA from source you need to install Programatica from source. Worse yet, the Programatica build system is quite broken, or rather, it does not do what we want. What we want is a GHC package we can link to. We have created the following patches to build Programatica: patches/programatica.pkg: a package definition file for programatica patches/Programatica-HuMake.diff: necessary to get Programatica to build if you do not have a 'mtl' package patches/Programatica-Show.diff necessary only if you want to create your own precompiled Catbase First, you need to download the Haskell libraries that will be used by the front-end, and check out Programatica from its CVS repository: $ curl -O http://www.cse.ogi.edu/~hallgren/Programatica/download/HierarchicalLibs.tar.gz $ cvs -d :pserver:anoncvs@cvs.haskell.org:/cvs login $ cvs -z3 -d :pserver:anoncvs@cvs.haskell.org:/cvs checkout programatica The following directory can be removed to recover some disk space: $ cd programatica/ $ rm -r tools/semantics/ Then, apply the patches from the patches/ directory: $ cd tools $ patch -p0 < $ULTRADIR/patches/Programatica-HuMake.diff $ patch -p0 < $ULTRADIR/patches/Programatica-Show.diff Now, configure and compile the Programatica tools: $ PGM_INST_DIR=$HOME/ultra/programatica-20060620-ghc6.2.2 $ touch pfe/Browser/InternetLib $ touch scripts/hsfudmake.sh $ ./configure At this point, there will be an error message; we do not need the Programatica GUI, so ignore it and continue... Note that we give GHC the "-package-name" flag; otherwise the package would be called Main. Also note that we do not build the "hs2alfa/apfe" frontend that would normally be built by the Programatica build system; instead, we build the "pfe/pfe" frontend, which is a lot smaller because it does not contain interfaces to every theorem prover known to man. $ make PREFIX=$PGM_INST_DIR "SUBDIRS=evman pfe" "HFLAGS=-package-name programatica" $ make PREFIX=$PGM_INST_DIR "HFLAGS=-package-name programatica" TARGETS=pfe OPT=-O -C pfe $ make PREFIX=$PGM_INST_DIR "SUBDIRS=evman pfe" "HFLAGS=-package-name programatica" template $ ln -sf ../pfe/pfe bin/pfe If you want, you can convert the Programatica source code to HTML. This is very convenient if you actually want to learn about its API. $ tar xzvf ../../HierarchicalLibs.tar.gz $ PATH=bin:$PATH PROGRAMATICA=lib/Programatica TARGET=apfe bin/pfesetup +h noplogic cpp pfe/pfe.hs pfe/pfeclient.hs $ bin/pfe noplogic webpages Now we need to build a GHC package for Programatica. This must be done by hand because the Programatica build system provides no support for doing this. Note that the modules UTF8 and UTF8Util conflict with HTk. HTk also contains modules with the same names, and GHC cannot cope with duplicate modules, so we need to remove them from the package library. $ mkdir imports $ B=base $ PGM_SRC_DIRS=$B/parse2:$B/parse2/Lexer:$B/parse2/Parser:$B/pretty:$B/AST:$B/syntax:$B/lib:$B/lib/Monads:$B/Modules:$B/defs:$B/TI:$B/transforms:$B/transforms/Deriving $ for dir in $(echo $PGM_SRC_DIRS | sed "s/:/ /g"); do cp $dir/*.hi imports; done $ for dir in $(echo $PGM_SRC_DIRS | sed "s/:/ /g"); do echo $dir/*.o; done | xargs ar cqs libHSprogramatica.a $ ar d libHSprogramatica.a UTF8.o UTF8Util.o PPU.o $ ln -s $PWD $PGM_INST_DIR $ echo [] > package.conf $ installdir=$PGM_INST_DIR ghc-pkg --auto-ghci-libs --config-file package.conf -a < $ULTRADIR/patches/programatica.pkg --------------------------------------------------------------------------- 6. Installation The easiest way to use ULTRA is to use the binary release. This is known to work on Debian GNU/Linux 3.1. Whether this works on other linux distributions depends on ABI compatibility of the GNU MP library, and libc. We don't know. The following should install all run-time dependencies: $ apt-get install libgmp3 tcl8.4 tk8.4 tix8.1 Also, you need to put the Haskell libraries where the Programatica front-end can find them. This can only be configured at compile time. But if you just untar the file HierarchicalLibs.tar.gz in the top directory of ULTRA (the one that contains this README), ULTRA should find the libraries. Building ULTRA from source is a bit more complicated, mostly because you will need to install Programatica and HTk as well. ULTRA has a Makefile which can be used for building. You have to give the paths where you have installed the Programatica tools and HTk: $ make HTK_DIR=/home/x/htk-1.0-ghc6.2.2 PGM_DIR=/home/x/programatica-ghc6.2.2 You can also use GHCi, in which case you have to adapt the paths in the .ghci configuration file. If you have Haddock, you can build the API documentation, which will be put in the directory haddock-html: $ make haddock --------------------------------------------------------------------------- 7. Usage There is a user manual for the ULTRA system. This manual describes the previous version of the ULTRA system, namely, version 2.2. However, we believe that for the most part it is still an accurate description of the current version of ULTRA. The manual can be downloaded from: http://www.informatik.uni-ulm.de/pm/projekte/ultra/ For an overview of ULTRA and a derivation of Heapsort see: W. Guttmann, H. Partsch, W. Schulte, T. Vullinghs Tool Support for the Interactive Derivation of Formally Correct Functional Programs Journal of Universal Computer Science, 9(2):173-188, 2003 http://www.jucs.org/jucs_9_2/tool_support_for_the/ --------------------------------------------------------------------------- 8. Clauses ULTRA theories are represented by standard Haskell modules. Representing transformation rules in this way is no problem: they can simply be represented as Haskell functions, using some special operators which are defined in the module Theory.Prelude. The clauses that constitute the fact database of ULTRA, however, use a custom syntax that is not valid Haskell. Such clauses can be defined in a specially marked comment section, from which they will be extracted when loading the file into ULTRA. The clause section begins at a line like this: {-*** CLAUSES and ends at a line like this: ***-} In between, you can use a prolog-inspired syntax to define facts. Note that all identifiers that are used in the clause section must be in scope, because the clauses are converted to Haskell function definitions, and are scope checked as such. The clause parser is a bit of a hack, so don't try anything too complicated. For example: {-*** CLAUSES lneutral (+) 0 rneutral (+) 0 neutral f e :- lneutral f e, rneutral f e ***-} --------------------------------------------------------------------------- 9. Precompilation (so ULTRA starts faster) Because the speed of our Programatica front-end leaves a bit to be desired, we have implemented support for precompiling the Catbase of ULTRA, which contains all the information about the loaded modules. When using a precompiled Catbase, startup of ULTRA is This requires patching the Programatica tools, as described in section 5 of this README. In order to dump the Catbase to some files in /tmp, there is the menu entry "Compile Theories...", which is only available in expert mode. To use the dumped files, move them into the directory Ultra/Frontend/Programatica, and define the preprocessor macro ULTRA_USE_PRECOMPILED (and increase the stack size of GHC): $ make HCFLAGS = -DULTRA_USE_PRECOMPILED +RTS -K24M -RTS Note that the dumped Catbase files are huge, and compiling them with GHC takes lots of time and memory. If you want to limit the amount of memory GHC uses you can use the flag -M. We have found that -M450M is sufficient to compile a dumped Catbase consisting of the modules Prelude, Hugs.Prelude, Ix, Data.Ix and Theory.Prelude. --------------------------------------------------------------------------- 10. Contact If you have installation issues, or have found a bug, or have fixed a bug (we really like that), or just want to comment on ULTRA, please do not hesitate to contact us. The person responsible for the current implementation and its bugs: concat ["michael.stahl", [chr 64], "informatik.uni-ulm.de"] The person responsible for future development: concat ["walter.guttmann", [chr 64], "uni-ulm.de"] ---------------------------------------------------------------------------