Merge branch 'master' into 4043-filter-smt-lemmas-for-predicate-checks

runtimeverification · Oct 1, 2024 · 9e3c834 · 9e3c834
2 parents 4e78fe8 + 4e95286
commit 9e3c834
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/booster/library/Booster/CLOptions.hs b/booster/library/Booster/CLOptions.hs
@@ -66,7 +66,7 @@ data LogFormat
     = Standard
     | OneLine
     | Json
-    deriving (Eq)
+    deriving (Eq, Enum)
 
 instance Show LogFormat where
     show = \case
@@ -155,7 +155,10 @@ parseLogOptions =
             ( metavar "LOGFORMAT"
                 <> value OneLine
                 <> long "log-format"
-                <> help "Format to output logs in"
+                <> help
+                    ( "Format to output logs in. Available formats: "
+                        <> intercalate ", " (map show $ enumFrom (toEnum @LogFormat 0))
+                    )
                 <> showDefault
             )
         <*> many

diff --git a/deps/k_release b/deps/k_release
@@ -1 +1 @@
-7.1.149
+7.1.151
diff --git a/dev-tools/booster-dev/Server.hs b/dev-tools/booster-dev/Server.hs
@@ -143,7 +143,7 @@ runServer port definitions defaultMain mLlvmLibrary rewriteOpts logFile mSMTOpti
         withFastLogger mTimeCache logFile $ \stderrLogger mFileLogger -> do
             let boosterContextLogger = case logFormat of
                     Json -> Booster.Log.jsonLogger $ fromMaybe stderrLogger mFileLogger
-                    _ -> Booster.Log.textLogger stderrLogger
+                    _ -> Booster.Log.textLogger $ fromMaybe stderrLogger mFileLogger
                 filteredBoosterContextLogger =
                     flip Booster.Log.filterLogger boosterContextLogger $ \(Booster.Log.LogMessage (Booster.Flag alwaysDisplay) ctxts _) ->
                         alwaysDisplay
@@ -163,10 +163,12 @@ runServer port definitions defaultMain mLlvmLibrary rewriteOpts logFile mSMTOpti
                         }
             jsonRpcServer
                 (serverSettings port "*")
-                ( const $
+                ( \rawReq req ->
                     flip runReaderT (filteredBoosterContextLogger, toModifiersRep prettyPrintOptions)
                         . Booster.Log.unLoggerT
+                        . Booster.Log.withContextFor (getReqId rawReq)
                         . Booster.Log.withContext Booster.Log.CtxBooster
                         . respond stateVar
+                        $ req
                 )
                 [handleSmtError, RpcError.handleErrorCall, RpcError.handleSomeException]