Prettyprint/produce proof tree #43
Open
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
nishantjr
force-pushed
the
detailed-proofs
branch
from
537952b to
b80c422
Compare
nishantjr
force-pushed
the
detailed-proofs
branch
2 times, most recently
from
507cb90 to
9a6889d
Compare
nishantjr
changed the title
nishantjr
changed the title
|
I have run the smoke test and things work. Please run any other tests you are concerned about |
lucaspena
reviewed
Apr 20, 2020
Thats an idea. Right now the tests are timing out. It looks like Xiaohong is right, and there is a performance issue. I've pushed a PR that reduces changes the set of goals to a list, and only considers the first goal as active. I'll need to re-implement |
nishantjr
force-pushed
the
detailed-proofs
branch
2 times, most recently
from
b853c84 to
2491890
Compare
Since we are not removing subgoals unless they fail this is no longer necessary
… a single uncomposed strategy
nishantjr
force-pushed
the
detailed-proofs
branch
from
2491890 to
e1dd33a
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds a script called
lib/render-proof-treethat pretty prints the proof tree and the current/selected goal.It also changes sequential composition to occur within a subgoal. Performance doesn't seem to have been affected much, but I have not tested that extensively.