Add an evaluation-only version of cryptol-remote-api

This version requires the file that's in scope to be provided as an
argument. It loads that file on startup, and then provides only
commands that don't change that module context. This means that it can
be used in a stateless load-balancing situation.

cryptol-remote-api/cryptol-eval-server/Main.hs

@@ -0,0 +1,89 @@
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Main (main) where
+
+import qualified Data.Aeson as JSON
+import Control.Lens hiding (argument)
+import Data.Text (Text)
+import System.Environment (lookupEnv)
+import System.Exit (exitFailure)
+import System.FilePath (splitSearchPath)
+import System.IO (hPutStrLn, stderr)
+import Options.Applicative
+
+import Cryptol.Eval (EvalOpts(..), defaultPPOpts)
+import Cryptol.ModuleSystem (ModuleInput(..), loadModuleByPath, loadModuleByName)
+import Cryptol.ModuleSystem.Monad (runModuleM, setFocusedModule)
+import Cryptol.TypeCheck.AST (mName)
+import Cryptol.Utils.Ident (preludeName)
+import Cryptol.Utils.Logger (quietLogger)
+
+import Argo
+import Argo.DefaultMain
+
+
+import CryptolServer
+import CryptolServer.EvalExpr
+import CryptolServer.FocusedModule
+import CryptolServer.Names
+import CryptolServer.TypeCheck
+
+main :: IO ()
+main = customMain initMod initMod initMod description buildApp
+  where
+    buildApp opts =
+      mkApp (startingState (userOptions opts)) cryptolEvalMethods
+
+    startingState (StartingFile file) reader =
+      do paths <- getSearchPaths
+         initSt <- setSearchPath paths <$> initialState
+         let menv = view moduleEnv initSt
+         let minp = ModuleInput False evOpts reader menv
+         let die =
+               \err ->
+                 do hPutStrLn stderr $ "Failed to load " ++ maybe "Cryptol prelude" ("file " ++) file ++ ":\n" ++ show err
+                    exitFailure
+         menv' <-
+           do (res, _warnings) <- maybe (loadModuleByName preludeName) loadModuleByPath file minp
+              -- NB Warnings suppressed when running server
+              case res of
+                Left err -> die err
+                Right (m, menv') ->
+                  do res' <- fst <$> runModuleM minp { minpModuleEnv = menv' } (setFocusedModule (mName (snd m)))
+                     case res' of
+                       Left err -> die err
+                       Right (_, menv'') -> pure menv''
+         return $ set moduleEnv menv' initSt
+
+    evOpts =
+      EvalOpts { evalLogger = quietLogger
+               , evalPPOpts = defaultPPOpts
+               }
+
+description :: String
+description =
+  "An RPC server for Cryptol that supports only type checking and evaluation of Cryptol code."
+
+getSearchPaths :: IO [FilePath]
+getSearchPaths =
+  maybe [] splitSearchPath <$> lookupEnv "CRYPTOLPATH"
+
+newtype StartingFile =
+  StartingFile (Maybe FilePath)
+
+initMod :: Parser StartingFile
+initMod = StartingFile <$> filename
+  where
+    filename =
+      optional $ argument str $
+      metavar "FILENAME" <>
+      help "Cryptol file to load on startup"
+
+cryptolEvalMethods :: [(Text, MethodType, JSON.Value -> Method ServerState JSON.Value)]
+cryptolEvalMethods =
+  [ ("focused module",      Query,   method focusedModule)
+  , ("evaluate expression", Query,   method evalExpression)
+  , ("visible names",       Query,   method visibleNames)
+  , ("check type",          Query,   method checkType)
+  ]

cryptol-remote-api/cryptol-eval-server/README.txt

@@ -0,0 +1,6 @@
+This server provides a subset of the methods that are available in
+cryptol-remote-api. It's reason for being is that it does not provide
+any commands that allow modifications to the server state (the
+provided Cryptol code must be specified in a command-line
+argument). This means that it can be used in situations with load
+balancing between multiple instances.

cryptol-remote-api/cryptol-remote-api.cabal

@@ -71,6 +71,19 @@ executable cryptol-remote-api
     cryptol-remote-api,
     sbv < 8.10
 
+executable cryptol-eval-server
+  import:              deps, warnings
+  main-is:             Main.hs
+  hs-source-dirs:      cryptol-eval-server
+  ghc-options:
+    -threaded
+
+  build-depends:
+    cryptol-remote-api,
+    optparse-applicative,
+    sbv < 8.10
+
+
 test-suite test-cryptol-remote-api
   import:              deps, warnings
   type:                exitcode-stdio-1.0

cryptol-remote-api/test-scripts/eval-server-test.py

@@ -0,0 +1,41 @@
+import os
+from pathlib import Path
+import subprocess
+import time
+
+import argo.connection as argo
+import cryptol
+
+dir_path = Path(os.path.dirname(os.path.realpath(__file__)))
+
+cryptol_path = dir_path.joinpath('test-data')
+
+
+env = os.environ.copy()
+env['CRYPTOLPATH'] = cryptol_path
+
+p = subprocess.Popen(
+    ["cabal", "v2-exec", "cryptol-eval-server", "--verbose=0", "--", "http", "/", "--port", "50005", str(cryptol_path.joinpath("M.cry"))],
+    stdout=subprocess.DEVNULL,
+    stdin=subprocess.DEVNULL,
+    stderr=subprocess.DEVNULL,
+    start_new_session=True,
+    env=env)
+time.sleep(5)
+assert(p is not None)
+assert(p.poll() is None)
+
+c = argo.ServerConnection(argo.HttpProcess('http://localhost:50005/'))
+
+
+mid = c.send_message("evaluate expression", {"expression": {"expression":"call","function":"f","arguments":[{"expression":"bits","encoding":"hex","data":"ff","width":8}]}, "state": None})
+reply = c.wait_for_reply_to(mid)
+assert('result' in reply)
+assert('answer' in reply['result'])
+assert('value' in reply['result']['answer'])
+assert(reply['result']['answer']['value'] ==
+       {'data': [{'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'},
+                 {'data': 'ff', 'width': 8, 'expression': 'bits', 'encoding': 'hex'}],
+        'expression': 'sequence'})
+
+os.killpg(os.getpgid(p.pid), signal.SIGKILL)

deps/argo

@@ -1 +1 @@
-Subproject commit ff0eb8a7767abed85bb0ee929a60ce189076be79
+Subproject commit 7d2c2085021825668412c62d31534568447d0fdc