Skip to content

Latest commit

 

History

History
147 lines (107 loc) · 6.67 KB

CONTRIBUTING.md

File metadata and controls

147 lines (107 loc) · 6.67 KB
Raw

Developing and contributing to tamarin-prover

We use Linux during the development of Tamarin. Mac OS X can be used just as well. Windows is not recommended as no testing is possible (due to GraphViz and Maude) and additionally the directory layout simplification introduced via symbolic links will not work.

As of October 1st, 2012, we started organizing our branches according to 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.

We manage the Haskell dependencies automatically, using 'stack'. Install 'stack' according to https://github.com/commercialhaskell/stack/blob/master/doc/install_and_upgrade.md

After cloning this repository run 'make default', which will install an appropriate GHC for your system, including all dependencies, and the tamarin-prover executable will be copied to

~/.local/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.

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.

The variants of the intruder rules for Diffie-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.

Making new releases

The Tamarin Prover is distributed through a number of channels: source and binaries through Github, and packages through Homebrew, Arch and NixOS. A new release should be made whenever a major new feature has been added, some significant bug(s) have been fixed, a new version of GHC should be used (possibly necessary due to MacOS auto-update), or whenever the maintainers deem it desirable. When a new release is cut, here's how to prepare the release first and then update the various distribution channels.

  1. Make the new release on Github. @rsasse or @jdreier usually does this.

    1. run 'make case-studies' and compare 'case-studies/' with 'case-studies-regression/'

    2. run 'tamarin-prover test'

    3. call 'tamarin-prover' and copy CSF'12 automatic command and check whether verification succeeds, i.e., run 'tamarin-prover --prove *.spthy' in the examples/csf12 folder.

    4. generate 'intruder_variants_{dh,bp}.spthy' and diff with versions in data/ so: 'tamarin-prover variants > tmp.txt' 'diff tmp.txt data/intrudervariants_both_bp_dh_for_diff.txt' which should be empty.

    5. call 'tamarin-prover' and copy CSF'12 interactive command and execute the following steps in the GUI after running 'tamarin-prover interactive .' in the examples/csf12 folder.

      (a) open one of the presented theories (b) try shortcuts (J,K,j,k,1,2,..,a) (c) try different graph/sequent options (d) try Download (e) try 'Loading a new theory' from the start page

    6. Bump version number to even minor version in cabal files and code, commit version bump, by running the 'version-change.sh' script as described in its comments. Then merge from 'develop' into 'master' and use "Release" functionality to prepare the release.

  2. Update the Homebrew tap at tamarin-prover/homebrew-tap:

    1. Update the formula to point to the new source tarball.
    2. Build bottles for Mac and Windows, and add them to the Homebrew formula as well.

  3. Update the NixOS repo: @thoughtpolice usually does this (example)

  4. Update the Arch repo: @felixonmars usually does this

Branches

There is only the 'develop' branch to which we are happy to accept your pull requests.

In general, we do ask developers to use their own, external, branches and send pull requests to include. There are some historical branches that we will keep around, but that are definitely stale and will bitrot:

  • feature-user-defined-sorts
  • feature-ac-rewrite-rules

Regression testing for pull requests

Before submitting a pull request, please double check that your changes do not break any of the existing proofs by running the regression test suite. To do this run the following commands in your clone of tamarin-prover:

rm -rf case-studies
make case-studies
diff -r case-studies case-studies-regression

This first removes any existing case-study runs you may have, then runs all the case studies, and finally compares the resulting output to the stored expected output. It is expected that the runtime of the analyses changes every time (but on the order of 1% or so, possibly more depending on the machine you run it on). If that is the only change, everything is fine. If some proof steps get reordered, but the number of steps stays constant that is ok, but should be noted. If that number changes or runtimes change significantly that must be discussed in a pull request.

If you are running the regression on a server you can run multiple case studies in parallel by adding the "-j #" parameter where # is the number of parallel runs. Note that your machine should have 16GB of memory per run, and each run uses 3 threads already. For example:

make -j 6 case-studies

to run 6 case studies in parallel.

Editor support

The directory etc holds files for editor support. For the vim editor, it is desirable to have a separate repository for these files, hence we include this directory as a git-subtree. Here is a tutorial. In summary:

  1. To merge changes from the outside repository into etc here, run the following command, where $branch is the branch you are in now, which is almost always develop.
 git subtree pull --prefix etc https://github.com/tamarin-prover/editors $branch --squash
  1. To contribute changes in etc back to that outside repository, run the following, where $github_user is your github user name, because you need to fork that directory, too.
git subtree push --prefix etc https://github.com/$github_user/editors $branch
  1. FYI: if we ever want to add another subtree, we use:
git subtree add --prefix $local_dir $remote_url $remote_branch --squash