I'm not sure why there is not a test file @jcommelin

I'd like to see a plan for one first

bors r-

Canceled.

@mattrobball You can see in these search results plenty of occurrences (in 206 files) of using example locally to showcase what the instances can do. Are the examples in this PR really that special or important to warrant that they be put in a separate test file?

Yes, there are existing uses as such but we have already seen that often hide undesirable behavior and are often poorly motivated. I think they should all be moved/removed (and some have) but that is out of scope here. Inclusion of new examples should meet a higher bar for justification.

My rationale: Most of the examples I've seen are to demonstrate that instance synthesis succeeds. However, success is highly dependent on the imports. For the end user, who most likely will be working with additional imports, examples declared directly after the relevant instance declaration in the original file will not serve as a guarantee their code works as expected. For mathematically well-motived instances (as this one definitely is), we want to lock in that success of type class search throughout the whole library. This can only be done when all available instances are in scope.

Additionally, since examples add nothing to the environment they confuse anything, like a linter, that uses the environment. We don't want to keep adding to noshake.json for each of them, for example. (This is not the case here but still.)

TLDR: yes these instances searches are of sufficient importance that we want to make sure they keep working indefinitely. We also want to model best practices going forward.

I appreciate your patience with me. I think the request is important enough relative to the effort required. Please let me know if there is anything I can do to help.

Thanks for the explanation. I'll add the tests in test/instances. Though I still have some doubts: it's possible that when importing the whole Mathlib, a declared instance itself may fail to synthesize (it might timeout, or fail due to some bad non-defeq instance introduced in between). Does it mean we should add every instance to the tests? Or is CI already checking every instance can be synthesized after importing Mathlib, somewhat like what the simpNF linter is doing to every simp lemma?

There is no such check. I think we should do this mainly for mathematically-important instances.

If it fails with import Mathlib, then we can postpone and merge as is. But hopefully that is not the case.

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style