Merge pull request #647 from conjure-cp/stats

stats.json

conjure-cp.cabal

@@ -251,6 +251,7 @@ Library
                      , Conjure.UI.ParameterGenerator
                      , Conjure.UI.NormaliseQuantified
                      , Conjure.UI.ErrorDisplay
+                     , Conjure.UI.SolveStats
 
                      , Conjure.LSP.LanguageServer
                      , Conjure.LSP.Documentation

src/Conjure/UI/MainHelper.hs

@@ -19,7 +19,7 @@ import Conjure.UI.Split ( outputSplittedModels, removeUnusedDecls )
 import Conjure.UI.VarSymBreaking ( outputVarSymBreaking )
 import Conjure.UI.ParameterGenerator ( parameterGenerator )
 import Conjure.UI.NormaliseQuantified ( normaliseQuantifiedVariables )
-
+import Conjure.UI.SolveStats ( mkSolveStats )
 
 import Conjure.Language.Name ( Name(..) )
 import Conjure.Language.Definition ( Model(..), ModelInfo(..), Statement(..), Declaration(..), FindOrGiven(..) )
@@ -52,9 +52,6 @@ import qualified Data.HashMap.Strict as M       -- unordered-containers
 -- filepath
 import System.FilePath ( splitFileName, takeBaseName, (<.>) )
 
--- system-filepath
--- import qualified Filesystem.Path as Sys ( FilePath )
-
 -- directory
 import System.Directory ( copyFile, findExecutable )
 
@@ -1096,21 +1093,30 @@ srStdoutHandler _ _ _ _ = bug "srStdoutHandler"
 srCleanUp :: FilePath -> UI -> Text -> [sols] -> Sh (Either [Doc] [sols])
 srCleanUp outBase Solve{..} stdoutSR solutions = do
 
+    let mkFilename ext = outputDirectory </> outBase ++ ext
+
     -- closing the array in the all solutions json file
     case outputFormat of
         JSON -> case solutionsInOneFile of
             False -> return ()
             True -> do
-                let mkFilename ext = outputDirectory </> outBase ++ ext
                 let filenameEssenceSolJSON = mkFilename ".solutions.json"
                 case solutions of
                     [] -> liftIO $ writeFile  filenameEssenceSolJSON "[]\n"
                     _  -> liftIO $ appendFile filenameEssenceSolJSON "]\n"
         _ -> return ()
 
+    let srInfoFilename = mkFilename ".eprime-info"
+    let statsFilename = mkFilename ".stats.json"
+    srInfoContent <- liftIO $ readFileIfExists srInfoFilename
+
     stderrSR   <- lastStderr
     exitCodeSR <- lastExitCode
     let combinedSR = T.unlines [stdoutSR, stderrSR]
+
+    let stats = mkSolveStats (fromMaybe "" srInfoContent) combinedSR
+    liftIO $ writeFile statsFilename (render lineWidth $ toJSON stats)
+
     if  | T.isInfixOf "Savile Row timed out." combinedSR ->
             return (Left ["Savile Row timed out."])
         | T.isInfixOf "where false" combinedSR ->

src/Conjure/UI/SolveStats.hs

@@ -0,0 +1,45 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE RecordWildCards #-}
+
+module Conjure.UI.SolveStats (mkSolveStats, SolveStats (..), SolveStatus (..)) where
+
+import Conjure.Prelude
+import Data.HashMap.Strict qualified as M -- unordered-containers
+import Data.Text qualified as T (isInfixOf) -- text
+
+data SolveStats = SolveStats {status :: SolveStatus, totalTime :: Maybe Double, savilerowInfo :: M.HashMap String String}
+  deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+instance Hashable SolveStats
+
+instance ToJSON SolveStats where toJSON = genericToJSON jsonOptions
+
+instance FromJSON SolveStats where parseJSON = genericParseJSON jsonOptions
+
+data SolveStatus = OK | TimeOut | MemOut
+  deriving (Eq, Ord, Show, Data, Typeable, Generic)
+
+instance Hashable SolveStatus
+
+instance ToJSON SolveStatus where toJSON = genericToJSON jsonOptions
+
+instance FromJSON SolveStatus where parseJSON = genericParseJSON jsonOptions
+
+mkSolveStats :: String -> Text -> SolveStats
+mkSolveStats raw stdout =
+  let info = M.fromList [(k, v) | [k, v] <- map (splitOn ":") (lines raw)]
+      status
+        | info M.! "SavileRowTimeOut" == "1" = TimeOut
+        | info M.! "SavileRowClauseOut" == "1" = TimeOut
+        | info M.! "SolverTimeOut" == "1" = TimeOut
+        | T.isInfixOf "Savile Row timed out." stdout = TimeOut
+        | T.isInfixOf "java.lang.OutOfMemoryError" stdout = MemOut
+        | otherwise = OK
+      totalTime
+        | Just srTotalTime <- readMay $ info M.! "SavileRowTotalTime",
+          Just solverTotalTime <- readMay $ info M.! "SolverTotalTime" =
+            Just (srTotalTime + solverTotalTime)
+        | otherwise = Nothing
+      savilerowInfo = info
+   in SolveStats {..}