Skip to content

Fix some small problems #3878

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
May 20, 2024
Merged

Fix some small problems #3878

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
02afb19
fix interim-simplification for max-depth < forceFallback
jberthold May 20, 2024
22ab0e0
fix cabal configuration for profiling
jberthold May 20, 2024
668befd
Do not confuse missing files with server connection error
jberthold May 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 8 additions & 5 deletions booster/tools/booster/Proxy.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Once cDepth was reaching maxDepth (see above, when maxDepth < forceDepth) we were starting to make requests with max-depth: 0 and looping.

| 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
Expand Down
14 changes: 8 additions & 6 deletions booster/tools/rpc-client/RpcClient.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 1 addition & 2 deletions cabal.project
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Loading