search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
228 stars 36 forks source link

Command line flag to disable warnings #34

Closed JasonGross closed 3 years ago

JasonGross commented 3 years ago

I'd like to be able to suppress warnings for long lines. But there don't seem to be any relevant flags?

cpitclaudel commented 3 years ago

Indeed, there's only a python-level option ATM. Is that enough for your case or do you want a command-line flag?

JasonGross commented 3 years ago

I would very much prefer a command-line flag; the HoTT library does one-line comments and relies on editors to linewrap them, so we get hundreds of useless "line very long" warnings from alectryon. (Alternatively, perhaps what we really want is a way to set the maximum line width from the command line, and a toggle to tell alectryon that it's allowed to line-wrap comments if it doesn't already. (And if it does already line-wrap comments, then perahps this warning should be disabled by default on lines where the default comment-wrapping behavior will display things nicely for us.))

JasonGross commented 3 years ago

There is no reason, IMO, to complain about the comment on the first line of https://hott.github.io/HoTT/alectryon-html/HoTT.Basics.Notations.html, for example. image

cpitclaudel commented 3 years ago

More generally, I think we shouldn't complain at all about long comments — only about long code lines, if anything. at all

cpitclaudel commented 3 years ago

More generally, I think we shouldn't complain at all about long comments — only about long code lines

I'd like to do this eventually, but it's a bit of a pain to handle lines that mix code and comments, so I'll leave this open for now.