Bump version to 0.9.0, update README and CHANGES

CHANGES

@@ -1,8 +1,19 @@
-* 1.0.0
+* 0.9.0
   - Improve build-stability by switching to Stackage-based precise
-    version-constraints.
-  - Add support for building tamarin-prover on GHC 7.8.X and 7.6.X
-  - Drop support for building tamarin-prover on GHC 7.4.X and lower.
+    version-constraints: tamarin-prover should now build under GHC
+    7.8.4, GHC 7.6.2, and GHC 7.4.2. See
+
+      https://travis-ci.org/tamarin-prover/tamarin-prover
+
+    for it's build status.
+
+  - Make executable relocatable => this means we can now offer pre-built
+    binaries. This is the preferred way for distributin tamarin-prover. We no
+    longer support publishing to Hackage and downloading from Hackage.
+
+  - We no longer include examples, manuals, and licence files. They should be
+    downloaded from the github repository:
+    https://github.com/tamarin-prover/tamarin-prover
 
 * 0.8.6.0
   - Incorporate a patch contributed by Ognjen Maric that improves reasoning

Makefile

@@ -15,7 +15,8 @@ install: build-setup
 	cabal --version  # Should be at least 1.18
 	$(CABAL_INSTALL) --force-reinstalls .
 
-build-setup: cabal-sandbox/created $(ALEX) $(HAPPY)
+# build-setup: cabal-sandbox/created $(ALEX) $(HAPPY)
+build-setup: cabal-sandbox/created
 	cabal sandbox add-source lib/*
 
 # Create a sandbox shared between the tamarin-prover its custom libraries.
@@ -50,7 +51,7 @@ $(HAPPY): cabal-sandbox/created
 # ###########################################################################
 
 
-VERSION=0.8.5.1
+VERSION=0.9.0
 
 
 source-dists:

README.md

@@ -1,32 +1,19 @@
 The Tamarin prover repository
 =============================
+![master branch build-status](https://travis-ci.org/tamarin-prover/tamarin-prover.svg?branch=develop)
 
 This README describes the organization of the repository of the Tamarin prover
 for security protocol verification. Its intended audience are interested
 users and future developers of the Tamarin prover. For installation
 and usage instructions of the Tamarin prover see:
 http://www.infsec.ethz.ch/research/software/tamarin.
 
-TODO: Usage and build instructions
+TODO: @cas, installation, usage, and examples (see #147)
 
 
 Developing
 ----------
 
-TODO: development instructions
-TODO: pinning instructions (switch template-haskell and base to 'installed')
-
-          array ==0.4.0.1,
-          deepseq ==1.3.0.1,
-          ghc-prim ==0.3.0.0,
-          old-locale ==1.0.0.5,
-          old-time ==1.1.0.1,
-          time ==1.4.0.1,
-          template-haskell,
-          base
-
-
-
 We use Linux and Mac OS X during the development of Tamarin. Windows can be
 used for development, but the directory layout simplification introduced via
 symbolic links will not work.
@@ -36,22 +23,33 @@ http://nvie.com/posts/a-successful-git-branching-model/.
 We moreover use the Haskell coding style from
 https://github.com/tibbe/haskell-style-guide/blob/master/haskell-style.md.
 
-The simplest way to start developing is to call `make force-install` in the
-root directory of this repository. This installs the repository versions of
-the `tamarin-prover` package and its supporting libraries
-`tamarin-prover-utils`, `tamarin-prover-term`, and `tamarin-prover-theory`
-in the global package database. Once this succeeded, compatible versions of
-all libraries required by the `tamarin-prover` are also installed in the
-global package database. Thus, you can load the `Main` module of the Tamarin
-prover by typing `ghci Main` in the root directory of this repository. Note
-that, if GHCi prints
+We manage the Haskell dependencies using 'cabal sandbox'es with all transitive
+dependencies pinned in the 'cabal.config' file. To bootstrap development, you
+should run a successful sandboxed installation by calling 'make install' in
+the repositories root directory. This will build the tamarin-prover executable
+at
 
-~~~~
-*** WARNING: /home/repositories/git/github/meiersi/tamarin-prover/.ghci is writable by someone else, IGNORING!
-~~~~
+  cabal-sandbox/bin/tamarin-prover
+
+This file is relocatable and you can copy it anywhere you'd like. Also to
+other systems with the same 'libc' and 'libgmp' libraries.
+
+To enter the GHCi repl, type
+
+  cabal repl
+
+in the root directory of this repository. If you are working on one of the
+tamarin-prover-XXX libraries, you can use GHCi to load them by typing 'cabal
+repl' in their respective root directory.
+
+The static web assets are embedded into the built binary in the file
+'src/Web/Dispatch.hs'. See the note on 'staticFile' on how to enable dynamic
+reloading in case you are working on the web assets.
 
-, then you have to `chmod g-w` the directory `.` and the GHCi configuration
-file `.ghci`.
+The variants of the intruder rules for Diffi-Hellman exponentiation and
+Bilinear-Pairing are embedded statically in 'src/Main/TheoryLoader.hs'. If you
+change them, then this file needs to be recompiled for the changes to come
+into effect.
 
 Note that we welcome all contributions, e.g., further protocol models. Just
 send us a pull request.

lib/term/tamarin-prover-term.cabal

@@ -2,7 +2,7 @@ name:               tamarin-prover-term
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.0.0
+version:            0.9.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

lib/theory/tamarin-prover-theory.cabal

@@ -2,7 +2,7 @@ name:               tamarin-prover-theory
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.0.0
+version:            0.9.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

lib/utils/tamarin-prover-utils.cabal

@@ -2,7 +2,7 @@ name:               tamarin-prover-utils
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            1.0.0
+version:            0.9.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers

src/Web/Dispatch.hs

@@ -68,7 +68,8 @@ getFaviconR = redirect (StaticR faviconRoute)
 getRobotsR :: Handler RepPlain
 getRobotsR = return $ RepPlain $ toContent ("User-agent: *" :: B.ByteString)
 
--- | NOTE (SM):
+-- | NOTE (SM): See the note on 'staticFiles' below on how to enable dynamic
+-- reloading.
 staticFiles :: Yesod.Static.Static
 staticFiles = $(Yesod.Static.embed "data")
 
@@ -94,7 +95,8 @@ withWebUI readyMsg cacheDir_ thDir loadState autosave thLoader thParser debug'
     thy    <- getTheos
     thrVar <- newMVar M.empty
     thyVar <- newMVar thy
-    -- st     <- static stPath
+    -- NOTE (SM): uncomment this line to load the assets dynamically.
+    -- staticFiles     <- Yesod.Static.static "data"
     when autosave $ createDirectoryIfMissing False autosaveDir
     -- Don't create parent dirs, as temp-dir should be created by OS.
     createDirectoryIfMissing False cacheDir_

tamarin-prover.cabal

@@ -1,7 +1,7 @@
 cabal-version:      >= 1.10
 build-type:         Simple
 name:               tamarin-prover
-version:            1.0.0
+version:            0.9.0
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -156,9 +156,9 @@ executable tamarin-prover
       , yesod-json
       , yesod-static
 
-      , tamarin-prover-utils  == 1.0.0
-      , tamarin-prover-term   == 1.0.0
-      , tamarin-prover-theory == 1.0.0
+      , tamarin-prover-utils  == 0.9.0
+      , tamarin-prover-term   == 0.9.0
+      , tamarin-prover-theory == 0.9.0
 
     other-modules:
       Paths_tamarin_prover