Skip to content
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

Apply formatting and linting #330

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from

Conversation

dragospe
Copy link

@dragospe dragospe commented Jun 8, 2024

Following some discussion at Zurihac, I wanted to give my take on the formatting/linting question.

This change will impact practically every file in the codebase, which can be difficult for contributors with open PRs. I've split up this PR into two separate commits:

  • 3f03d37: this is the commit that adds the formatting/linting utilities, and updates the Makefile with relevant commands and the README with some documentation
  • 01213d2: runs the make format and make lint commands. THIS BREAKS THINGS.

I'm marking this currently as draft, because there are a few things I still need to work out.

  • Add this to CI. Having formatting/linting goes out of sync quickly if its not enforced.
  • Determine what type(s) of breakage come from using these tools. Currently, all of the haskell compiles, but some of the tests don't run. This is may actually highlight some issues with Agda2hs itself, too; or it may just indicate that hlint/fourmolu/cabal-fmt don't work well with the generated code.

I think there was someone else who also had ideas here. Happy to chat and compare approaches -- the setup here is just my default when I'm starting new projects.

Copy link
Member

@jespercockx jespercockx left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In general I think this is a good idea and we should investigate further. My main concern with the output of the auto-formatter is the extra indentation it sometimes creates, which is something I am personally quite sensitive to.

Also, we should exclude the files in the golden directory from the auto-formatter, though we could consider applying auto-formatting to the output of agda2hs when generating the Haskell code.

sig <-
if not withSig
then return []
else do
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This seems to create a lot of extra indentation that I'd rather avoid.

@@ -16,5 +16,4 @@ testCong :: Int
testCong = 1 + testRezz

rTail :: [Int] -> [Int]
rTail = \ ys -> tail ys

rTail ys = tail ys
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We should not apply the linting to the files in the golden directory, since these are the expected outputs of the test suite. However, we could consider applying the auto-formatter to the code generated by agda2hs (which would then lead to an update of the golden files too).

@anka-213
Copy link
Member

..., though we could consider applying auto-formatting to the output of agda2hs when generating the Haskell code.

I do agree with this part, since, even though the formatting is generally quite decent, the formatting of the output from agda2hs can sometimes be fairly ugly, especially for things like large records or long type-lines.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants