Linting

[xrchz]

We would like to automatically check various stylistic conventions in the CakeML code base (i.e., to run a linter as part of the regression test). This issue is to implement the first version of the linter, probably as an extension to the existing README checker and generator, and to incorporate it in the regression test.

For the first version, the linter should check the following uncontroversial conventions:

• max line width of 80 columns
• no trailing whitespace
• no tabs
• (inherit readme-gen's checks)
• optional: check store_thm (etc.) has a matching name and bound variable

As is common with linters, it should be possible to circumvent the automatic checks with an explicit comment.

(Note: other, more controversial, ideas for linting conventions are being collected on the Candle backlog.)

[mn200]

The first three of these are now checked by the (misleadingly named) unicode-grep tool in the HOL distribution.

[xrchz]

Would using unicode-grep for this be a reasonable gateway to linting more complex and controversial CakeML conventions? How much are you willing to add to that tool? We could use it for CakeML by making the regression test worker call it, but if we're also going to have our own linting tool, I don't mind duplicating the simple whitespace+width checks above.

[mn200]

Yes, I think using it would be reasonable, and I'm certainly willing to add further to it. I will try to add a --lint option to Holmake to enable the specification of a tool that will be run before anything else happens in a directory. This could then be passed unicode-grep as an argument, or anything else more CakeML specific. Of course, this option could be made "easy to access" by putting it into a CLINE_OPTIONS spec inside a Holmakefile.

[myreen]

Related to the "optional: check store_thm" point, @mn200 and I are considering changes to HOL that would make HOL treat

Theorem foo[simp] goal tactic

as if it was

val foo = Q.store_thm("foo[simp]",goal,tactic)

As of a few minutes ago, HOL master has this behaviour.

One could eventually move towards a state of the codebase where Theorem is used instead of store_thm. The linter could eventually enforce this, if it is the direction we want to go in.