Fix some small problems (#3878)

* `--interim-simplification` problem: When `maxDepth < forceFallback` ,
the proxy was considering a genuine `DepthBound` result as an artefact
caused by the interim simplification, and would try to continue
execution.
* The `cabal.project` file was set up to never profile any `booster` or
`kore-rpc-types` code
* When given a path to a non-existing file as input, `RpcClient`
reported a server connection error and retried (the criterion for
recognising connection errors was to general).

Author: jberthold

booster/tools/booster/Proxy.hs

@@ -292,18 +292,21 @@ respondEither cfg@ProxyConfig{statsVar, boosterState} booster kore req = case re
                 else "Iterating execute request at " <> show currentDepth
         -- calculate depth limit, considering possible forced Kore simplification
         let mbDepthLimit = case (cfg.forceFallback, r.maxDepth) of
-                (Just (Depth forceDepth), Just (Depth maxDepth)) ->
-                    if cDepth + forceDepth < maxDepth
-                        then Just $ Depth forceDepth
-                        else Just $ Depth $ maxDepth - cDepth
+                (Just (Depth forceDepth), Just (Depth maxDepth))
+                    | cDepth + forceDepth < maxDepth ->
+                        cfg.forceFallback
+                    | otherwise ->
+                        Just $ Depth $ maxDepth - cDepth
                 (Just forceDepth, _) -> Just forceDepth
                 (_, Just maxDepth) -> Just $ maxDepth - currentDepth
                 _ -> Nothing
         (bResult, bTime) <- Stats.timed $ booster (Execute r{maxDepth = mbDepthLimit})
         case bResult of
             Right (Execute boosterResult)
                 -- the execution reached the depth bound due to a forced Kore simplification
-                | boosterResult.reason == DepthBound && isJust cfg.forceFallback -> do
+                | DepthBound <- boosterResult.reason
+                , Just forceDepth <- cfg.forceFallback
+                , forceDepth == boosterResult.depth -> do
                     Log.logInfoNS "proxy" . Text.pack $
                         "Forced simplification at " <> show (currentDepth + boosterResult.depth)
                     simplifyResult <- simplifyExecuteState logSettings r._module def boosterResult.state

booster/tools/rpc-client/RpcClient.hs

@@ -192,16 +192,18 @@ retryTCPClient delay retries host port operation
         error $ "retryTCPClient: negative parameters " <> show (delay, retries)
     | retries == 0 = runTCPClient host port operation
     | otherwise =
-        catchJust isNoSuchThing (runTCPClient host port operation) tryAgain
+        catchJust isSocketError (runTCPClient host port operation) tryAgain
   where
-    tryAgain _ = do
-        hPutStrLn stderr $ "[Warning] Could not connect (retrying " <> show retries <> " times)"
+    tryAgain msg = do
+        hPutStrLn stderr $
+            "[Warning] Could not connect: " <> msg <> ". Retrying " <> show retries <> " times"
         sleep delay
         retryTCPClient delay (retries - 1) host port operation
 
-    isNoSuchThing :: IOError -> Maybe ()
-    isNoSuchThing IOError{ioe_type = NoSuchThing} = Just ()
-    isNoSuchThing _other = Nothing
+    isSocketError :: IOError -> Maybe String
+    isSocketError IOError{ioe_type = NoSuchThing, ioe_filename = Nothing, ioe_description} =
+        Just ioe_description
+    isSocketError _other = Nothing
 
 ----------------------------------------
 -- Logging

cabal.project

@@ -6,11 +6,10 @@ packages:
 
 package *
   ghc-options: -fhide-source-paths -haddock
-  profiling-detail: none
 
 package kore
   ghc-options: -Wall -Werror
-  profiling-detail: toplevel-functions
+  profiling-detail: exported-functions
 
 source-repository-package
   type: git