unscoped notations

Stream: mathlib4

[Chris Henson]

Motivated by recent threads about notation scopes, I wrote the below code to check how many unscoped notations Mathlib introduces. Let me know if there are any flaws in this logic, but by this count it is 147. (The code prints each notation name and the module that defines it.)

My questions on this:

• Previous discussion has seemed to converge on placing notations in appropriately narrow scopes to avoid conflicts. Are there any exceptions that should remain in the top-level namespace?
• Would PRs scoping some of these (for me motivated by notation conflicts in CSlib) be welcome?
• If consensus is that usually scoped notations are best, could this be included in the technical debt metrics script?

import Mathlib

open Lean

run_meta
  let env ← getEnv
  let unscopedNotations : List (Name × Name) :=
    env.constants.toList.filterMap (fun (name,cinfo) => do
      let isNotation := cinfo.type.isConstOf ``Lean.TrailingParserDescr
      let isAnon := name.getPrefix.isAnonymous
      if isNotation && isAnon then
        let idx ← env.getModuleIdxFor? name
        let module ← env.allImportedModuleNames[idx]?
        if module.getRoot == `Mathlib then
          return (name, module)
        else
          none
      else
        none
    )
  println! unscopedNotations.length
  for n in unscopedNotations do
    println! n

[Christian Merten]

As long as docgen does not use scoped notations, we should not generally scope all notations. Prominent examples include set notation (image, preimage etc.) and big operators (which were intentionally unscoped some time ago).

[Michael Rothgang]

How difficult is it to make docgen use scoped notations (for instance, looking for the list of opens in a file and using those)?

[Christian Merten]

There exists a thread for this on Zulip (on mobile right now, so can’t find the link). IIRC, it depends on a core RFC.

[Chris Henson]

Here is a previous thread: #general > docgen scoped notations

lean4#6050 is the RFC to keep track of what namespaces are open when a declaration is added

[Chris Henson]

I had seen that thread before and it slipped my mind while writing this, sorry! I suppose with that context, there is not much that can be done at the moment (except reacting to that RFC for visibility!). Every scoping of notation is at the moment forced to be a tradeoff between documentation readability and downstream conflicts.

[Chris Henson]

Maybe this portion is more relevant to another channel, but note how this especially conflicts with the advice given to downstream libraries. In CSlib for instance we have taken seriously the idea that all new declarations should be namespaced to the extent that I have written an environment linter to enforce that we not not create any new top-level declarations or namespaces (besides Cslib). This means that almost all of our notations are scoped and not printed in our docs.