Zulip Chat Archive

Stream: general

Topic: How long should lines be?

Kevin Buzzard (Feb 04 2019 at 18:23):

Are there general guidelines here which I could slavishly follow? One of my co-authors has put some very long lines in the perfectoid project but I don't know whether I should be worried by this.

Johan Commelin (Feb 04 2019 at 18:23):

mathlib wants <= 100.

Johan Commelin (Feb 04 2019 at 18:23):

I think we can follow that.

Kevin Buzzard (Feb 04 2019 at 18:29):

I think you might be the author of a 151-character line in the perfectoid project :-)

Johan Commelin (Feb 04 2019 at 18:29):

git blame it

Johan Commelin (Feb 04 2019 at 18:29):

I will happily believe you though (-;

Kevin Buzzard (Feb 04 2019 at 18:30):

https://github.com/leanprover-community/lean-perfectoid-spaces/blame/8968057b78c8902044515a94a28489f24d3da86d/src/continuous_valuations.lean#L20

Johan Commelin (Feb 04 2019 at 18:31):

That does look like me (-;

Kevin Buzzard (Feb 04 2019 at 18:32):

Can I make VS Code punish me if I go over 100 characters?

Chris Hughes (Feb 04 2019 at 18:35):

A recent mathlib update gives me a line in the editor at 100 characters.

Johan Commelin (Feb 04 2019 at 18:37):

https://github.com/leanprover-community/mathlib/blob/master/.vscode/settings.json#L4

Kevin Buzzard (Feb 04 2019 at 18:39):

I never used to care about this sort of thing, but when I forget my glasses I have to start changing font size and then it becomes an issue.

Last updated: Dec 20 2023 at 11:08 UTC