prove-everywhere-server (empty) → 0.1

raw patch · 4 files changed

+130/−0 lines, 4 filesdep +aesondep +basedep +bytestringsetup-changed

Dependencies added: aeson, base, bytestring, case-insensitive, http-types, optparse-applicative, parsec, parsers, process, safe, text, time, unordered-containers, wai, warp

Files

LICENSE +30/−0
Setup.hs +2/−0
prove-everywhere-server.cabal +40/−0
src/Main.hs +58/−0

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright (c) 2014, Shohei Yasutake++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Shohei Yasutake nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ prove-everywhere-server.cabal view

@@ -0,0 +1,40 @@+-- Initial prove-everywhere-server.cabal generated by cabal init.  For+-- further documentation, see http://haskell.org/cabal/users-guide/++name:                prove-everywhere-server+version:             0.1+synopsis:            The server for ProveEverywhere+description:         This is the server for ProveEverywhere project.+homepage:            https://github.com/amutake/prove-everywhere+license:             BSD3+license-file:        LICENSE+author:              Shohei Yasutake+maintainer:          amutake.s@gmail.com+-- copyright:+category:            Web+build-type:          Simple+-- extra-source-files:+cabal-version:       >=1.10++executable prove-everywhere-server+  main-is:             Main.hs+  -- other-modules:+  -- other-extensions:+  build-depends:       base == 4.*+                     , warp == 3.0.*+                     , wai == 3.0.*+                     , optparse-applicative == 0.9.*+                     , process == 1.2.*+                     , bytestring == 0.10.*+                     , unordered-containers == 0.2.*+                     , http-types == 0.8.*+                     , aeson == 0.7.*+                     , text == 1.1.*+                     , parsers == 0.11.*+                     , parsec == 3.1.*+                     , safe == 0.3.*+                     , time == 1.4.*+                     , case-insensitive >= 0.2+  hs-source-dirs:      src+  default-language:    Haskell2010+  ghc-options:         -Wall

+ src/Main.hs view

@@ -0,0 +1,58 @@++module Main where++import Control.Exception+import Options.Applicative+import System.Process++import ProveEverywhere.Types+import ProveEverywhere.Server++main :: IO ()+main = do+    config <- execParser opts+    result <- getCoqtopVersion+    case result of+        Nothing -> putStrLn "coqtop not found"+        Just (n, m, p) | (n, m, p) < (8, 4, 0) -> do+            putStrLn $ concat+                [ "coqtop (" ++ show n ++ "." ++ show m ++ "pl" ++ show p ++ ") found\n"+                , "but this server does not support this version"+                ]+        Just (n, m, p) -> do+            putStrLn $ "coqtop (" ++ show n ++ "." ++ show m ++ "pl" ++ show p ++ ") found"+            putStrLn $ "Server started on port " ++ show (configPort config)+            runServer config+  where+    opts = info (helper <*> configParser) $+        fullDesc <> header "prove-everywhere-server - The server for ProveEverywhere"++configParser :: Parser Config+configParser = Config+    <$> option (long "port" <>+                short 'p' <>+                metavar "PORT" <>+                help "Specify port number")+    <*> optional (option+                  (long "number" <>+                   short 'n' <>+                   metavar "NUM_OF_PROCS" <>+                   help "Max number of coqtop processes (default: infinity)"))+    <*> optional (option+                  (long "time" <>+                   short 't' <>+                   metavar "KILL_TIME" <>+                   help "The time to terminate unused coqtop process (unit of time: minute) (default: infinity)"))++getCoqtopVersion :: IO (Maybe (Int, Int, Int)) -- e.g., (8, 4, 4) = 8.4pl4+getCoqtopVersion = handle failure $ do+    v_all <- readProcess "coqtop" ["-v"] ""+    let [n_str, '.', m_str, 'p', 'l', p_str]+            = drop (length "The Coq Proof Assistant, version ")+            . take (length "The Coq Proof Assistant, version *.*pl*")+            $ v_all+    let (n, m, p) = (read [n_str], read [m_str], read [p_str])+    return (Just (n, m, p))+  where+    failure :: IOError -> IO (Maybe (Int, Int, Int))+    failure _ = return Nothing