Building tamarin prover on windows

Building tamarin prover on windows

Notes

• I checked out the git repository on my network homedir. Changing the directory in cmd.exe to a network share works using the command pushd \\d.ethz.ch\dfs\users\m\meiersi. Adapt the last to parts to your user-name, if required.
• Setting the Path variable in Windows 7 is described here. The path is C:\Users\meiersi\AppData\Roaming\cabal\bin.
• It is possible to "install" the maude version from MOMENT by just unzipping the downloaded executable into the tamarin-prover directory. Then using the flag --with-maude=maude/maude.exe works at least for detecting the maude version.

Known Issues

This is a list of issues, I had on Feb 22th 2012 while building tamarin-prover (from #cd5d399800) on the student lab Windows 7 machines using the Haskell platform HP 2011.2.0.1.

• symlinks in git repo (etc and examples) do not work and make a proper install fail. For now, I removed all references to these files in tamarin-prover.cabal. We'll have to see what a good solution is in the future.
• The maude install on windows cannot resolve paths very well, as it uses an internal cygwin.dll.
• Trying to install with the GUI did not work due to dependency resolution problems. Building the cabal install -fno-gui works.
• The error messages from a failed interaction with the maude executable are incomprehensible. (Currently, *** Exception: fd:10: hGetChar: end of file)

TODO

• Change directory structure such that all files required for building the source distribution and installing tamarin-prover from the repository version are real files and no symlinks; i.e, use symlinks to provide convenient locations for development on unix-style OSes.
• Ensure that tamarin-prover test uses the right path provided with --with-maude [DONE 77eb74fdb211650f1da914fef3ff99043619b08e]
• Fix the file resolution problem by piping the maude theory directly into stdin instead of using a temporary file.
• Improve the Term.Maude.Process infrastructure such that the most recent content of stdin/stdout/stderr are output or attached to the exception message.