-
Notifications
You must be signed in to change notification settings - Fork 20
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
Switch from ansi-wl-pprint
to the prettyprinter
package.
#178
Conversation
This probably won't work yet because the git submodule references need to be updated for what4 and crucible, and also there are some additional packages that still need to be ported. Also, this draft PR should not be merged until the corresponding what4 and crucible PRs that it builds on have been merged into their respective master branches. |
The CI log also has a very fast failure with an error message, "rejecting: prettyprinter-1.7.0 (constraint from project config TODO requires ==1.6.2)". So we'll have to do something about that. |
I should note that this PR depends on GaloisInc/what4#77 and GaloisInc/crucible#586. |
Regarding CI - the Github Actions use freeze files that fix an older version of prettyprinter |
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 WARNING: Do not merge this commit into master until all of the above PRs are merged into their respective master branches and the submodule references of this commit can be patched up.
pretty (CodePointers s b) = text "code" <+> ppSet (s0 ++ sd) | ||
where s0 = if b then [text "0"] else [] | ||
pretty (BoolConst b) = viaShow b | ||
pretty (FinSet s) = pretty "finset" <+> ppIntegerSet s |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm inclined to just rely on OverloadedStrings
and use "finset"
since it looks like prettyprinter
Doc
implements IsString
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it does implement IsString
. My default approach has been to change text "foo"
to "foo"
if the module already had OverloadedStrings
enabled, and to use pretty "foo"
otherwise. But I can certainly go back and enable OverloadedStrings
in those modules instead.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks. Enabling OverloadedStrings
would be my preference.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have a commit that enables OverloadedStrings
on a separate branch (doc-overloaded-strings
). I just wanted to get CI to pass before I cherry-pick that commit back onto this PR.
Yes, I think just updating the frozen files to the latest versions of packages would be fine. If that ends up being a pain, I'm happy to help out with fixing any errors in a separate PR. |
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 WARNING: Do not merge this commit into master until all of the above PRs are merged into their respective master branches and the submodule references of this commit can be patched up.
b2a1c9f
to
3c16b57
Compare
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 WARNING: Do not merge this commit into master until all of the above PRs are merged into their respective master branches and the submodule references of this commit can be patched up.
3c16b57
to
c4a70ad
Compare
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 WARNING: Do not merge this commit into master until all of the above PRs are merged into their respective master branches and the submodule references of this commit can be patched up.
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 - GaloisInc/elf-edit#20 WARNING: Do not merge this commit into master until all of the above PRs are merged into their respective master branches and the submodule references of this commit can be patched up.
I think I'm pretty close to getting CI to pass. It turns out that I needed to patch yet another submodule: GaloisInc/asl-translator#28 |
b9cf8aa
to
f73730e
Compare
The tests for 8.6.5 and 8.10.2 are now passing! However the test for ghc 8.8.4 is still failing because it looks like I'm also waiting to get GaloisInc/asl-translator#28 merged so that I can point this branch at the submodule hash for the merge commit, and then I can apply the |
This patch relies on the following submodule updates: - GaloisInc/what4#77 - GaloisInc/elf-edit#20 - GaloisInc/crucible#586 - GaloisInc/asl-translator#28 This patch updates the following packages: - macaw-base - macaw-symbolic - macaw-x86 - macaw-x86-symbolic - macaw-aarch32 - macaw-ppc - macaw-semmc - macaw-refinement
f73730e
to
2a620d4
Compare
I think if you recreate the cabal ghc-8.8.4.freeze file with an updated cabal, this will generate correctly now. I just tested this on my machine and it seems to work -- I can create a patch if you'd prefer. |
@joehendrix: The |
Yes. I'm signed off on this. Thanks. |
This commit includes the following submodule PRs: - GaloisInc/what4#77 - GaloisInc/crucible#586 - GaloisInc/macaw#178 - GaloisInc/elf-edit#20
This patch updates the following packages: