Rename withLogger to withLoggerLegacy, withLogger1 to withLogger

geo2a · geo2a · commit 4c137eb916d6 · 2024-04-24T09:59:41.000+02:00
diff --git a/booster/tools/booster/Server.hs b/booster/tools/booster/Server.hs
@@ -76,7 +76,7 @@ import Kore.Log (
     TimestampsSwitch (TimestampsDisable),
     defaultKoreLogOptions,
     swappableLogger,
-    withLogger1,
+    withLogger,
  )
 import Kore.Log qualified as Log
 import Kore.Log.DebugSolver qualified as Log
@@ -152,7 +152,7 @@ main = do
                         pure (const False)
                     Just es -> pure (`elem` es)
 
-            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
+            liftIO $ void $ withBugReport (ExeName "kore-rpc-booster") BugReportOnError $ \_reportDirectory -> withMDLib llvmLibraryFile $ \mdl -> do
                 let coLogLevel = fromMaybe Log.Info $ toSeverity logLevel
                     koreLogOptions =
                         (defaultKoreLogOptions (ExeName "") startTime)
@@ -183,7 +183,7 @@ main = do
                             }
                     srvSettings = serverSettings port "*"
 
-                withLogger1 reportDirectory koreLogOptions $ \actualLogAction -> do
+                withLogger koreLogOptions $ \actualLogAction -> do
                     mLlvmLibrary <- maybe (pure Nothing) (fmap Just . mkAPI) mdl
                     definitionsWithCeilSummaries <-
                         liftIO $
diff --git a/dev-tools/kore-rpc-dev/Server.hs b/dev-tools/kore-rpc-dev/Server.hs
@@ -66,7 +66,7 @@ import Kore.Log (
     TimestampsSwitch (TimestampsDisable),
     defaultKoreLogOptions,
     swappableLogger,
-    withLogger1,
+    withLogger,
  )
 import Kore.Log qualified
 import Kore.Log qualified as Log
@@ -191,8 +191,8 @@ main = do
                     }
             srvSettings = serverSettings port "*"
 
-        liftIO $ void $ withBugReport (ExeName "kore-rpc-dev") BugReportOnError $ \reportDirectory ->
-            withLogger1 reportDirectory koreLogOptions $ \actualLogAction -> do
+        liftIO $ void $ withBugReport (ExeName "kore-rpc-dev") BugReportOnError $ \_reportDirectory ->
+            withLogger koreLogOptions $ \actualLogAction -> do
                 mvarLogAction <- newMVar actualLogAction
                 let logAction = swappableLogger mvarLogAction
                 kore@KoreServer{runSMT} <-
diff --git a/kore/app/repl/Main.hs b/kore/app/repl/Main.hs
@@ -26,7 +26,7 @@ import Kore.Log (
     logEntry,
     runLoggerT,
     swappableLogger,
-    withLogger,
+    withLoggerLegacy,
  )
 import Kore.Log.ErrorException (
     errorException,
@@ -230,7 +230,7 @@ mainWithOptions :: LocalOptions KoreReplOptions -> IO ()
 mainWithOptions LocalOptions{execOptions} = do
     exitCode <-
         withBugReport Main.exeName bugReportOption $ \tempDirectory ->
-            withLogger tempDirectory koreLogOptions $ \actualLogAction -> do
+            withLoggerLegacy tempDirectory koreLogOptions $ \actualLogAction -> do
                 mvarLogAction <- newMVar actualLogAction
                 let swapLogAction = swappableLogger mvarLogAction
                 flip runLoggerT swapLogAction $
diff --git a/kore/src/Kore/Log.hs b/kore/src/Kore/Log.hs
@@ -8,11 +8,12 @@ module Kore.Log (
     koreLogFilters,
     koreLogTransformer,
     withLogger,
-    withLogger1,
+    withLoggerLegacy,
     emptyLogger,
     stderrLogger,
     swappableLogger,
     makeKoreLogger,
+    makeKoreLoggerLegacy,
     Colog.logTextStderr,
     Colog.logTextHandle,
     runKoreLog,
@@ -90,43 +91,41 @@ data WithTimestamp = WithTimestamp SomeEntry TimeSpec
 {- | Generates an appropriate logger for the given 'KoreLogOptions'. It uses
  the CPS style because some outputters require cleanup (e.g. files).
 -}
-withLogger ::
+withLoggerLegacy ::
     FilePath ->
     KoreLogOptions ->
     (LogAction IO SomeEntry -> IO a) ->
     IO a
-withLogger reportDirectory koreLogOptions = runContT $ do
-    mainLogger <- ContT $ withMainLogger reportDirectory koreLogOptions
+withLoggerLegacy reportDirectory koreLogOptions = runContT $ do
+    mainLogger <- ContT $ withMainLoggerLegacy reportDirectory koreLogOptions
     let KoreLogOptions{exeName, debugSolverOptions} = koreLogOptions
     smtSolverLogger <- ContT $ withSmtSolverLogger exeName debugSolverOptions
     traceLogger <- ContT $ withRewriteTraceLogger koreLogOptions
     let KoreLogOptions{logSQLiteOptions} = koreLogOptions
     logSQLite <- ContT $ withLogSQLite logSQLiteOptions
     return $ mainLogger <> smtSolverLogger <> traceLogger <> logSQLite
 
-{- | Generates an appropriate logger for the given 'KoreLogOptions'. It uses
- the CPS style because some outputters require cleanup (e.g. files).
+{- | Like 'withLoggerLegacy', but modified for the needs for 'kore-rpc-booster':
+  * optional JSON logging
+  * no bug report
+  * no SQL logging
 -}
-withLogger1 ::
-    FilePath ->
+withLogger ::
     KoreLogOptions ->
     (LogAction IO SomeEntry -> IO a) ->
     IO a
-withLogger1 reportDirectory koreLogOptions = runContT $ do
-    mainLogger <- ContT $ withMainLogger1 reportDirectory koreLogOptions
+withLogger koreLogOptions = runContT $ do
+    mainLogger <- ContT $ withMainLogger koreLogOptions
     let KoreLogOptions{exeName, debugSolverOptions} = koreLogOptions
     smtSolverLogger <- ContT $ withSmtSolverLogger exeName debugSolverOptions
-    traceLogger <- ContT $ withRewriteTraceLogger koreLogOptions
-    let KoreLogOptions{logSQLiteOptions} = koreLogOptions
-    logSQLite <- ContT $ withLogSQLite logSQLiteOptions
-    return $ mainLogger <> smtSolverLogger <> traceLogger <> logSQLite
+    return $ mainLogger <> smtSolverLogger
 
-withMainLogger ::
+withMainLoggerLegacy ::
     FilePath ->
     KoreLogOptions ->
     (LogAction IO SomeEntry -> IO a) ->
     IO a
-withMainLogger reportDirectory koreLogOptions = runContT $ do
+withMainLoggerLegacy reportDirectory koreLogOptions = runContT $ do
     let KoreLogOptions{exeName, startTime} = koreLogOptions
         bugReportLogFile = reportDirectory </> getExeName exeName <.> "log"
     bugReportLogAction <- ContT $ Colog.withLogTextFile bugReportLogFile
@@ -140,17 +139,16 @@ withMainLogger reportDirectory koreLogOptions = runContT $ do
         KoreLogOptions{logFormat} = koreLogOptions
         logAction =
             userLogAction <> bugReportLogAction
-                & makeKoreLogger exeName startTime timestampsSwitch logFormat
+                & makeKoreLoggerLegacy exeName startTime timestampsSwitch logFormat
                 & koreLogFilters koreLogOptions
                 & koreLogTransformer koreLogOptions
     pure logAction
 
-withMainLogger1 ::
-    FilePath ->
+withMainLogger ::
     KoreLogOptions ->
     (LogAction IO SomeEntry -> IO a) ->
     IO a
-withMainLogger1 _reportDirectory koreLogOptions = runContT $ do
+withMainLogger koreLogOptions = runContT $ do
     let KoreLogOptions{exeName} = koreLogOptions
     (entryFilter, standardLogAction, jsonLogAction) <-
         case logType koreLogOptions of
@@ -161,10 +159,12 @@ withMainLogger1 _reportDirectory koreLogOptions = runContT $ do
                     , jsonLogAction ldata
                     )
             LogStdErr -> pure (const False, Colog.logTextStderr, Colog.logTextStderr)
-            LogFileText _logFile -> pure (const False, Colog.logTextStderr, Colog.logTextStderr) -- Not sure what to put here
+            LogFileText logFile -> do
+                action <- lift (checkLogFilePath exeName "" logFile) >>= ContT . Colog.withLogTextFile
+                pure (const False, action, action)
     let KoreLogOptions{logFormat} = koreLogOptions
         logAction =
-            makeKoreLogger1
+            makeKoreLogger
                 exeName
                 logFormat
                 entryFilter
@@ -288,56 +288,51 @@ filterSeverity level entry =
 -- | Run a 'LoggerT' with the given options.
 runKoreLog :: FilePath -> KoreLogOptions -> LoggerT IO a -> IO a
 runKoreLog reportDirectory options loggerT =
-    withLogger reportDirectory options $ runLoggerT loggerT
+    withLoggerLegacy reportDirectory options $ runLoggerT loggerT
 
 -- | Run a 'LoggerT' with the given options, using `swappableLogger` to make it thread safe.
 runKoreLogThreadSafe :: FilePath -> KoreLogOptions -> LoggerT IO a -> IO a
 runKoreLogThreadSafe reportDirectory options loggerT =
-    withLogger reportDirectory options $ \actualLogAction -> do
+    withLoggerLegacy reportDirectory options $ \actualLogAction -> do
         mvarLogAction <- newMVar actualLogAction
         let swapLogAction = swappableLogger mvarLogAction
         runLoggerT loggerT swapLogAction
 
-{- | The logger that redirects some of the items to a file
-TODO: needs better description
+{- | The default Kore logger used by the legacy backend.
+
+Creates a kore logger which:
+  * adds timestamps
+  * formats messages: "<exe-name>: [<timestamp>] <severity> (<entry-type>): <message>"
 -}
-makeKoreLogger1 ::
+makeKoreLoggerLegacy ::
     forall io.
     MonadIO io =>
     ExeName ->
+    TimeSpec ->
+    TimestampsSwitch ->
     KoreLogFormat ->
-    (Text -> Bool) ->
-    LogAction io Text ->
     LogAction io Text ->
     LogAction io SomeEntry
-makeKoreLogger1 exeName koreLogFormat entryFilter prettyLogAction jsonLogAction =
-    let actionForJsonLogs =
-            jsonLogAction
-                & Colog.cmap renderJson
-                & Colog.cfilter (entryFilter . entryTypeText)
-        actionForPrettyLogs =
-            prettyLogAction
-                & Colog.cmap render
-                & Colog.cfilter (not . entryFilter . entryTypeText)
-     in actionForJsonLogs <> actionForPrettyLogs
+makeKoreLoggerLegacy exeName startTime timestampSwitch koreLogFormat logActionText =
+    logActionText
+        & contramap render
+        & Colog.cmapM withTimestamp
   where
-    renderJson :: SomeEntry -> Text
-    renderJson (SomeEntry _context actualEntry) =
-        LazyText.toStrict . JSON.encodeToLazyText . addOriginField $ oneLineJson actualEntry
-      where
-        addOriginField :: JSON.Value -> JSON.Value
-        addOriginField = \case
-            (JSON.Object xs) -> JSON.Object $ JSON.insert (JSON.fromText "origin") (JSON.toJSON KoreRpc) xs
-            xs -> xs
-
-    render :: SomeEntry -> Text
-    render entry =
-        prettyActualEntry entry
+    render :: WithTimestamp -> Text
+    render (WithTimestamp entry entryTime) =
+        prettyActualEntry timestamp entry
             & Pretty.layoutPretty Pretty.defaultLayoutOptions
             & Pretty.renderText
-
+      where
+        timestamp =
+            case timestampSwitch of
+                TimestampsDisable -> Nothing
+                TimestampsEnable ->
+                    Just . Pretty.brackets . Pretty.pretty $
+                        toMicroSecs (diffTimeSpec startTime entryTime)
+        toMicroSecs = (`div` 1000) . toNanoSecs
     exeName' = Pretty.pretty exeName <> Pretty.colon
-    prettyActualEntry entry@(SomeEntry entryContext actualEntry)
+    prettyActualEntry timestamp entry@(SomeEntry entryContext actualEntry)
         | OneLine <- koreLogFormat =
             Pretty.hsep [header, oneLineDoc actualEntry]
         | otherwise =
@@ -350,6 +345,7 @@ makeKoreLogger1 exeName koreLogFormat entryFilter prettyLogAction jsonLogAction
         header =
             (Pretty.hsep . catMaybes)
                 [ Just exeName'
+                , timestamp
                 , Just severity'
                 , Just (Pretty.parens $ type' entry)
                 ]
@@ -378,41 +374,44 @@ makeKoreLogger1 exeName koreLogFormat entryFilter prettyLogAction jsonLogAction
 
     indent = Pretty.indent 4
 
-{- | The default Kore logger.
-
-Creates a kore logger which:
-  * adds timestamps
-  * formats messages: "<exe-name>: [<timestamp>] <severity> (<entry-type>): <message>"
--}
+-- | The logger used by 'kore-rpc-booster' and 'kore-rpc-dev'
 makeKoreLogger ::
     forall io.
     MonadIO io =>
     ExeName ->
-    TimeSpec ->
-    TimestampsSwitch ->
     KoreLogFormat ->
+    (Text -> Bool) ->
+    LogAction io Text ->
     LogAction io Text ->
     LogAction io SomeEntry
-makeKoreLogger exeName startTime timestampSwitch koreLogFormat logActionText =
-    logActionText
-        & contramap render
-        & Colog.cmapM withTimestamp
+makeKoreLogger exeName koreLogFormat entryFilter prettyLogAction jsonLogAction =
+    let actionForJsonLogs =
+            jsonLogAction
+                & Colog.cmap renderJson
+                & Colog.cfilter (entryFilter . entryTypeText)
+        actionForPrettyLogs =
+            prettyLogAction
+                & Colog.cmap render
+                & Colog.cfilter (not . entryFilter . entryTypeText)
+     in actionForJsonLogs <> actionForPrettyLogs
   where
-    render :: WithTimestamp -> Text
-    render (WithTimestamp entry entryTime) =
-        prettyActualEntry timestamp entry
+    renderJson :: SomeEntry -> Text
+    renderJson (SomeEntry _context actualEntry) =
+        LazyText.toStrict . JSON.encodeToLazyText . addOriginField $ oneLineJson actualEntry
+      where
+        addOriginField :: JSON.Value -> JSON.Value
+        addOriginField = \case
+            (JSON.Object xs) -> JSON.Object $ JSON.insert (JSON.fromText "origin") (JSON.toJSON KoreRpc) xs
+            xs -> xs
+
+    render :: SomeEntry -> Text
+    render entry =
+        prettyActualEntry entry
             & Pretty.layoutPretty Pretty.defaultLayoutOptions
             & Pretty.renderText
-      where
-        timestamp =
-            case timestampSwitch of
-                TimestampsDisable -> Nothing
-                TimestampsEnable ->
-                    Just . Pretty.brackets . Pretty.pretty $
-                        toMicroSecs (diffTimeSpec startTime entryTime)
-        toMicroSecs = (`div` 1000) . toNanoSecs
+
     exeName' = Pretty.pretty exeName <> Pretty.colon
-    prettyActualEntry timestamp entry@(SomeEntry entryContext actualEntry)
+    prettyActualEntry entry@(SomeEntry entryContext actualEntry)
         | OneLine <- koreLogFormat =
             Pretty.hsep [header, oneLineDoc actualEntry]
         | otherwise =
@@ -425,7 +424,6 @@ makeKoreLogger exeName startTime timestampSwitch koreLogFormat logActionText =
         header =
             (Pretty.hsep . catMaybes)
                 [ Just exeName'
-                , timestamp
                 , Just severity'
                 , Just (Pretty.parens $ type' entry)
                 ]
@@ -471,7 +469,7 @@ stderrLogger ::
     KoreLogFormat ->
     LogAction io SomeEntry
 stderrLogger exeName startTime timestampsSwitch logFormat =
-    makeKoreLogger exeName startTime timestampsSwitch logFormat Colog.logTextStderr
+    makeKoreLoggerLegacy exeName startTime timestampsSwitch logFormat Colog.logTextStderr
 
 {- | @swappableLogger@ delegates to the logger contained in the 'MVar'.
 
diff --git a/kore/src/Kore/Repl/State.hs b/kore/src/Kore/Repl/State.hs
@@ -526,7 +526,7 @@ liftSimplifierWithLogger mLogger simplifier = do
     (textLogger, maybeHandle) <- logTypeToLogger logType
     let logger =
             Log.koreLogFilters koreLogOptions $
-                Log.makeKoreLogger
+                Log.makeKoreLoggerLegacy
                     exeName
                     startTime
                     timestampsSwitch
