LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Use new-style HLint comments #660

Closed georgefst closed 1 year ago

georgefst commented 1 year ago

My primary motivation for this is cross-compiling SBV. Before this change, this wasn't possible due to the warning Ignoring ANN annotation, because this is a stage-1 compiler without -fexternal-interpreter or doesn't support GHCi, combined with -Werror. With the change, it's only blocked by #659.

Out of interest:

LeventErkok commented 1 year ago

Do these have an extra stray $ at the end of each hint? Looks odd to me. And the hlint check fails on them. See below.

georgefst commented 1 year ago

Ah, yes, sorry, I am genuinely unsure how I managed to mess that up. Fixed now.

LeventErkok commented 1 year ago

Thanks for the PR. Regarding your specific questions:

  1. -Werror is my personal preference. SBV never claimed to work with anything but the latest GHC, and I keep track of the changes in GHC to make sure it compiles cleanly with it. Nothing deeper than that.
  2. HLint policy is to keep it lint-free when I run the following target in the Makefile: https://github.com/LeventErkok/sbv/blob/3bdc3fdb804d74f7f654c841bae1c42c6c9e789d/Makefile#L73-L74 Looks like I'm not checking the "Documentation" directory; that's an oversight which I'll fix. It's of course entirely possible that some pragmas are outdated, or they can be reduced; but in a project like SBV that's been around for more than a decade, this sort of cruft accumulates. Happy to accept PRs that improve the hlint pragmas anytime.