ban `example`

Stream: mathlib4

[Matthew Ballard]

Should we banish all examples to /test?

[Matthew Ballard]

I am seeing too many of that are really tests. I am sure there are other uses though...

[Michael Rothgang]

Can you say more why you would like to do this? I have certainly seen examples in documentation which are really useful (not sure about ones in code).

[Eric Wieser]

I think it's sometimes quite useful to add these tests immediately after the thing they are testing, especially in the context of instance diamonds etc

[Matthew Ballard]

There are some problems with this particular use case:

1. We explicitly have test/instance_diamond.lean for this
2. Too often, we blow up the context in a lower level file just for the example
3. If we leave some arguments as _ that still need synthesis, then changes downstream can break the test. I would argue this is more what we care about.

[Matthew Ballard]

4. These get written inconsistently. Most are rfl tests and should be with_reducible_and_instances rfl. Scattering them across files makes it harder to catch.

[Matthew Ballard]

5. If I want to know which are broken right now, how can I collect the spiritually broken ones?

[Eric Wieser]

Matthew Ballard said:

1. We explicitly have test/instance_diamond.lean for this

This is a bad solution, because it means you have to build every file that could possibly contain an instance diamond before being able to run any of the tests. Probably it would make more sense to split this file into one file per import.

[Matthew Ballard]

There is also folder with that name :)

[Matthew Ballard]

I think no one has finished that

[Yaël Dillies]

I am strongly against banning example from mathlib proper. It's really useful to show how API should be used

[Eric Rodriguez]

Too often, we blow up the context in a lower level file just for the example

What does this mean?

[Johan Commelin]

I suppose it means adding imports to make the example work

[Kim Morrison]

That should definitely be banned. :-)

[Ruben Van de Velde]

At least shake should alert on that, right?

[Kevin Buzzard]

From my #14176:

instance : TopologicalSpace (FiniteAdeleRing R K) :=
  SubmodulesRingBasis.topology (submodulesRingBasis R K)

-- the point of the above: this now works
example : TopologicalRing (FiniteAdeleRing R K) := inferInstance

This used to be a commented-out -- #synth TopologicalRing (FiniteAdeleRing R K) -- the point of the above but a reviewer suggested I change it to example to avoid any regressions. What would you rather I do here? The point is to explain what all the code above just did, for those not familiar with SubmodulesRingBasis (the CommRing instance has been there for a long time, the art was to add a TopologicalSpace instance which made TopologicalRing not a huge chore to prove).

[Yaël Dillies]

I think it makes sense for this to be an example

[Kevin Buzzard]

I only mention it because I'm pretty sure it's the first time I've ever PRed an example and I would have been hard pressed to justify examples in mathlib before I ran into this.

[Damiano Testa]

I think that there are good reasons to have examples in Mathlib, but also that this should be sporadic. If "sporadic" is measured by the fact that you are supposed to add set_option linter.noExamples false in before the example, maybe with a mandatory comment, that seems like a reasonable compromise.

[Damiano Testa]

The linter could even just be triggered on doc-string-less examples. (Like the non-existing one for theorems.)

[Yaël Dillies]

I just don't see the point of banning example, full stop

[Jireh Loreaux]

I'm in favor of example, modulo not blowing up imports.

[Matthew Ballard]

I still haven’t seen a good use of example. If it’s to prevent regression, then it’s a test.

If it’s to demonstrate API use, then it belongs in a doc string where it is discoverable.

[Jireh Loreaux]

Counterpoints:

1. I want to know about my regression when I implement it, not after I build Mathlib and run a test.
2. We don't have Verso in docstrings yet, so they're not interactive the way code is.

[Matthew Ballard]

6. I end up fighting shake because examples don't affect the environment (much). Cf 2

[Damiano Testa]

Matt, you may "like" the following: in Mathlib/Topology/Sheaves/Forget.lean import Mathlib.Algebra.Category.Ring.Limits could be lowered to import Mathlib.Algebra.Category.Ring.Basic, if it were not for the example that concludes the file.

[Matthew Ballard]

I asked GPT who gave a nuanced take

[Damiano Testa]

(Oddly enough, this was the very first file on which I decided to test the min_imports linter and I could not understand why it was failing on Expr information, while getting the Syntax one right...)

[Matthew Ballard]

Damiano Testa said:

Matt, you may "like" the following: in Mathlib/Topology/Sheaves/Forget.lean import Mathlib.Algebra.Category.Ring.Limits could be lowered to import Mathlib.Algebra.Category.Ring.Basic, if it were not for the example that concludes the file.

Is this one noshaken because of this?

[Damiano Testa]

I am not sure...

[Damiano Testa]

"Mathlib.Topology.Sheaves.Forget": ["Mathlib.Algebra.Category.Ring.Limits"],

[Damiano Testa]

There you go, happy now? :smile:

[Ruben Van de Velde]

So we agree this is not allowed? :innocent:

[Matthew Ballard]

I may have come across as absolute but I think this merits cleaning up at the least

[Damiano Testa]

Actually, with the min_imports linter, that gives you incremental import information, you can even lint for that!

[Damiano Testa]

(Sorry, have to go now, but I am really enjoying this conversation! :upside_down: )

[Kevin Buzzard]

Reviews of #14176 welcome :-)

[Damiano Testa]

With the comment before the example, I find this helpful and like it when I find it in code.

[Damiano Testa]

Would requiring no import-bump and a doc-string be a good compromise for having examples in code?

[Kevin Buzzard]

I have no opinion on this, as I already said the suggestion to make it an example came from code review. I'd happily give the example a docstring if examples are allowed docstrings :-) I just didn't want to make it an instance because it would clutter the place up.

[Kyle Miller]

I'm wondering whether it would be better to make examples be private defs/lemmas? A side effect is that they would appear in documentation, which is both good (it helps people know what's supposed to work without reading the code) and bad (it clutters the documentation somewhat).

/-- The above instance makes the following work. -/
private def testTopologicalRingInstance : TopologicalRing (FiniteAdeleRing R K) := inferInstance

[Yaël Dillies]

I thought private defs didn't appear in documentation?

[Kyle Miller]

Ah, so they don't.

[Kyle Miller]

At least this would help with the shake issues with examples though, right?

[Ruben Van de Velde]

Depends on what for mean by "help" - it would no longer flag imports that are only used in those defs as unused, which I'm not sure is a good thing

[Mario Carneiro]

Ruben Van de Velde said:

At least shake should alert on that, right?

Shake actually has several exceptions in noshake.json because of this practice

[Mario Carneiro]

All of them were added as single file exceptions so you can probably find them by deleting all noshakes for files containing example and review the failures

[Matthew Ballard]

When I tried to do a bulk deletion (of the whole file), shake would hang

[Mario Carneiro]

I believe all recent reports of shake hanging are this bug, for which the fix has not yet landed

[Mario Carneiro]

in the current situation shake is very likely to hang if it has to calculate the downstream consequences of any change

[Mario Carneiro]

(I think the fix is still not completely correct, but it should at least restore the structural property needed to ensure termination)

[Matthew Ballard]

Mario Carneiro said:

I believe all recent reports of shake hanging are this bug, for which the fix has not yet landed

It works without a noshake file now.

[Matthew Ballard]

Gist of the output without the noshake file