tamarin-prover 0.6.0.0 → 0.6.1.0

raw patch · 5 files changed

+10/−6 lines, 5 files

Files

• data/CHANGES +4/−0
• interactive-only-src/Paths_tamarin_prover.hs +1/−1
• src/Main/Console.hs +3/−3
• src/Theory/Proof.hs +1/−1
• tamarin-prover.cabal +1/−1

@@ -1,3 +1,7 @@+* 0.6.1.0+   - fixed: parallel exploration of proof tree was using too much memory+   - fixed: reference to Tutorial.spthy broken in help message+ * 0.6.0.0    - open-sourced the code: https://github.com/tamarin-prover/tamarin-prover 

@@ -12,7 +12,7 @@   version :: Version-version = Version {versionBranch = [0,6,0,0], versionTags = []}+version = Version {versionBranch = [0,6,1,0], versionTags = []} bindir, libdir, datadir, libexecdir :: FilePath  bindir     = "./"

@@ -187,7 +187,7 @@     when (tmIsMainMode tmode) $ do       examplePath <- getDataFileName "examples"       manualPath  <- getDataFileName ("doc" </> "MANUAL")-      let tutorialPath = examplePath </> "stable" </> "Tutorial.spthy"+      let tutorialPath = examplePath </> "Tutorial.spthy"           csf12Path = examplePath </> "csf12" </> "*.spthy"           csf12Cmd  = programName ++ " --prove -Ocase-studies +RTS -N -RTS " ++ csf12Path           csf12Cmd' = programName ++ " interactive +RTS -N -RTS " ++ csf12Path@@ -196,8 +196,8 @@       putStrLn $ unlines         [ separator         , e "For example protocol models see:" [examplePath]-        , e "A tutorial and the user manul are found at" [tutorialPath, manualPath]-        , e "To run all case-studies from our CSF'12 submission, use" [csf12Cmd]+        , e "A tutorial and the user manual are found at" [tutorialPath, manualPath]+        , e "To run all case-studies from our CSF'12 paper, use" [csf12Cmd]         , e "To construct their security proofs interactively, use" [csf12Cmd']         , "Note that the +RTS -N -RTS flags instruct the Haskell runtime system to"         , "use as many cores as your system has. This speeds-up some of the computations."

@@ -493,7 +493,7 @@           | otherwise = case node of               LNode (ProofStep Solved (_,path)) _ -> Solution path               LNode _ cs                          ->-                mconcat $ parMap rseq (findSolved (succ d)) $ M.elems cs+                  foldMap (findSolved (succ d)) cs      extractSolved []         p               = p     extractSolved (label:ps) (LNode pstep m) = case M.lookup label m of

@@ -1,7 +1,7 @@ cabal-version:      >= 1.8 build-type:         Simple name:               tamarin-prover-version:            0.6.0.0+version:            0.6.1.0 license:            GPL license-file:       LICENSE category:           Theorem Provers