sanity_check

Stream: general

[Johan Commelin]

What is the attribute to mark something that shouldn't be checked by sanity check? I couldn't find it in the docs

[Rob Lewis]

@[sanity_skip]

[Sebastian Ullrich]

Should really be @[insane]

[Johan Commelin]

@Floris van Doorn Currently, if everything is fine in the file, then #sanity_check still prints some output. Would it be possible to have a version that only prints something if it finds something "insane"?

[Johan Commelin]

Because then it would be possible to have #sanity_check at the end of every file in a project, and it wouldn't create any noise during compilation, unless something is wrong.

[Johan Commelin]

#doc_blame already does this: it is silent if everything is fine.

[Johan Commelin]

Also... could it (maybe with some config option) report which file it is checking? Here is a snippet coming from a compilation of the perfectoid project:

/home/jmc/data/math/lean-perfectoid-spaces/src/for_mathlib/topological_groups.lean: parsing at line 294/- Note: This command is still in development. -/
/- Checking 23 declarations in the current file -/

/- OK: No unused arguments. -/
/- OK: All declarations correctly marked as def/lemma. -/
/- OK: No declarations have a duplicate namespace. -/
/- OK: No illegal constants in declarations. -/

linear_ordered_comm_group_with_zero.to_linear_ordered_comm_monoid
linear_ordered_comm_group_with_zero.to_comm_group_with_zero
/home/jmc/data/math/lean-perfectoid-spaces/src/valuation/basic.lean: valuation.comap_comp/- Note: This command is still in development. -/
/- Checking 26 declarations in the current file -/

/- UNUSED ARGUMENTS: -/
#print linear_ordered_comm_group_with_zero.ne_zero_filter_basis /- argument 4: (h : x ≠ 0) -/
#print linear_ordered_comm_group_with_zero.discrete_ordered_comm_group /- argument 2: [_inst_2 : linear_ordered_comm_group α] -/

[Johan Commelin]

The unused arguments are in the file src/valuation/with_zero_topology.lean...

[Johan Commelin]

