theorem names with primes?

Stream: mathlib4

[Kim Morrison]

I've always been sad about theorem names with primes. Sometimes though it is really hard to come up with a better name.

How about we add a linter that requires that theorem names ending with a prime have a doc-string. The linter error should explain that the doc-string should at least explain how the statement differs from the unprimed version, and possibly explain why no better naming scheme is possible. (Thereby forcing people to think about it before just going with a prime!)

Of course we would have to nolint or set_option all the existing primed lemmas.

[Bhavik Mehta]

Or fix all the existing primed lemmas!

[Kim Morrison]

Thanks, Bhavik, looking forward to merging your PR. :-)

[Johan Commelin]

This will add a massive entry in our technical-debt-counters table

[Kim Morrison]

Better late than never?

[Johan Commelin]

Yeah, I didn't mean to suggest that we shouldn't do this :smile:

[Damiano Testa]

I'm looking into this!

[Damiano Testa]

Should the doc-string of the ' declaration explicitly mention the un-primed declaration (whether it exists or not), or is it enough for it to have a doc-string?

[Kim Morrison]

I think it would be okay to merely enforce having a doc-string.

[Kim Morrison]

If people want to say "this differs from the unprimed version by ..." I don't think we want to police that.

[Damiano Testa]

#16694

[Damiano Testa]

It is doing its very first run, so I expect some issues to surface! :smile:

[Damiano Testa]

... such as forgetting to import it in Mathlib.Init. :man_facepalming:

[Damiano Testa]

Should the current exceptions be flagged with set_option or should there be a nolint file containing them?

[Damiano Testa]

By the way, I set up the linter to catch ' anywhere in their name. Is this ok, or were you thinking of just terminal '?

[Damiano Testa]

A rough estimate is that there are

• ~8k exceptions with a ' anywhere, and
• ~6k exceptions with a terminal '.

[Kim Morrison]

Wow... that is a lot of exceptions. :-(

[Damiano Testa]

Ok, there are really 6119 exception in Mathlib.

[Kim Morrison]

We can't possibly do that with set_option, I think. I don't know, I'd want to have buy in from everyone before adding that many set_options...

[Damiano Testa]

and 4811 with a terminal '-

[Damiano Testa]

The exceptions are distributed over 1419 files, so even blanket exceptions at the beginning of the files may not cut it...

[Damiano Testa]

The files with at least 20 exceptions:

20  Mathlib/Algebra/Group/Basic.lean
20  Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean
20  Mathlib/Order/Basic.lean
20  Mathlib/Topology/Order/OrderClosed.lean
21  Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
22  Mathlib/Data/Nat/Defs.lean
22  Mathlib/Topology/ContinuousOn.lean
22  Mathlib/Topology/Order/Basic.lean
23  Mathlib/Topology/Basic.lean
24  Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
24  Mathlib/MeasureTheory/Integral/Lebesgue.lean
25  Mathlib/Algebra/Homology/ShortComplex/Homology.lean
25  Mathlib/Analysis/Asymptotics/Asymptotics.lean
25  Mathlib/GroupTheory/Complement.lean
26  Mathlib/Algebra/CubicDiscriminant.lean
26  Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
26  Mathlib/Order/CompleteLattice.lean
26  Mathlib/Order/Filter/Basic.lean
27  Mathlib/Analysis/Calculus/FDeriv/Mul.lean
29  Mathlib/Data/Num/Lemmas.lean
30  Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
30  Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
30  Mathlib/Topology/Order/Lattice.lean
31  Mathlib/Algebra/Order/ToIntervalMod.lean
31  Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
33  Mathlib/Data/Matrix/Block.lean
34  Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
34  Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
34  Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
34  Mathlib/MeasureTheory/Integral/SetToL1.lean
35  Mathlib/GroupTheory/MonoidLocalization/Basic.lean
36  Mathlib/LinearAlgebra/Matrix/ToLin.lean
37  Mathlib/Order/Filter/Lift.lean
39  Mathlib/Data/List/Basic.lean
39  Mathlib/Data/List/Chain.lean
41  Mathlib/Algebra/Module/LocalizedModule.lean
47  Mathlib/RingTheory/Localization/Basic.lean
51  Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
59  Mathlib/Analysis/Normed/Group/Basic.lean
65  Mathlib/Data/Ordmap/Ordset.lean
94  Mathlib/Data/Finset/Lattice.lean

[Yaël Dillies]

A bunch of such lemmas are due to the Group vs GroupWithZero naming convention. However, we have decided ages ago to switch from '/ to /₀. I would rather have us finish those renames before enforcing a "no prime policy".

[Yaël Dillies]

Yaël Dillies said:

A bunch of such lemmas are due to the Group vs GroupWithZero naming convention. However, we have decided ages ago to switch from '/ to /₀. I would rather have us finish those renames before enforcing a "no prime policy".

[Damiano Testa]

Is there some easy way to tell if a declaration has a prime due to the GroupWithZero convention? Even if it is not failsafe, but does not require looking at too many concurrent issues, I could try to include it in the linter and see if that reduces drastically the number of exceptions.

[Damiano Testa]

If it only cuts it down by a factor of 2 or 3, it may not be enough to address that issue first.

[Damiano Testa]

For instance, there are only 686 declarations with a ' and containing the substring mul.

[Damiano Testa]

Here is a random sample of primed names

elim'_none
inf_compl_eq_bot'
NeZero.ne'
le_coe_unbot'
inv_le_iff_one_le_mul'
le_div_iff_of_neg'
ciSup_or'
map₂Right'_nil_cons
Chain'.take
inf'_product_right
Applicative.pure_seq_eq_map'
orbitRel.quotient_eq_of_quotient_subgroup_eq'
finSuccEquiv'_symm_coe_below
mem_span_insert'
min'_eq_sorted_zero
linearIndependent_equiv'
mul_top'
neg_of_smul_neg_left'
Matrix.toLinAlgEquiv'_toMatrixAlgEquiv'
ofDigits_zmodeq'
algEquiv_symm_mk'
natDegree_pow'
map_comp_heq'
composePath_comp'
homologyMap'_eq
toIocDiv_sub'
Continuous.quotient_map'
nhdsWithin_Ici_eq'
cauchy_map_iff'
NNReal.closedBall_zero_eq_Icc'
str'
algebraMap_eq_inl'
ext_to_X'
Basis.det_map'
coe_chainTop'
hasProd_nat_add_iff'
sum_apply_eq_zero'
dist_le_norm_add_norm'
Finset.norm_prod_le'
rpow_add_natCast'
lintegral_rpow_nnnorm_lt_top_of_eLpNorm'_lt_top
coe_flipₗᵢ'
integral_neg'
conjneg_neg'
negAddY_eq'
map_on_summand₀'
iteratedFDerivWithin_eventually_congr_set'
expSeries_apply_eq'
stolzCone_subset_stolzSet_aux'
algebraMap_adicCompletion'
apriori_edist_iterate_efixedPoint_le'
dart_edge_eq_mk'_iff'
unpaired'
destutter'_nil
valid'_singleton
pNilradical_eq_bot'
inv_rnDeriv'
orbitRelEquiv_apply_mk''
measurableSet_eq_of_countable_range'
Cotangent.val_smul'''
closure_def'

(I extracted the exceptions whose position in the list of exception is divisible by 100.)

[Ruben Van de Velde]

Do any involve names of definitions that already include a prime?
(Does this need to be in the private stream?)

[Kim Morrison]

Let me move it out, sorry, my mistake.

[Damiano Testa]

Ruben Van de Velde said:

Do any involve names of definitions that already include a prime?
(Does this need to be in the private stream?)

Very likely (and the primed definition would be linted as well).

[Bhavik Mehta]

Yaël Dillies said:

A bunch of such lemmas are due to the Group vs GroupWithZero naming convention. However, we have decided ages ago to switch from '/ to /₀. I would rather have us finish those renames before enforcing a "no prime policy".

Aren't these consistent policies? Switching from primes to zeros and enforcing "no prime" seem to go hand-in-hand rather than opposing each other

[Damiano Testa]

I agree, although the fix is different.

[Yaël Dillies]

Yes, my point is that those Group/GroupWithZero renames are a principled established way of removing the primes which don't involve people removing primes in random ways because the technical debt counter said so

[Violeta Hernández]

I was just adding a primed lemma! :frown:

[Violeta Hernández]

Specifically, I wanted to generalize the universes of a theorem, but had to keep the old version due to the issue where a Small.{u, max u v} instance can't be synthesized. So, I guess this is an example of tech debt.

[Damiano Testa]

You, and 6119 other people before you...

[Eric Wieser]

Damiano Testa said:

Should the current exceptions be flagged with set_option or should there be a nolint file containing them?

My understanding was that set_option is intended for "I know what I'm doing stop annoying me", and nolints.json is for "here is a TODO list of things to fix"

[Damiano Testa]

Ok, so then the linter should be made aware of the exceptions by reading from the appropriate nolints file. (Not a problem, just a small extra piece of code.)

[Damiano Testa]

Now that I think of it, the linter misses out on declarations that do not have explicitly a ' but that are inside a namespace SomethingWith'.

[Damiano Testa]

(There are not that many such namespaces, but there are some.)

[Damiano Testa]

I added the list of exceptions to the primed linter. It failed the latest run, since yet another primed declaration was added. It also did not get a chance to run on Archive and Counterexamples.

[Damiano Testa]

Does adding this linter seem like a good idea, or not really?

[Jon Eugster]

I think it's a good idea that primed theorems should have docstring :+1:

Regarding Yaël Dillies 's remark

However, we have decided ages ago to switch from '/ to /₀. [in group theory]

is this noted somewhere? If not, it would probably be good if people deciding this made an effort of getting it done, and I think the no-lint file in this PR might actually help with the chore.

[Kim Morrison]

I think it's actually good idea. It adds an annoyingly large amount to our nolint file, and I don't think we need to aspire to dealing with that quickly, but it would be good to have a better trajectory going forward.

[Yaël Dillies]

Jon Eugster said:

it would probably be good if people deciding this made an effort of getting it done

It is one of my (many) battles

[Damiano Testa]

Ok, I need to think a bit more about the nolint file though. Right now, the linter reads the exceptions from a file. Adding an exception to the file, though, does not re-trigger building files that logged warnings.

[Damiano Testa]

This means that to add an exception, you should add it to the exception file and modify the file with the primed lemma (or an earlier file), since otherwise lake will replay the file with the warning, even though the warning would not be there this time!

[Damiano Testa]

Yaël Dillies said:

It is one of my (many) battles

This linter might help with that, suggesting using ₀ instead of ' if appropriate.

[Damiano Testa]

Btw, is there a lake setting that will take warning as errors seriously and rebuild files that had warning, instead of replaying them?

[Kim Morrison]

@Damiano Testa, I think it is lake build --wfail

[Floris van Doorn]

Damiano Testa said:

Now that I think of it, the linter misses out on declarations that do not have explicitly a ' but that are inside a namespace SomethingWith'.

I recommend only flagging declarations that end with a prime. If there is a prime anywhere else, that likely indicates that it is something about another primed declaration, and there is no reason to flag this declaration as well as the other one.

[Damiano Testa]

Kim Morrison said:

Damiano Testa, I think it is lake build --wfail

That is what is already in CI and it fails the whole build with warnings, but replays them the second time, instead of rebuilding them. At least, this is what I think it does based on what is happening with this PR.

[Kim Morrison]

You may need to ask Mac for that one, I don't think it exists.

[Jon Eugster]

I think Sebastian once told me of a way you can include the no-lint json as build artifact so that modifying it causes lean files depending on it (or the entire project?) to be rebuild. I dont remember how though

[Martin Dvořák]

One of the things we should do in order to get rid of ' in theorem names is to stop using neg both for < 0 and for - (unary minus).

[Violeta Hernández]

I recently came across two other widespread uses of primes:

• docs#List.Chain' which disambiguates from docs#List.Chain
• Lemmas on docs#ConditionallyCompleteLinearOrderBot generally use primes to distinguish from other weaker typeclasses, e.g. docs#le_csSup_iff'

[Eric Wieser]

Martin Dvořák said:

One of the things we should do in order to get rid of ' in theorem names is to stop using neg both for < 0 and for - (unary minus).

There is a thread somewhere about switching to lt_zero naming

[Damiano Testa]

I made the linter only flag terminal ' in names.

[Damiano Testa]

As for building issues, I think that it may be useful to have lake build take various flags, since replaying-with-warnings is useful, as is rebuilding-from-warnings!

[Damiano Testa]

I'm wondering whether it would be acceptable to make the linter import the exceptions file (where all the file consists of a commented list of exceptions), so that any change in that file triggers a rebuild from scratch.

[Damiano Testa]

What do people think of the docPrime linter? Should declarations ending in ' be allowed without a doc-string?

[Damiano Testa]

If not, then it would be good to know this in advance, since every time that I merged master, there were a couple of new primed-declarations in mathlib that required a full re-run.

[Damiano Testa]

If not, then I can simply close the PR and be happy about it! :smile:

[Mario Carneiro]

Damiano Testa said:

If not, then it would be good to know this in advance, since every time that I merged master, there were a couple of new primed-declarations in mathlib that required a full re-run.

that means it's working

[Bryan Gin-ge Chen]

Should we have a poll?

[Damiano Testa]

/poll Should declarations whose name ends with ' be required to have a doc-string?
Yes
No

[Damiano Testa]

(Note that an implication of voting Yes is somehow dealing with close to 5k current exceptions that would be placed in a nolint file in bulk.)

[Damiano Testa]

As there seems to be a good support for the PR, I preemptively updated the nolints file, so the current run should be green and contain all of the latest commits.

[Damiano Testa]

I left the mechanism for adding exceptions to the file intentionally awkward, since I get the impression that the nolints file should only decrease, after its creation.

[Damiano Testa]

Should this change, I can always add better infrastructure for managing the file.

[Violeta Hernández]

I agree with this on principle, but I'd first like to see an action plan to either refactor or document the broad families of exceptions we have. Otherwise we'll just keep adding more and more primed lemmas, most of which will have very useless docstrings.

[Violeta Hernández]

Violeta Hernández said:

I recently came across two other widespread uses of primes:

• docs#List.Chain' which disambiguates from docs#List.Chain
• Lemmas on docs#ConditionallyCompleteLinearOrderBot generally use primes to distinguish from other weaker typeclasses, e.g. docs#le_csSup_iff'

Here's a third potential source of trouble: docs#Cardinal.aleph' (which is disambiguated from docs#Cardinal.aleph by including finite cardinals). I don't think we currently have any lemmas ending in aleph', but it's perfectly reasonable we might add some later on, which might not necessarily make sense or be true for aleph.

[Damiano Testa]

I really hope that this would be an incentive to write good documentation. When I find a primed lemma name, it is not always easy to figure out what is the difference with the unprimed version and I welcome docstrings explaining differences and related lemmas.

[Damiano Testa]

As for the nolints, it would be great if docstrings were added, but I view it as "these lemmas should have a docstring, but sadly they do not have one".

[Eric Wieser]

Perhaps Foo.bar_baz' should be automatically allowed if Foo.baz' exists / is mentioned in the statement?

[Violeta Hernández]

Thinking about it a bit more, I agree with at least the conditionally complete lattice lemmas that they should each document how they differ from their unprimed versions. I'll get to that at some point.

[Damiano Testa]

A heads up to everyone: the linter is now active!

[Damiano Testa]

As mentioned elsewhere, it is "hard" to silence it, unless you add a docstring. Hopefully this will encourage people to write good explanations for their primes!

[Damiano Testa]

Should it be really obnoxious, let me know and we'll come up with better solutions.

[Kim Morrison]

It just complained to me about a double primed lemma on nightly-testing, and eventually I realised the correct solution was to delete the lemma and replace its use with the unprimed version. :-) Feels like a win to me!

[Damiano Testa]

Avoiding primes or adding documentation are definitely wins!

[Damiano Testa]

There is a potential issue raised in this thread: it could be the project downstream of mathlib that do not get the cache from Mathlib, but build it locally may trigger the linter.

[Damiano Testa]

I do not understand how project-options work in detail to even know if this is a possible issue or not.

[Damiano Testa]

If it is, would it be a good idea to preemptively add to the nolint file all primed lemmas in mathlib dependencies to prevent this?

[Jon Eugster]

Maybe the linter should only look at things in the Mathlib. namespace then? or at least exclude anything that's in Lean, Std, Batteries, etc...

I dont see this linter being super useful outside mathlib, so I think the first could be a valid option and more robust

[Jon Eugster]

(or defined in mathlib, Mathlib. doesnt even exist consistently does it?)

[Kim Morrison]

@Damiano Testa, can we modify the linter so it doesn't require doc-strings when the prime "comes from" another declaration? In this case mk' definitely needs a doc-string, but then coe_mk' doesn't.

[Kim Morrison]

Mac Malone said:

My suggestion would be to add the no lint files as a target (via inputTextFile) and an extraDepTargets of the relevant libaries (or the whole package). For example, something like this:

Presumably this can't be translated to a toml, so lets find another solution here.

[Damiano Testa]

I am aware that the linter is hard to silence without adding a doc-string. The idea is that the linter should make you prefer to add a doc-string, rather than increase the nolints file. For this reason, I would like to think hard about making it easier to increase the nolints file.

[Damiano Testa]

A cheap way of silencing the linter after you extended the nolints file, is to add another modification to the file where the nolint was found (or earlier), as that would trigger recompilation, rather than replay.

[Damiano Testa]

Having said that, I'll think about Kim's suggestion: I agree that just having a ' at the end may not be enough to justify a doc-string, so making the linter's logic a bit more elaborate is my preference.

[Damiano Testa]

Btw, the idea of not linting when a ' "comes from" another declaration, is the reason why the linter only looks at terminal ', rather than all of them.

[Damiano Testa]

Btw, this is the thread with the discussion of the linter and the awkwardness of silencing it.

[Damiano Testa]

Does allowing declarations that end in _mk' seem reasonable?

[Damiano Testa]

It "fixes" the current issue and allows the removal of 126 nolints.

[Damiano Testa]

Another suggestion would be to inspect the constants ending in ' that are "visible" in the declaration and if one of them is not linted (either because of a doc-string or because it is in the nolints file), then ignore the current one as well.

[Damiano Testa]

I have not thought a lot about whether this would exclude declarations for which you would really like a doc-string: this does not check that it comes from the other, just that it uses the other.

[Bhavik Mehta]

Damiano Testa said:

I have not thought a lot about whether this would exclude declarations for which you would really like a doc-string: this does not check that it comes from the other, just that it uses the other.

I'd guess it's not too hard to make it approximate this - the constant identified must be terminal in the current name?

[Damiano Testa]

So you are saying the if x.y' is no-linted, then x.y_mk' should also not be linted? Possibly generalizing also over mk?

[Bhavik Mehta]

Oh, that's not what I meant and now I realise I misunderstood what you were saying. My mistake, sorry for the noise

[Yaël Dillies]

Could be disable linter.docPrime on private declarations?

[Eric Wieser]

This example should be fixed by locally disabling the linter, not adding to nolints, right?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I changed the nolints because other declarations in the same file were listed there rather than locally silenced with set_option. That would also work, but it should probably be done consistently?

[Eric Wieser]

I think the rule is that nolints contains everything that still needed to be dealt with when the linter is created (the author of the linter shouldn't necessarily be burdened with fixing all existing code first), and set_option is for when the correct thing to do is silence the linter.

[Jireh Loreaux]

I don't like this linter (sorry Damiano!), I just didn't comment on the relevant thread in time to voice my objection.

[Damiano Testa]

It's ok not to like stuff, no worries! Do you not like at all the idea of documenting primed declarations, or is it just how this is implemented?

[Jireh Loreaux]

I don't like the idea of forcing documentation of primed declarations, as I think there are too many situations where it just doesn't make sense / isn't needed. The above example I think is the most obvious case of this, but I also think it's not necessary for many other primed declarations, and the ones for which it is necessary generally already get docstrings detailing the difference. (But I was grossly outvoted in the other thread, so perhaps my opinion shouldn't matter much.)

[Damiano Testa]

I certainly agree that documenting all primed declarations is excessive. I am also happy when I find a doc-string on a primed declaration that explains the difference with the unprimed twin and that there have been cases where there was no such doc-string.

[Damiano Testa]

I think that the "success" of this linter depends on being able to find a good heuristic for when to flag a declaration, though, I also completely agree that flagging everything is not (yet) the good heuristic! :smile:

[Damiano Testa]

With respect to the poll, I would not necessarily give it much weight: one thing is to agree with the idea of something, another thing is to actually see it in action. I do think that experimenting a little with automatic exclusions might yield an overall improvement.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

This is an important discussion to have, but I intended this thread to be about Lake caching rather than the merits of any specific linter. Would an admin be able to split off the linter discussion into a separate thread?

[Damiano Testa]

... and actually moving it to the docPrime thread?

[Damiano Testa]

#mathlib4 > theorem names with primes?

[Notification Bot]

26 messages were moved here from #mathlib4 > Caching of lints by Yaël Dillies.

[Damiano Testa]

Yaël Dillies said:

Could be disable linter.docPrime on private declarations?

Yaël: #17361.

[Damiano Testa]

I also realize that maybe the linter does not have support for continuing, but this change was so simple that I simply went ahead and did it! :smile:

[Violeta Hernández]

Damiano Testa said:

Does allowing declarations that end in _mk' seem reasonable?

This would be really nice. There's a few misnamed lemmas on docs#aleph' like docs#aleph'_cof that should really end in aleph', but I can't fix them without triggering the linter.

[Violeta Hernández]

I'm also working on introducing a function omega', and the linter is getting in my way

[Violeta Hernández]

The docs for aleph' already explain the difference with aleph, I shouldn't have to repeat this explanation for every single lemma on it that happens to trigger the linter...

[Yaël Dillies]

Violeta Hernández said:

Damiano Testa said:

Does allowing declarations that end in _mk' seem reasonable?

This would be really nice. There's a few misnamed lemmas on docs#aleph' like docs#aleph'_cof that should really end in aleph', but I can't fix them without triggering the linter.

You are allowed to edit no_lints_prime.txt!

[Sébastien Gouëzel]

You are also allowed to add a docstring :-). The goal is that it should be easier to add a docstring than to fix the nolint file -- because more docstrings is always good.

[Yaël Dillies]

Yes but docstrings shouldn't be added during unrelated refactors.

1. That's scope-creep
2. That's the recipe for low-quality docstrings

[Sébastien Gouëzel]

I definitely don't count docstrings as scope-creep. And I trust people to add good docstrings.

[Eric Wieser]

Yaël Dillies said:

You are allowed to edit no_lints_prime.txt!

Aren't you specifically _not_ supposed to do this, and instead you should use set_option linter.docPrime false in?

[Violeta Hernández]

To give my actual example, say I rename docs#Cardinal.aleph'_isNormal to Cardinal.isNormal_aleph' (I won't since this lemma will get deprecated for irrelevant reasons, but morally I should).

What sort of docstring could I add? "The aleph' function is normal"? What info does this provide that the name or type signature didn't already immediately convey? Should I also add "The aleph function is normal" to docs#Cardinal.aleph_isNormal ?

[Eric Wieser]

Eric Wieser said:

Perhaps Foo.bar_baz' should be automatically allowed if Foo.baz' exists / is mentioned in the statement?

You're asking for this feature, right?

[Violeta Hernández]

Yep

[Violeta Hernández]

I guess another alternative might be to rename docs#Cardinal.aleph', but I have no idea how to do this

[Violeta Hernández]

"the aleph function except we also enumerate the finite cardinals" doesn't really have a name in literature and isn't very easy to condense. In my view, the docstring already gets the point across.

[Heather Macbeth]

How is it possible that #18917 passed CI, given that it removed docs#div_le_div_iff' from the nolints list, but doesn't seem to have added a docstring to that lemma?

[Heather Macbeth]

(I'm curious because this change -- now merged to master -- seems to be making #19262 fail.)

[Damiano Testa]

Yes, I am also investigating this, as I have also been affected...

[Damiano Testa]

I suspect that this is the same mechanism that makes silencing the linter annoying without touching the file with the exception or something earlier than it: modifying the no_lints file for the linter does not trigger a re-build. So lake will replay the noiseless file, even though if it recompiled it, it would be noisy.

[Damiano Testa]

I imagine that if the only change that a PR did was removing the no_lints file, CI would pass for that PR, as there would be no build, just replay. However, after that, every modification in a file that contains or is followed by a file with a docPrime extension would trigger the linter.

[Eric Wieser]

We should be adding no_lints as a dependency of the mathlib library in the lakefile

[Damiano Testa]

I've readded the primed lemma to the no_lints file and I am rebuilding everything: #19267.

[Damiano Testa]

Eric Wieser said:

We should be adding no_lints as a dependency of the mathlib library in the lakefile

I agree: I knew that it was hard to silence the linter, so that was an incentive to not add exceptions to the no_lints and actually add doc-strings. However, I had not realized until now that there was the possibility of someone removing a still existing lemma from the no_lints file!

[Eric Wieser]

Wait, I'm confused again; does any lean code actually read the no_lints file?

[Damiano Testa]

Yes, the docPrime linter.

[Eric Wieser]

Oh, nolints-style.txt not nolints.json

[Damiano Testa]

https://github.com/leanprover-community/mathlib4/blob/25b91b6001b15abdba13e10b8dcf838cfe9d292f/Mathlib/Tactic/Linter/DocPrime.lean#L67

[Damiano Testa]

Actually, scripts/no_lints_prime_decls.txt.

[Eric Wieser]

Ouch, can we not have a single nolints file?

[Eric Wieser]

Or at least, decide whether it is nolints or no_lints

[Damiano Testa]

Given how short scripts/nolints-style.txt is, I think that simply appending the content of scripts/no_lints_prime_decls.txt to that file and aiming the linter there would work.

[Eric Wieser]

Eric Wieser said:

We should be adding no_lints as a dependency of the mathlib library in the lakefile

#19275 does this

[Damiano Testa]

I delegated it, since this has been causing issues for a while and I am no longer convinced that it is working as intended anyway! :smile:

[Damiano Testa]

You'll probably have to re-add the lemma...

[Damiano Testa]

With the lemma added back to the no_lints file, rebuilding all of mathlib no longer gives a warning. So, hopefully, Eric's PR will then solve these issues.

[Violeta Hernández]

Off-topic, but in the weeks since we started enforcing this I've become more and more in favor of the change. Most of the primed lemmas in the files I frequent turned out to just be bad API.

[Heather Macbeth]

Heather Macbeth said:

How is it possible that #18917 passed CI, given that it removed docs#div_le_div_iff' from the nolints list, but doesn't seem to have added a docstring to that lemma?

Looks like @Kim Morrison silenced this in #19279 by adding a set_option linter.docPrime false to that declaration. I would have thought the right move here was to add it back to the nolints list, do I misunderstand the system?

[Damiano Testa]

Ah, that explains how the linter was silent, the declaration was present and the no_lints file had not been touched! I would also agree that the name should be in the no_lints file.

[Heather Macbeth]

#19309

[Eric Wieser]

Heather Macbeth said:

do I misunderstand the system?

• set_option linter.docPrime false in is for "I assert that this lint violation is deliberate (and the reviewers agree it is ok)"
• nolints is for "I do not want to deal with this right now".

[Eric Wieser]

Given the file is full of primes, it does look like the second case

[Kim Morrison]

It's unfortunate that the ease of use of the two mechanisms is reversed -- I really didn't want to deal with this right now, as I was just doing a dependency bump, and the easiest thing to reach for was set_option. Thanks for cleaning up my mess...

[Yaël Dillies]

Eric Wieser said:

Given the file is full of primes, it does look like the second case

Actually I would say we are in the first case here :thinking: