Pull requests to OCaml now being linted

Community
#1

OCaml GPR#1148 has been merged this weekend. Contrary to the title of this PR, the most relevant thing for contributors to the compiler itself is that pull requests are now run via our linting tool which resides in tools/check-typo in the compiler distribution. It produces output like the following:

./asmcomp/selectgen.ml:798.81: [long-line] line is over 80 columns
./asmcomp/selectgen.ml:1129.81: [long-line] line is over 80 columns
./bytecomp/simplif.ml:419.81: [long-line] line is over 80 columns
./bytecomp/symtable.ml:43.3: [white-at-eol] whitespace at end of line
./bytecomp/symtable.ml:62.3: [white-at-eol] whitespace at end of line
./tools/dumpobj.ml:533.81: [long-line] line is over 80 columns
./typing/includemod.ml:167.48: [white-at-eol] whitespace at end of line
./typing/includemod.ml:168.64: [white-at-eol] whitespace at end of line
./typing/includemod.ml:319.81: [long-line] line is over 80 columns
./utils/misc.ml:180.40: [white-at-eol] whitespace at end of line
./utils/misc.mli:105.7: [white-at-eol] whitespace at end of line

It’s necessary for this test to pass (in certain situations it’s possible to override the tests via .gitattributes, but in general this is not permitted). It’s hoped that this won’t cause too much pain for our wonderful contributors, and, to ease development, that GPR includes a Git pre-commit hook which can be installed to your local Git clone simply by running cp tools/pre-commit-githook .git/hooks/pre-commit (even on Windows). Once installed, the hook blocks attempts to commit files which are invalid:

[git:git-precommit] C:\DRA\ocaml>git commit -m "GPR#1148 Changes"
./Changes:108.81: [long-line] line is over 80 columns

If you’re in a rush or, perish the thought, there’s a bug in the pre-commit hook, you can always use the --no-verify flag for git commit to skip the check-type test, but bear in mind that Travis will still test it.

Please do report any issues either here, on caml-list or on Mantis.

Happy linted compiler hacking!

5 Likes
#2

I see that you added a mention of the test in CONTRIBUTING.md, but maybe it would also be worth adding the explanation (with example outputs from the tool and git commit) to HACKING.adoc?

1 Like
#3

Good idea, @gasche! Will do.

#4

Hi, IMHO in general it’s a bad idea to abort commits on lint failure, for two reasons: (1) a lot of people’s git workflow is to make small commits and use them as snapshots, to be cleaned up later; and (2) for any size of commit it’s very distracting and discouraging to have typed up a good commit message and then have it thrown away by a lint failure.

I’d recommend turning off the pre-commit lint and moving it to pre-push.

#5

@yawaramin - that’s not how pre-commit hooks work. The hook runs before you’ve entered a commit message, so either you haven’t typed it yet or you used -m "message" and it’ll be in your command history to re-use (also bear in mind that any previously used commit message would still be in .git/COMMIT_EDITMSG)

I already plan to adapt the script used in tools/ci/travis/travis-ci.sh to provide a script to check whether your branch passes tools/check-typo - that’s a great idea also to provide it as pre-push hook as well.

Regarding workflow, if using a pre-commit hook doesn’t fit your Git workflow, then please of course don’t use it! The script provided is only intended to assist that the fact that a PR now won’t be merged if it doesn’t pass tools/check-typo.

#6

Ah, my mistake about the pre-commit hook. I was under that impression based on a discussion I’d had at a previous workplace. I guess I misunderstood.

In any case, not interfering with the commit process (whether before or after composing the message) is a good idea :slight_smile:

#7

As I said, that depends on your chosen Git workflow. We can’t force use of a hook, so it remains your call! (incidentally, linting whitespace is the “official” example of a pre-commit hook - see .git/hooks/pre-commit.sample in any Git repo you’ve ever cloned)