Feature/logging part 1 #448

eviefp · 2019-02-11T16:55:29Z

Reviewer checklist

Test coverage: stack test --coverage
Public API documentation: stack haddock
Style conformance: stylish-haskell

eviefp · 2019-02-14T14:53:33Z

A few things that I did not decide on yet, but we might want to wait until there are more use-cases, although I could be convinced otherwise:

do we want the log functions to take Builder instead of Text?
what do we do about Text.pack (show pattern)? Do we need a Text (or Builder) based Show?
no filtering by scope yet
should scope be a [Text] instead of Text, in LogMessage?
do we want the helper log* functions or should we just say log Debug? I like the idea of importing qualified and using Log.logDebug, in which case they are needed

Dockerfile

ttuegel · 2019-02-15T16:26:30Z

what do we do about Text.pack (show pattern)? Do we need a Text (or Builder) based Show?

I would recommend using the formatting library for this. Summary: you can define reusable, typed format strings and instantiate them to Text, Builder, or anything you can imagine.

should scope be a [Text] instead of Text, in LogMessage?

I would recommend newtype-ing Text (as Scope?) and taking a [Scope].

I like the idea of importing qualified and using Log.logDebug, in which case they are needed

👍, import ALL THE THINGS qualified.

ttuegel · 2019-02-15T16:28:05Z

src/main/haskell/kore/README.md

@@ -18,6 +18,9 @@ To regenerate the golden data for regression tests:
 `stack test --no-keep-going --ta --accept`

 To generate documentation: `stack build --haddock`.
+Note that because of `co-log`'s `typerep-map` dependency (which fails haddock),
+we are currently building with `--no-haddock-deps`. This should be reverted
+once `typerep-map`'s haddock is fixed.


Could you open an issue on our tracker for this, and include a link to the upstream issue?

I have, and they closed it and linked to this bug in stack: commercialhaskell/stack#3989 ; I'll add this to the docs here.

ttuegel · 2019-02-15T16:36:17Z

src/main/haskell/kore/bench/exec/Main.hs

@@ -183,7 +183,7 @@ execBenchmark root kFile definitionFile mainModuleName test =
        -> IO (CommonStepPattern Object)
    execution (verifiedModule, purePattern) =
        SMT.runSMT SMT.defaultConfig
-        $ evalSimplifier
+        $ evalSimplifier mempty


Could we define a value, say emptyLogger = mempty, just to keep this clear?

ttuegel · 2019-02-15T16:40:13Z

src/main/haskell/kore/src/Kore/Logger.hs

+Copyright   : (c) Runtime Verification, 2018
+License     : NCSA
+Maintainer  : vladimir.ciobanu@runtimeverification.com
+Stability   : experimental


For this and all the other new modules, I would be inclined to leave off Stability and Portability. Stability doesn't mean anything, except it makes a tiny note in the upper right-hand corner of the generated documentation that nobody looks at. All of our Portability fields are wrong, anyway: they should say GHC-only, which is what everyone's say, or should say, so it's just noise.

ttuegel · 2019-02-15T16:43:04Z

src/main/haskell/kore/src/Kore/Step/Step.hs

@@ -123,7 +126,9 @@ transitionRule tools substitutionSimplifier simplifier =
            $ stepWithRewriteRule tools substitutionSimplifier config a
        case result of
            Left _ -> pure []
-            Right results -> return $ mapMaybe (patternFromResult proof) results
+            Right results ->
+                Log.withLogScope "transitionRule" $


Can we easily get a source location here? There are already multiple things called transitionRule.

ttuegel · 2019-02-15T16:43:47Z

src/main/haskell/kore/src/SMT.hs

@@ -7,7 +7,7 @@ Maintainer  : thomas.tuegel@runtimeverification.com
 -}

 module SMT
-    ( SMT, getSMT
+    ( SMT (..)


I specifically want to avoid exporting the constructor here:

Suggested change

( SMT (..)

( SMT, getSMT

ttuegel · 2019-02-15T16:46:05Z

src/main/haskell/kore/src/Kore/Logger.hs

+
+-- | This type should not be used directly, but rather should be created and
+-- dispatched through the `log` functions.
+data LogMessage = LogMessage


The field names here do not conform to the style guide.

dwightguth · 2019-02-15T21:49:24Z

While you are at it, can you replace --only-dependencies with --only-snapshot?

eviefp · 2019-02-18T15:56:37Z

@ttuegel I addressed all comments. I actually need a way to go from the Simplifier :: ReaderT (..., MVar Solver) to SMT :: ReaderT (MVar Solver) so I created withSolver'. Is that better than exporting the constructor directly?

Also, I did not add the formatters library yet. I think formatting the log message is not necessarily the main problem here (it might become soon, I agree). I was actually concerned by Show pat being show because (I think?) it does a lot of concats on strings, which are slow...? So I was hoping there was a Show-like class that uses Text -- or better yet, Builder?

ttuegel · 2019-02-18T16:34:26Z

Is that better than exporting the constructor directly?

I think so.

I was actually concerned by Show pat being show because (I think?) it does a lot of concats on strings, which are slow...?

Show is actually based on shows, which returns a String-builder (String -> String), so it's not too bad actually.

So I was hoping there was a Show-like class that uses Text -- or better yet, Builder?

shows is still string-based, but I recommended formatting because you can use the same format declaration to send output to Text, Builder, String, even directly to a Handle. It does not provide a class, but I'm not sure how valuable a class would be for logging: We will always know the concrete type of the thing we are logging (no runtime instance resolution), and it is likely that different types of logging will want to represent the same information in different ways (no single-instance per type).

eviefp · 2019-02-18T21:49:57Z

Ok, now I get it. I think I might add formatting once I get into the meat of adding debugging logs with some real use-cases, along with perhaps some variants of the log functions that take a Format as an argument. Thanks for the review!

virgil-serbanuta · 2019-02-21T12:44:54Z

src/main/haskell/kore/src/Kore/Step/BaseStep.hs

-  = do
-
+  = Log.withLogScope "stepWithRule" $ do
+    Log.logDebug


This handles both function evaluation and rewrite rule application. There is a good chance that this will be extremely verbose for everything except trivial examples (especially since it's using show and not unparse). Also, if you want to reduce verbosity, both for rewriting and for function application, we apply a (sometimes large) number of axioms on the same pattern, so it might be better to log the pattern in this function's caller and to log only the axiom here.

virgil-serbanuta · 2019-02-21T14:49:53Z

src/main/haskell/kore/src/Kore/Logger.hs

@@ -0,0 +1,134 @@
+{-|


You should include documentation about the expected usage patterns.

virgil-serbanuta · 2019-02-21T14:50:00Z

src/main/haskell/kore/src/Kore/Logger.hs

+{-|
+Module      : Kore.Logger
+Description : Logging functions.
+Copyright   : (c) Runtime Verification, 2018


Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Georgy Lukyanov <mail@geo2a.info>

eviefp force-pushed the feature/logging branch 5 times, most recently from 5757fc7 to 6fa1c3f Compare February 14, 2019 14:49

eviefp changed the title ~~Feature/logging (NOT READY)~~ Feature/logging part 1 Feb 14, 2019

eviefp requested a review from ttuegel February 14, 2019 14:49

ttuegel reviewed Feb 14, 2019

View reviewed changes

Dockerfile Outdated Show resolved Hide resolved

Logging part 1

0b9510f

eviefp force-pushed the feature/logging branch from c1bc6bc to 0b9510f Compare February 15, 2019 12:54

ttuegel suggested changes Feb 15, 2019

View reviewed changes

Addressed review comments

32e017d

ttuegel approved these changes Feb 18, 2019

View reviewed changes

eviefp merged commit c5015d2 into runtimeverification:master Feb 18, 2019

eviefp deleted the feature/logging branch February 19, 2019 12:23

virgil-serbanuta reviewed Feb 21, 2019

View reviewed changes

jberthold pushed a commit that referenced this pull request Apr 10, 2024

Update dependency: deps/k_release (#448)

d3b34af

Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Georgy Lukyanov <mail@geo2a.info>

jberthold pushed a commit that referenced this pull request Apr 10, 2024

Update dependency: deps/k_release (#448)

5198882

Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Georgy Lukyanov <mail@geo2a.info>

jberthold pushed a commit that referenced this pull request Apr 10, 2024

Update dependency: deps/k_release (#448)

28db5b2

Co-authored-by: devops <devops@runtimeverification.com> Co-authored-by: Georgy Lukyanov <mail@geo2a.info>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feature/logging part 1 #448

Feature/logging part 1 #448

eviefp commented Feb 11, 2019

eviefp commented Feb 14, 2019

ttuegel commented Feb 15, 2019

ttuegel Feb 15, 2019

eviefp Feb 18, 2019

ttuegel Feb 15, 2019

ttuegel Feb 15, 2019

ttuegel Feb 15, 2019

ttuegel Feb 15, 2019

ttuegel Feb 15, 2019

dwightguth commented Feb 15, 2019

eviefp commented Feb 18, 2019

ttuegel commented Feb 18, 2019

eviefp commented Feb 18, 2019

virgil-serbanuta Feb 21, 2019

virgil-serbanuta Feb 21, 2019

virgil-serbanuta Feb 21, 2019

Feature/logging part 1 #448

Feature/logging part 1 #448

Conversation

eviefp commented Feb 11, 2019

Reviewer checklist

eviefp commented Feb 14, 2019

ttuegel commented Feb 15, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

dwightguth commented Feb 15, 2019

eviefp commented Feb 18, 2019

ttuegel commented Feb 18, 2019

eviefp commented Feb 18, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment