Preserve active options around extracted syntax context

LeanEvalGenerator/Core/Generate.lean

@@ -1244,10 +1244,12 @@ def isScopedOpenLine (stripped : String) : Bool := Id.run do
     if toks[i]! == "in" then return true
   return false
 
-/-- True if `block` is the single-command `<command> … in` form, which binds to
-the declaration following it rather than to the rest of the enclosing section. -/
+/-- True if `block` contains the single-command `<command> … in <declaration>`
+form, which binds to one declaration rather than to the rest of the enclosing
+section. The declaration may begin on the same line as `in` or on a following
+line. -/
 def isScopedCommandBlock (block : String) : Bool :=
-  (commandTokens block).back? == some "in"
+  (commandTokens block).contains "in"
 
 /-- True if the upcoming lines starting at `peekIdx` (0-indexed) form the
 continuation of a scoped `open … in` — that is, after any blank or
@@ -1622,8 +1624,8 @@ def extractContextLocalSyntaxDeclarations (source : String)
     (extracted? : Option ExtractedTheorem) : String :=
   extractScopedCommandBlocksWhere source extracted? isLocalSyntaxContextDeclaration (fun _ => true)
 
-/-- Collect the in-scope `variable` commands together with the
-notation/syntax/macro commands, preserving their source order.
+/-- Collect the in-scope `variable` and unscoped `set_option` commands together
+with the notation/syntax/macro commands, preserving their source order.
 
 Emitting them as two separate blocks reorders them, and the order matters in
 both directions: a notation may mention a variable, as in
@@ -1633,17 +1635,27 @@ both directions: a notation may mention a variable, as in
 
 and a later `variable` may be written using a notation. Emitting the notation
 first made the quotation precheck fail with `Unknown identifier 'd'` and left
-the macro without an elaborator. `syntaxMatches` selects which syntax commands to
-carry, so callers can keep the `local`-only behaviour when the non-local ones
-have already gone into `ChallengeDeps.lean`. -/
+the macro without an elaborator. An active option may likewise be required to
+elaborate a syntax declaration; for example, a set-builder notation can require
+`set_option quotPrecheck false` to precede it. Scoped `set_option ... in`
+commands are excluded because they belong only to their following declaration
+and hoisting them would change the target theorem's environment.
+
+`syntaxMatches` selects which syntax commands to carry, so callers can keep the
+`local`-only behaviour when the non-local ones have already gone into
+`ChallengeDeps.lean`. -/
 def extractContextVariablesAndSyntax (source : String)
     (extracted? : Option ExtractedTheorem) (theoremBinderNames : Array String)
     (syntaxMatches : String → Bool) : String :=
   extractScopedCommandBlocksWhere source extracted?
-    (fun stripped => startsWithKeyword stripped "variable" || syntaxMatches stripped)
+    (fun stripped => startsWithKeyword stripped "variable" ||
+      startsWithKeyword stripped "set_option" || syntaxMatches stripped)
     (fun block =>
-      if startsWithKeyword block.trimAsciiStart.toString "variable" then
+      let stripped := block.trimAsciiStart.toString
+      if startsWithKeyword stripped "variable" then
         !isScopedCommandBlock block && !variableShadowedByTheorem block theoremBinderNames
+      else if startsWithKeyword stripped "set_option" then
+        !isScopedCommandBlock block
       else true)
 
 /-! ## Delegation arguments -/

tests/Context.lean

@@ -0,0 +1,58 @@
+import LeanEvalGenerator.Core.Generate
+
+open LeanEvalGenerator.Core
+
+private def targetAt (line : Nat) : ExtractedTheorem := {
+  declarationName := "Fixture.target"
+  module := "Fixture"
+  startLine := line
+  startColumn := 0
+  endLine := line
+  endColumn := 1
+  sameModuleDependencies := #[]
+  kind := "theorem"
+}
+
+private def expectEq (label actual expected : String) : IO Unit := do
+  unless actual == expected do
+    throw <| IO.userError
+      s!"{label} mismatch\nexpected:\n{repr expected}\nactual:\n{repr actual}"
+
+def main : IO Unit := do
+  let erdosStyle :=
+    "namespace Fixture\nset_option quotPrecheck false\n\n" ++
+    "local notation \"A\" => { x : Nat | x = 0 }\nvariable (n : Nat)\n" ++
+    "theorem target : True := by sorry\nend Fixture\n"
+  expectEq "active set_option order"
+    (extractContextVariablesAndSyntax erdosStyle (some (targetAt 6)) #[]
+      isLocalSyntaxContextDeclaration)
+    ("set_option quotPrecheck false\n" ++
+      "local notation \"A\" => { x : Nat | x = 0 }\n" ++
+      "variable (n : Nat)\n\n")
+
+  let endedSection :=
+    "section Gone\nset_option quotPrecheck false\nlocal notation \"A\" => Nat\n" ++
+    "end Gone\nlocal notation \"B\" => Nat\n" ++
+    "theorem target : True := by sorry\n"
+  expectEq "ended section context"
+    (extractContextVariablesAndSyntax endedSection (some (targetAt 6)) #[]
+      isLocalSyntaxContextDeclaration)
+    "local notation \"B\" => Nat\n\n"
+
+  let declarationScoped :=
+    "set_option pp.universes true in\ndef helper : Nat := 0\n" ++
+    "local notation \"A\" => Nat\ntheorem target : True := by sorry\n"
+  expectEq "declaration-scoped option does not leak"
+    (extractContextVariablesAndSyntax declarationScoped (some (targetAt 4)) #[]
+      isLocalSyntaxContextDeclaration)
+    "local notation \"A\" => Nat\n\n"
+
+  let inlineDeclarationScoped :=
+    "set_option pp.universes true in def helper : Nat := 0\n" ++
+    "local notation \"A\" => Nat\ntheorem target : True := by sorry\n"
+  expectEq "inline declaration-scoped option does not leak"
+    (extractContextVariablesAndSyntax inlineDeclarationScoped (some (targetAt 3)) #[]
+      isLocalSyntaxContextDeclaration)
+    "local notation \"A\" => Nat\n\n"
+
+  IO.println "PASS active set_option context is preserved without scoped-option leakage"

tests/scripts/contract.py

@@ -68,6 +68,11 @@ def assert_rejected(payload: dict[str, object], message: str) -> None:
 
 def main() -> int:
     subprocess.run(["lake", "build"], cwd=ROOT, check=True)
+    subprocess.run(
+        ["lake", "env", "lean", "--run", "tests/Context.lean"],
+        cwd=ROOT,
+        check=True,
+    )
     malformed = invoke("not json")
     assert malformed.returncode == 1
     assert malformed.stdout == ""