Stream: Coq users

Topic: Linter?

view this post on Zulip Cody Roux (Sep 11 2020 at 20:33):

When do we get a linter for Coq?

view this post on Zulip Karl Palmskog (Sep 11 2020 at 20:36):

there are many levels to linting. If you mean things like naming and spacing, then we have work on the former here and we reported on work-in-progress for the latter here. Members of the Lean community have some other forms of linting here.

view this post on Zulip Karl Palmskog (Sep 11 2020 at 20:41):

the bottom line is that I don't think anyone will make a general rule-based linter anytime soon for Coq, since it would be very hard to make it work across the extremely diverse set of Coq styles/projects. Thanks to work by devs, we can at least access Coq syntax nowadays without implementing higher-order unification.

view this post on Zulip Cody Roux (Sep 11 2020 at 21:05):

Thanks Karl! I was being a bit tongue-in-cheek, but I would be a user of a very simple tool that enforces spacing and indentation according to some God-given criteria, as well as some minor name checks, e.g. CamelCase vs names_with_underscores (though I've seen some Horrible_Hybrids).

view this post on Zulip Karl Palmskog (Sep 11 2020 at 21:51):

we will probably try to do a simplified tool for spacing trained on, say, the standard library with some additional heuristics as a showcase.

view this post on Zulip Karl Palmskog (Sep 11 2020 at 21:57):

old school solution here: http://www.eelis.net/coqindent/

view this post on Zulip Bas Spitters (Sep 12 2020 at 08:28):

I imagine that coq indent could be simplified with serapi and add support for bullets. It would already be useful for students.
http://www.eelis.net/coqindent/

view this post on Zulip Robin Green (Sep 12 2020 at 09:56):

For the special case of correcting incorrect indentation after removing superfluous braces, I have found that in vscoq you can just hold down the middle mouse button and drag to select the wrongly-indented text, and it seems to correctly reindent it. Not sure how general this is, or how it works, but it might be useful.

view this post on Zulip Paolo Giarrusso (Sep 12 2020 at 10:24):

I think VsCoq indentation just depends on the source syntax, unlike coqindent. OTOH, I wouldn't personally want indentation based on goal count; that's what bullets are for. And possibly, Set Default Selector "!".

Last updated: Oct 01 2023 at 19:01 UTC