Build with -Wall

[philderbeast]

WIP: Please don't merge yet.

[philderbeast]

@nikivazou or @ranjitjhala I'd like to attach the "WIP: Don't merge yet" label to this but cannot do this myself. I'm putting this up here so that I could ask about which direction to take with -Wno-name-shadowing.

[philderbeast]

That's funny, I leave this work sit idle for a few weeks and now I can't seem to trigger name-shadowing warnings. If that is truly the case then we can drop the [WIP: Don't Merge Yet] label and this is ready to merge as a fix for #538.

@facundominguez I haven't added stack build --pendantic to the stack CI job but when I do it locally it builds without error.

[facundominguez]

Thanks @philderbeast!

We could merge this promptly by removing the commits from #565 and reverting or addressing the comments in 0628354. Merging promptly is preferable for the large PRs like this, I'd say.

If --pedantic works, it would make sense to add it in the circleci configuration to keep LF warning-free.

[facundominguez]

We could merge this promptly by removing the commits from #565 and reverting or addressing the comments in 0628354.

I actually went ahead and merged all the commits except 0628354 and #565. The merged commits are listed here: #570

Rebasing develop now should allow to shrink the remaining changes to review in this PR.

By the way, nice breakdown of commits. They did help the review.

[ranjitjhala]

Fantastic thank you!!!

…

On Fri, May 20, 2022 at 6:56 PM Facundo Domínguez ***@***.***> wrote: We could merge this promptly by removing the commits from #565 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_565&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=ujC0cyTduhACbiNRhfpA6KIEaPZ2KJMoFrPyJPYOw9k&e=> and reverting or addressing the comments in 0628354 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_commit_0628354b853d1dfcccde9be40717671a3cdce77f&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=zqPPgRBkd7G5RQVFeCXShWZnEr1PWcP1FEgAEGiNNuU&e=> . I actually went ahead and merged all the commits except 0628354 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_commit_0628354b853d1dfcccde9be40717671a3cdce77f&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=zqPPgRBkd7G5RQVFeCXShWZnEr1PWcP1FEgAEGiNNuU&e=> and #565 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_565&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=ujC0cyTduhACbiNRhfpA6KIEaPZ2KJMoFrPyJPYOw9k&e=>. The merged commits are listed here: #570 <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_570&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=BNxYxfBzV9ZzEEO_xBLeH-deTzaOMn77rAbp9npbxJM&e=> Rebasing develop now should allow to shrink the remaining changes to review in this PR. By the way, nice breakdown of commits. They did help the review. — Reply to this email directly, view it on GitHub <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_pull_567-23issuecomment-2D1133499521&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=22gZVZxxO1yONsOdnlQEqUnFdX2i_-T3kAi1qIXQvWs&e=>, or unsubscribe <https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OGLB7PXYJKU3ZFQ3XDVLA7GLANCNFSM5UYKABLQ&d=DwMFaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=enML1KeBKfznTiTKgmXdI7VoclcE5XuqloY5AxW5JS7OCemchsauhIpvd79epo_7&s=5ao2lzAI53lIKUNYq8Lf1L72tIXogiDJbXgBQZyKh9o&e=> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[philderbeast]

If --pedantic works, it would make sense to add it in the circleci configuration to keep LF warning-free.

I found that the stack command cares about the position of --pendantic. It has got to come after test.

> stack --pedantic --no-terminal test -j2 liquid-fixpoint:test --flag liquid-fixpoint:devel
Invalid option `--pedantic'
> stack --no-terminal test --pedantic -j2 liquid-fixpoint:test --flag liquid-fixpoint:devel
...
liquid-fixpoint> Test suite test passed

The --pedantic is not doing any more than we're doing when the --flag devel is set. Not wanting to drive the same nail home with two hammers, I will leave things as they are in the CI scripts.

> stack test --help
...
Available options:
  --pedantic               Turn on -Wall and -Werror

# .cirlceci/config.yml
      - run:
          name: Test
          command: |
            stack --no-terminal test -j2 liquid-fixpoint:test --flag liquid-fixpoint:devel

[philderbeast]

By the way, nice breakdown of commits. They did help the review.

Thanks @facundominguez. I was lucky to find a methodical way to work through the errors.

After doing the rebase, I remember now why I had previously stopped for -Wno-name-shadowing. I used a combination of module pragmas and renamings with primes, x -> x'. The modules with {-# OPTIONS_GHC -Wno-name-shadowing #-} had more name clashes than I felt comfortable with changing in bulk. I added this pragma to 5 modules but then found 30 other modules already had this. Are we OK with setting this warning off in so many modules?

35 results - 35 files

src/Language/Fixpoint/Defunctionalize.hs:
src/Language/Fixpoint/Minimize.hs:
src/Language/Fixpoint/Parse.hs:
src/Language/Fixpoint/Solver.hs:
src/Language/Fixpoint/SortCheck.hs:
src/Language/Fixpoint/Horn/Solve.hs:
src/Language/Fixpoint/Horn/Transformations.hs:
src/Language/Fixpoint/Horn/Types.hs:
src/Language/Fixpoint/Smt/Interface.hs:
src/Language/Fixpoint/Smt/Serialize.hs:
src/Language/Fixpoint/Smt/Theories.hs:
src/Language/Fixpoint/Smt/Types.hs:
src/Language/Fixpoint/Solver/Common.hs:
src/Language/Fixpoint/Solver/EnvironmentReduction.hs:
src/Language/Fixpoint/Solver/Extensionality.hs:
src/Language/Fixpoint/Solver/GradualSolution.hs:
src/Language/Fixpoint/Solver/Instantiate.hs:
src/Language/Fixpoint/Solver/Interpreter.hs:
src/Language/Fixpoint/Solver/PLE.hs:
src/Language/Fixpoint/Solver/Prettify.hs:
src/Language/Fixpoint/Solver/Rewrite.hs:
src/Language/Fixpoint/Solver/Sanitize.hs:
src/Language/Fixpoint/Solver/Simplify.hs:
src/Language/Fixpoint/Solver/Solution.hs:
src/Language/Fixpoint/Solver/Solve.hs:
src/Language/Fixpoint/Solver/TrivialSort.hs:
src/Language/Fixpoint/Solver/UniqifyBinds.hs:
src/Language/Fixpoint/Solver/UniqifyKVars.hs:
src/Language/Fixpoint/Types/Constraints.hs:
src/Language/Fixpoint/Types/Graduals.hs:
src/Language/Fixpoint/Types/Solutions.hs:
src/Language/Fixpoint/Types/Sorts.hs:
src/Language/Fixpoint/Types/Theories.hs:
src/Language/Fixpoint/Types/Visitor.hs:
tests/tasty/Arbitrary.hs:

[facundominguez]

Are we OK with setting this warning off in so many modules?

Looks like a feasible way to breakdown the work to fix the warnings. I'd like to enable the warning in all of the modules eventually.

[philderbeast]

It is a shame that cabal or ghc doesn't give us a summary of warning counts by module. Would help us pick our battles.

[facundominguez]

I merged the newer commits here in #571
I squashed together 90a92b7 and 846d040.

This can be closed if nothing else remains besides #565.

[philderbeast]

This can be closed if nothing else remains besides #565.

I rebased again and yes that seems to be the case, closing now.