(Ooh, and let me stress that I'm only complaining about this tool because it is so incredibly useful that it deserves to have these tiny improvements as well. Without this tool, these clean ups would be almost impossible.)

[Johan Commelin]

Once again: big kudos from me. :tada:

[Johan Commelin]

@Floris van Doorn Here is another thing: #sanity_check complains about

lemma directed_lt : directed (≥) (λ (γ₀ : units Γ₀), principal {γ : Γ₀ | γ < ↑γ₀}) :=

because this lemma mentions ≥. I can mark this as [sanity_skip], but I wonder if we can somehow detect that this is not something like (h : a ≥ b)...

[Floris van Doorn]

Vote with emotes: @[sanity_skip] should be renamed @[insane]

[Floris van Doorn]

Floris van Doorn Currently, if everything is fine in the file, then #sanity_check still prints some output. Would it be possible to have a version that only prints something if it finds something "insane"?

I'll add an option to toggle that, and turn that option on for #sanity_check.

Also... could it (maybe with some config option) report which file it is checking?

I don't know how to access the current file name via metaprogramming. Is this possible (Maybe using the IO monad)?

(Ooh, and let me stress that I'm only complaining about this tool because it is so incredibly useful that it deserves to have these tiny improvements as well. Without this tool, these clean ups would be almost impossible.)

I'm happy that it is helpful, and also like to add these quality of life features!

Floris van Doorn Here is another thing: #sanity_check complains about

lemma directed_lt : directed (≥) (λ (γ₀ : units Γ₀), principal {γ : Γ₀ | γ < ↑γ₀}) :=

because this lemma mentions ≥. I can mark this as [sanity_skip], but I wonder if we can somehow detect that this is not something like (h : a ≥ b)...

I'll add a check that ge is fully applied.

[Johan Commelin]

Thanks! And I'm sorry that I can't help you with figuring out the filename...

[Keeley Hoek]

@[nolint], why are there no lint ⟶ leant puns!?! :D

[Simon Hudon]

I've been very quit about it but those punts have been happening in my head :P

[Anne Baanen]

To be honest, I would prefer another name (like "lint") for sanity_check, since the programming environments I'm used to interpret "sanity check" as a correctness test, not readability test. Also, some consider the term "sanity check" to be disparaging to people with mental illness (although I can't find a good source for this right now).

[Anne Baanen]

(This StackExchange answer mentions the last point briefly: https://english.stackexchange.com/questions/387320/non-idiomatic-synonym-for-sanity-check/387355#387355)

[Simon Hudon]

I think linting or style check might be better substitute

[Keeley Hoek]

https://en.wikipedia.org/wiki/Linter_(software) is the famous name, after all; and I'd claim even nolint is ubiquitous, though I'd only support that claim with a google search

[Johan Commelin]

+1 for renaming to lint

[Floris van Doorn]

I'm happy to rename #sanity_check. I'm a bit hesitant renaming it to lint, since it doesn't do many things a linter normally does. My command doesn't even have access to the source code in the .lean file...

[Simon Hudon]

The good news is that, if someone writes a linter that has access to the Lean files, it's probably not how it's going to be called.

[Jesse Michael Han]

maybe we could rename it #insanity_check (because it's really checking for insane things in our code); then @[sanity_skip] becomes @[sane], which makes more sense :^)

[Simon Hudon]

@Jesse Michael Han you might have missed the bit about disparaging people with mental illness

[Patrick Massot]

@Floris van Doorn Could you have a look at what sanity_check says in topology/algebra/group_completion? It incorrectly reports an unused argument in uniform_space.completion.is_add_group_hom_map.

[Floris van Doorn]

It is an unused argument:

theorem uniform_space.completion.is_add_group_hom_map : ∀ {α : Type u_1} [_inst_1 : uniform_space α] [_inst_2 : add_group α] [_inst_3 : uniform_add_group α]
{β : Type u_2} [_inst_4 : uniform_space β] [_inst_5 : add_group β] [_inst_6 : uniform_add_group β]
[_inst_7 : add_group β] [_inst_8 : uniform_add_group β] {f : α → β} [_inst_9 : is_add_group_hom f],
  continuous f → is_add_group_hom (completion.map f)

Note that [add_group β] [uniform_add_group β] both occur twice. If you remove both duplicates from the declaration, it will happily compile. If you only remove _inst_8 it will not compile, because the two difference add_group instances will conflict with each other, that confused me (too) when I tried to remove it.
Note that my duplication test doesn't apply here, since _inst_6 and _inst_8 have different implicit arguments (and _inst_5 is not marked as unused, since it is used in _inst_6)

[Patrick Massot]

Oooh. Ok

[Mario Carneiro]

oh, I guess the unused check should ignore uses by other unused variables, which makes this a graph reachability problem

[Mario Carneiro]

actually it's probably better to just rerun the unused analysis until fixpoint, because that will perform better in the common case that nothing is unused

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

(deleted)

[Kevin Buzzard]

[really sorry -- wrong thread]

[Reid Barton]

It occurs to me that naming topological spaces X, rings R, and so on, and reserving α, β, ... for types which really have no extra structure (such as types which index families) would also go some way towards making one class of errors caught by sanity_check more unlikely, those where we accidentally have an unwanted [topological_space α] hypothesis.

[Reid Barton]

(Besides making it easier to set up variables that work as intended throughout a file, even if one ignores the possibility of making mistakes.)

[Patrick Massot]

@Floris van Doorn I met a new problem with the ge vs le check. sanity_check complains about every lemma containing ∀ ε > 0, .... And I think we want to keep those.

[Sebastien Gouezel]

I don't think we want to keep those, they create many problems down the road. We still can't write ∀ 0 < ε, but ∀ε (h : 0 < ε), ... is not so bad.

[Kevin Buzzard]

I always felt that ∀ 0 < ε was somehow not "correct" -- I would always parse it as "for all zero,...".

[Floris van Doorn]

I have no strong opinions either way.

[Simon Hudon]

The problem with ∀ 0 < ε is: what happens if, instead of 0 we want to use x? In ∀ x < ε which one is the bound variable and which one is the free variable? Whichever choice we make, there are people who will assume the opposite

[Scott Morrison]

I just read somewhere else:

Nonsensical abbreviations like ∃0 <i<n [...] are not justifiable by the space that they save.