search

ucsd-progsys / liquid-fixpoint

Horn Clause Constraint Solving for Liquid Types
BSD 3-Clause "New" or "Revised" License
132 stars 60 forks source link

Build with -Werror -Wall #538

Open facundominguez opened 2 years ago

facundominguez commented 2 years ago

I've tripped a couple of times over unintended name captures. It would be for the better to enable -Werror -Wall when building all modules.

stack has the --pedantic flag to turn on these.

These flags are usually specified for development builds or in CI, but not when building liquid-fixpoint as a dependency (this would interfere with the user ability to install it).

liquid-fixpoint.cabal already has -Werror behind a devel flag. For builds with cabal-install this could be augmented to use -Wall as well.

ranjitjhala commented 2 years ago

Excellent idea!!

On Thu, Apr 7, 2022 at 2:39 PM Facundo Domínguez @.***> wrote:

I've been tripped a couple of times by unintended name captures. It would be for the better to enable -Werror -Wall when building all modules.

stack has the --pedantic flag to turn on these.

These flags are usually specified for development builds or in CI, but not when building liquid-fixpoint as a dependency (this would interfere with the user ability to install it).

liquid-fixpoint.cabal already has -Werror behind a devel flag. For builds with cabal-install this could be augmented to use -Wall as well.

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_538&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=skgib_A8Yh0zqVhY623O5SuKAvIwMBVtg733TbGJUGPVtl-qJ9PBYhW_MJKaTP5Q&s=8ALnXuXkQ6rwqLbolQV990NHaRml6MAgvLNhN-bZvHA&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OD6V7E2YNROOH7YN73VD5IY5ANCNFSM5S2VWYQA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=skgib_A8Yh0zqVhY623O5SuKAvIwMBVtg733TbGJUGPVtl-qJ9PBYhW_MJKaTP5Q&s=ZmI0Nt97iDllZZ9-fxMyBploe7PE_bm5aUfMhTR27-8&e= . You are receiving this because you are subscribed to this thread.Message ID: @.***>

philderbeast commented 2 years ago

Dropping `GHC == 7.10.3" would allow us to use the newer warning syntax.

https://github.com/ucsd-progsys/liquid-fixpoint/blob/db2c3c7ce116cf953d361e04e918cd3be0732c31/liquid-fixpoint.cabal#L148

In GHC < 8 the syntax for -W was -fwarn- (e.g. -fwarn-incomplete-patterns). This spelling is deprecated, but still accepted for backwards compatibility. Likewise, -Wno- used to be fno-warn- (e.g. -fno-warn-incomplete-patterns). SOURCE: using warnings

ranjitjhala commented 2 years ago

Yes please thank you!

On Thu, Apr 28, 2022 at 6:31 AM Phil de Joux @.***> wrote:

Dropping `GHC == 7.10.3" would allow us to use the newer warning syntax.

https://github.com/ucsd-progsys/liquid-fixpoint/blob/db2c3c7ce116cf953d361e04e918cd3be0732c31/liquid-fixpoint.cabal#L148 https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_blob_db2c3c7ce116cf953d361e04e918cd3be0732c31_liquid-2Dfixpoint.cabal-23L148&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Thc9sM0auPlD_7QViwosJcNlWKiV-m4mu9G5-L54yOGU8iIxK2Q9hkTuJ_osLqQW&s=PgFdl0pk9gKD5AbTDEQpTyjumq92aDK6YBxhyPp_1eA&e=

In GHC < 8 the syntax for -W was -fwarn- (e.g. -fwarn-incomplete-patterns). This spelling is deprecated, but still accepted for backwards compatibility. Likewise, -Wno- used to be fno-warn- (e.g. -fno-warn-incomplete-patterns).

— Reply to this email directly, view it on GitHub https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_ucsd-2Dprogsys_liquid-2Dfixpoint_issues_538-23issuecomment-2D1112207342&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Thc9sM0auPlD_7QViwosJcNlWKiV-m4mu9G5-L54yOGU8iIxK2Q9hkTuJ_osLqQW&s=lR5jcF2sCAwIrlPfzdKimWk0OZIMYkdZ57w0uoH9xyg&e=, or unsubscribe https://urldefense.proofpoint.com/v2/url?u=https-3A__github.com_notifications_unsubscribe-2Dauth_AAMS4OAMN267JDJHTMM7E33VHKHJDANCNFSM5S2VWYQA&d=DwMCaQ&c=-35OiAkTchMrZOngvJPOeA&r=r3JfTqNkpwIJ1InE9-ChC2ld7xwATxgUx5XHAdA0UnA&m=Thc9sM0auPlD_7QViwosJcNlWKiV-m4mu9G5-L54yOGU8iIxK2Q9hkTuJ_osLqQW&s=zVuKacgtnTRU1_E2uwR1YPBwKfmyFoYjwZoq86FTyDE&e= . You are receiving this because you commented.Message ID: @.***>

philderbeast commented 2 years ago

I'm most of the way there with this one, can it be assigned to me please?

philderbeast commented 2 years ago

@facundominguez is this complete with #591?

Are we going to try for a stretch goal of having fewer {-# OPTIONS_GHC -Wno-name-shadowing #-}?

facundominguez commented 2 years ago

Are we going to try for a stretch goal of having fewer {-# OPTIONS_GHC -Wno-name-shadowing #-}?

This would be helpful to have eventually. I'd leave this issue open until then.