Documenting `Scope`

Stream: lean4

[Michael Rothgang]

There's an in-progress mathlib linter (#14378) which warns when a section or namespace is not closed at the end of the current file. Reviewing the implementation, I found that Scope is mostly undocumented. Would a PR adding documentation be welcome?

Is the following roughly correct? Let me know if you have any corrections, or if some of this is an implementation detail you prefer not to mention or guarantee.

[Michael Rothgang]

/--
A `Scope` gathers context information which is inherently scoped: this contains
the current namespace and information about `open`, `universe` or `variable` declarations.
There is always a base scope; scopes can be nested.

`universe`, `open` and `variable` declarations only modify the current scope
(and all scopes nested below it): these declarations usually *append* to the context in the current scope; `variable` statements can also change existing items.
(xxx Is shadowing possible? If so, this should be reworded.)
Unclosed scopes are automatically closed at the end of the current module.
-/
structure Scope where
  header        : String
  opts          : Options := {}
  /-- The current namespace: by default, this is an anonymous namespace -/
  currNamespace : Name := Name.anonymous
  /-- All currently `open`ed namespaces
  openDecls     : List OpenDecl := []
  /-- All universe levels declared in the current scope -/
  levelNames    : List Name := []
  /-- All variable binders in the current scope -/
  varDecls      : Array (TSyntax ``Parser.Term.bracketedBinder) := #[]
  /-- Globally unique internal identifiers for the `varDecls` -/
  varUIds       : Array Name := #[]
  /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
  isNoncomputable : Bool := false
  deriving Inhabited

[Michael Rothgang]

Some other details I found worth documenting

• the base scope is always the last one in getScopes
• noncomputability is inherited: scopes below a noncomputable scope remain noncomputable

If there are not implementation details, I can also document them.

[Michael Rothgang]

I didn't find anybody listed in CODEOWNERS for Lean/Elab/Command. @Sebastian Ullrich You made most recent changes to this module; would you like to comment? Should I ask somebody else instead?

[Filippo A. E. Nuccio]

Michael Rothgang said:

/--
A Scope gathers context information which is inherently scoped: this contains
the current namespace and information about open, universe or variable declarations.
There is always a base scope; scopes can be nested.

universe, open and variable declarations only modify the current scope
(and all scopes nested below it), by appending to it. (Is shadowing possible? If so, this should be reworded.)
Unclosed scopes are automatically closed at the end of the current module.
-/
structure Scope where
header : String
opts : Options := {}
/-- The current namespace: by default, this is an anonymous namespace -/
currNamespace : Name := Name.anonymous
/-- All currently opened namespaces
openDecls : List OpenDecl := []
/-- All universe levels declared in the current scope -/
levelNames : List Name := []
/-- All variable binders in the current scope -/
varDecls : Array (TSyntax `Parser.Term.bracketedBinder) := #[] /-- Globally unique internal identifiers for the varDecls -/ varUIds : Array Name := #[] /-- noncomputable sections automatically add the noncomputable` modifier to any declaration we cannot generate code for. -/
isNoncomputable : Bool := false
deriving Inhabited

Thanks! I find this documentation very useful and well-done, so I'd be all in favour to adding it. Perhaps the sentence "...only modify the current scope (...) by appending to it" can be clarified a bit more?

[Michael Rothgang]

Filippo A. E. Nuccio said:

Michael Rothgang said:

/--
A Scope gathers context information which is inherently scoped: this contains
the current namespace and information about open, universe or variable declarations.
There is always a base scope; scopes can be nested.

universe, open and variable declarations only modify the current scope
(and all scopes nested below it), by appending to it. (Is shadowing possible? If so, this should be reworded.)
Unclosed scopes are automatically closed at the end of the current module.
-/
structure Scope where
header : String
opts : Options := {}
/-- The current namespace: by default, this is an anonymous namespace -/
currNamespace : Name := Name.anonymous
/-- All currently opened namespaces
openDecls : List OpenDecl := []
/-- All universe levels declared in the current scope -/
levelNames : List Name := []
/-- All variable binders in the current scope -/
varDecls : Array (TSyntax `Parser.Term.bracketedBinder) := #[] /-- Globally unique internal identifiers for the varDecls -/ varUIds : Array Name := #[] /-- noncomputable sections automatically add the noncomputable` modifier to any declaration we cannot generate code for. -/
isNoncomputable : Bool := false
deriving Inhabited

Thanks! I find this documentation very useful and well-done, so I'd be all in favour to adding it. Perhaps the sentence "...only modify the current scope (...) by appending to it" can be clarified a bit more?

I edited that sentence, hopefully it's clearer now.

[Kyle Miller]

@Michael Rothgang If you create a Lean PR and ping me, I'll fact check it carefully and make sure it gets in. We're happy to receive high-quality docstring PRs!

[Michael Rothgang]

@Kyle Miller Thank you for the encouragement! I just submitted lean#4748 with this change.

[Kim Morrison]

lean#4748