Skip to content
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.

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

[Trivial] Improve log message. #186

Closed

Conversation

SimonDold
Copy link
Contributor

No description provided.

Copy link
Contributor

@maltehelmert maltehelmert left a comment

Choose a reason for hiding this comment

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

I think this would need more discussion, I don't think the new phrasing is an improvement. It looks like we lose the distinction between inherently incomplete algorithms like EHC and ones that are complete in principle, but can be made incomplete by certain parameter choices.

@maltehelmert
Copy link
Contributor

Also, I see that this would break some scripts, such as a merge-and-shrink parser than Silvan has been using. Not necessarily a big problem, but it means we should warn of this in the release notes. I think I've also seen others parse output for lines like these to figure out what the planner thought of the input.

@maltehelmert
Copy link
Contributor

I talked to some more people offline, and they agree that this will break their parsing and that they consider the current behaviour better than the proposed change, so I'm closing this. We can of course still work on this, but I guess we need some more discussion and it's not a trivial pull request (which would have to be uncontroversial).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants