Zulip Chat Archive

Stream: general

Topic: declaration linter


view this post on Zulip Reid Barton (Oct 19 2018 at 16:30):

I wrote a "declaration linter" that processes each declaration and checks for things that look dodgy.
Currently, it looks for lemmas whose type is not a Prop, and structures/classes which could be Props but aren't.
Here's the output on the core library and (a slightly out-of-date) mathlib: https://gist.github.com/rwbarton/4e119ba9b812debac08c8a54afb104bd

view this post on Zulip Reid Barton (Oct 19 2018 at 16:31):

I want to add warnings for unused variables next, but that will be a bit more difficult.

view this post on Zulip Reid Barton (Oct 19 2018 at 16:35):

Hmm, some of the output is duplicated--not sure why

view this post on Zulip Reid Barton (Oct 19 2018 at 16:35):

Start at line 141

view this post on Zulip Reid Barton (Oct 19 2018 at 16:37):

Ah, I figured out why--some leftover testing code.


Last updated: May 08 2021 at 19:11 UTC