Small executable to fix whitespace issues

[gallais]

Following #931 we have a linting action making sure we do not have trailing whitespace. People can add a git pre-commit hook so that it is impossible to commit until there are no whitespace issues left.

It would be nice to have a script that not only reports these issues but fixes them too. Agda uses this but the Haskell dependencies may be a bit too much.

It may be a good Idris project for those who want to write a little executable.

[stefan-hoeck]

I'll give this a try but got some questions:

• Are you looking for an Idris project explicitly or would a (POSIX) shell script be just as fine?
• Should the concept of "line break" be platform independent, or are we only dealing with Unix newlines ('\n')?

[gallais]

The current linter goes beyond just Unix newlines but switching from one style to another in commits would also introduce needless noise so I think it's desirable to enforce the sole use of Unix newlines.

I am not dead set on an Idris program (the linter itself is in Python3 for instance) but that would solve the issue of not having any additional external dependencies, and being portable across all of the platforms Idris2 compiles on.

[stepancheg]

Eventually, in the distant future it should not just fix whitespaces, but also reformat idris files (normalize indentation, sort imports). We may call it idris2fmt (similarly to gofmt or rustfmt).

BTW, why do you need to fix whitespaces with some utility? Virtually all editors/IDEs support editorconfig nowadays. Even Vim and Emacs.

[gallais]

Virtually all editors/IDEs support editorconfig nowadays. Even Vim and Emacs.

Good to know. The addition of editorconfig is really recent so maybe the errors we got in the past few days were leftovers from PRs opened prior to that addition.

[buzden]

Even Vim and Emacs

Well, I'm as a vim user knew about editorconfig only by the pull request #932. Then I knew that vim needs a plugin to support it. It's great and I installed it but still it's easy to use vim without this plugin.

So, maybe, we need at least mention usage of such plugins somewhere. But where? CONTRIBUTING.md contains things that are needed, but not guidelines or rules of contributions.

[stefan-hoeck]

A first (hopefully) working version of an Idris program can be found here. Although I do not know whether we still need this, it might still be useful. So far, I only tested this on Linux. Have fun.

While writing this, I came up with a port of Haskell's GetOpt module. This could probably go to contrib. I'll write a PR if there is any interest.

I used some monad transformers form base (ReaderT and EitherT) and found that there are quite a few transformer instances missing. For instance, there is no MonadReader instance for StateT nor is there a MonadState instance for ReaderT. Again, if there is any interest, I could draft a PR for adding these missing instances.

[stefan-hoeck]

May I ask, what the status is on this? Should the fix_whitespace program I linked to be somehow included in this repository or do we need something different. I'd be glad to help out but am not sure how to proceed.

[gallais]

@stefan-hoeck That looks quite nice. I do agree that some of the library code could go straight to contrib. As for the executable itself, it could live here in a tools/ directory or as part of https://github.com/idris-community as it's useful beyond just the Idris2 compiler.