Skip to content

Conversation

@ana-pantilie
Copy link
Contributor

Fixes #1956


Reviewer checklist
  • Test coverage: stack test --coverage
  • Public API documentation: stack haddock

@ana-pantilie ana-pantilie marked this pull request as ready for review July 15, 2020 13:04
@ttuegel ttuegel requested a review from andreiburdusa July 15, 2020 14:10
Copy link
Contributor

@andreiburdusa andreiburdusa left a comment

Choose a reason for hiding this comment

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

Looks good. I barely made a couple of observations. I can't find any place to refactor

-> Log.KoreLogOptions
-> Log.KoreLogOptions
generalLogOptionsTransformer
logOptions@(GeneralLogOptions _ _ _ _)
Copy link
Contributor

Choose a reason for hiding this comment

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

Do you need to pattern match here?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Yes, when a new field is added to GeneralLogOptions this will not type check anymore. This way we won't forget to modify this function as well.

Comment on lines +482 to +483
\debug-[type]-equation [eqId1] [eqId2] .. show debugging information for multiple specific equations;\
\ [type] can be 'attempt' or 'apply', or nothing\
Copy link
Contributor

Choose a reason for hiding this comment

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

I don't think anyone will get confused by this explanation, but when [type] is nothing then the remaining command is debug--equation (with two -)

Copy link
Contributor Author

@ana-pantilie ana-pantilie Jul 17, 2020

Choose a reason for hiding this comment

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

Yeah I wrote it like that initially, debug[-type]-equation, and thought it might actually be more confusing for a new user than the explanation above. If you think it's the other way around I can change it back.

Copy link
Contributor

Choose a reason for hiding this comment

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

You're probably right

@ana-pantilie
Copy link
Contributor Author

I can't find any place to refactor

@andreiburdusa Maybe you could look through the repl code and see if anything is implemented awkwardly or if there is any clean up which can be done?

@rv-jenkins rv-jenkins merged commit 0b434df into runtimeverification:master Jul 17, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

kore-repl: debug-equation dynamically

3 participants