RFC: No implicit sections in `$cmd in $cmd` and non-atomic declaration names

The current implementation of command-scoped options (set_option … in $cmd) and declarations with non-atomic names (def Foo.a := …) are by expansion to section; set_option …; $cmd end resp. namespace Foo; def a := …; end. This implicit opening and closing of section causes unexpected interaction with other feature, in particular local attributes (@[local foo]), so that in

set_option linter.unusedVariable false in
@[local grind] theorem foo := …

or

@[local grind] theorem Foo.bar := …

the attribute would not be visible afterwards.

Proposal

This regularly and understandably confuses users. Therefore it seems desirable to avoid this footgun:

• set_option $opt $val in $cmd
  

  should set the option before elaborating the command, and reset it to the value it it had before afterwards, but otherwise not reset other parts of the environment.

• Same for open Namespace in …

• theorem Foo.bar := …
  

  should open the namespace Foo during elaboration of the command, as now, but not using the namespace command which also acts like a section.

• For recursive declarations, the waters are quite muddy.

  It seems that a namespace command is introduced only for the common prefix of names in the mutual group. So mutual def Foo.a := … ; def Bar.a := … will not open the namespace for Foo or Bar. Users would expect that the appropriate namespace is opened during elaboration of each of the commands. Maybe implementing this RFC will require a refactoring that makes this possible.

  It also seems that a mutual … end block produces an implicit section block whenever one of these commands appear in it:

  private def isMutualPreambleCommand (stx : Syntax) : Bool :=
    let k := stx.getKind
    k == ``Lean.Parser.Command.variable ||
    k == ``Lean.Parser.Command.universe ||
    k == ``Lean.Parser.Command.check ||
    k == ``Lean.Parser.Command.set_option ||
    k == ``Lean.Parser.Command.open
  

  Fixing this implicit section is probably harder.

• Lean actually allows arbitrary $cmd in $cmd, for example

  example : True := by simp in
  @[local simp] axiom a : A ↔ True 
  

  This is sometimes silly (as in this case) and sometimes used for good effect (as in variable … in …).

  This is again hard to address. Most plausible by identifying all commands that make sense to be combined with in and implementing them without section.

Hmm, maybe this needs more thought than I thought when I started writing this. Too bad that there are no “draft issues”

Smaller proposal

Given the complexity, it would already be helpful to fix this for non-atomic declaration names only, and leave the issue around in for later.

Maybe the elaboration of the … in … variants could elaborate to a form of section that remembers that was implicit, so that local $attrib can at least warn about that it is less effective than it looks like. This might be good enough to avoid most of the frustration.

MWE

axiom A : Prop

@[simp] def Foo.T := True
@[simp] def Bar.T := True

namespace ex0
@[local simp] axiom a : A ↔ True 
example : A := by simp
end ex0

namespace ex1
set_option linter.unusedVariables false in
@[local simp] axiom a : A ↔ True 
example : A := by simp -- fails
end ex1

namespace ex2
open Nat in
@[local simp] axiom a : A ↔ True 
example : A := by simp -- fails
end ex2

namespace ex3
@[local simp] axiom Foo.a : A ↔ True
example : A := by simp -- fails
end ex3

namespace ex4
@[local simp] axiom _root_.Foo.a : A ↔ True
example : A := by simp -- works??
end ex4

namespace ex5
mutual
@[local simp] theorem Foo.a : A ↔ True := sorry
end
example : A := by simp -- fails
end ex5

namespace ex6
mutual
@[local simp] theorem a : A ↔ True := sorry
end
example : A := by simp -- works
end ex6

namespace ex7
mutual
open Nat
@[local simp] theorem a : A ↔ True := sorry
end
example : A := by simp -- fails
end ex7

namespace ex8
mutual
@[local simp] theorem Foo.a : A ↔ True := sorry
theorem Bar.b : A ↔ True := sorry
end
example : A := by simp -- works (no common namespace)
end ex8

namespace ex9
example : True := by simp in
@[local simp] axiom a : A ↔ True 
example : A := by simp -- fails
end ex9

Work-around

Until this is implemented, a work-around can be

theorem Foo.bar := …
attribute [local grind]  Foo.bar

or, it seems,

@[local grind] theorem _root_.Foo.bar := …

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reproducing the MWE, especially the set_option … in …, open … in …, non-atomic declaration, and mutual cases. Read the command elaboration paths and the shown isMutualPreambleCommand logic; done means the proposed forms preserve local attributes without unintended implicit sections, including the smaller non-atomic-name proposal.