leanprover · kim-em · May 19, 2026 · May 19, 2026 · May 19, 2026
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -167,6 +167,9 @@ jobs:
       - name: Run Submission Policy Tests
         run: lake exe test_validate_submission
 
+      - name: Run Generate Tests
+        run: lake exe test_generate
+
       - name: Run Leaderboard Update Tests
         run: python -m unittest tests.test_update_leaderboard
 

diff --git a/EvalTools/Generate.lean b/EvalTools/Generate.lean
@@ -714,18 +714,72 @@ def Source.findKeywordBasename (s : Source) (keywords : Array String) (basename
 
 /-! ## Context opens -/
 
+/-- Drop block comments `/- … -/` (nested-aware) that open and close on the
+same line. Multi-line block comments are left alone — they're handled by
+peeking through whole comment-only lines in the line scanner. -/
+private def stripSingleLineBlockComments (s : String) : String := Id.run do
+  let chars := s.toList.toArray
+  let n := chars.size
+  let mut out : String := ""
+  let mut i : Nat := 0
+  let mut depth : Nat := 0
+  while i < n do
+    if i + 1 < n && chars[i]! == '/' && chars[i + 1]! == '-' then
+      depth := depth + 1
+      i := i + 2
+    else if depth > 0 && i + 1 < n && chars[i]! == '-' && chars[i + 1]! == '/' then
+      depth := depth - 1
+      i := i + 2
+    else
+      if depth == 0 then out := out.push chars[i]!
+      i := i + 1
+  return out
+
+/-- Drop a trailing `--` line comment from `s`. Used together with
+`stripSingleLineBlockComments` to keep `in` tokens that appear in comments
+from being mistaken for the `open … in` scoping keyword. -/
+private def stripLineComment (s : String) : String :=
+  match s.splitOn "--" with
+  | x :: _ => x
+  | [] => s
+
+/-- True if `stripped` is a scoped `open … in …` line — the single-command
+form that binds an open to one following expression. Detected by an `in`
+token appearing somewhere after the leading `open` keyword. Top-level opens
+like `open Foo` or `open scoped Classical` return false. -/
+def isScopedOpenLine (stripped : String) : Bool := Id.run do
+  if !(stripped.startsWith "open ") then return false
+  let toks := splitWhitespace (stripLineComment (stripSingleLineBlockComments stripped))
+  for i in [1:toks.size] do
+    if toks[i]! == "in" then return true
+  return false
+
+/-- True if the upcoming lines starting at `peekIdx` (0-indexed) form the
+continuation of a scoped `open … in` — that is, after any blank or
+comment-only lines, the next syntactic line is `in` or begins with `in `.
+Used to catch the multi-line variant where `in` is on its own line. -/
+private def followingLineIsScopingIn (lines : Array String) (peekIdx : Nat) : Bool := Id.run do
+  let mut i := peekIdx
+  while i < lines.size do
+    let s := (lines[i]!).trimAscii.toString
+    if s.isEmpty || s.startsWith "--" then
+      i := i + 1
+    else
+      return s == "in" || s.startsWith "in "
+  return false
+
 def extractContextOpens (problemId : String) (sourcePath : System.FilePath)
     (source : String) (extracted? : Option ExtractedTheorem)
     (includeNamespaces : Bool) : IO String := do
   let _ := problemId
   let _ := sourcePath
-  let lines := source.splitOn "\n"
+  let lines := (source.splitOn "\n").toArray
   let targetLine? : Option Nat := extracted?.map fun e => e.startLine
   let mut namespaceStack : Array String := #[]
   let mut openLayers : Array (Array String) := #[#[]]
   let mut inBody := false
   let mut done := false
-  for idx in [1:lines.length + 1] do
+  for idx in [1:lines.size + 1] do
     if done then break
     if let some t := targetLine? then
       if idx ≥ t then break
@@ -760,6 +814,11 @@ def extractContextOpens (problemId : String) (sourcePath : System.FilePath)
         namespaceStack := namespaceStack.pop
         openLayers := openLayers.pop
     else if stripped.startsWith "open " then
+      if isScopedOpenLine stripped then continue
+      -- Multi-line scoped form: `open Foo` on one line, `in <body>` on a
+      -- following (possibly blank/comment-padded) line. Skip the whole
+      -- thing rather than emitting a dangling `open Foo` as top-level.
+      if followingLineIsScopingIn lines idx then continue
       let layerIdx := openLayers.size - 1
       let layer := openLayers[layerIdx]!.push line
       openLayers := openLayers.set! layerIdx layer

diff --git a/lakefile.toml b/lakefile.toml
@@ -41,3 +41,8 @@ root = "EvalToolsTests.ValidateSubmissionTest"
 name = "test_check_comparator_installation"
 srcDir = "tests/lean"
 root = "EvalToolsTests.CheckComparatorInstallationTest"
+
+[[lean_exe]]
+name = "test_generate"
+srcDir = "tests/lean"
+root = "EvalToolsTests.GenerateTest"
diff --git a/tests/lean/EvalToolsTests/GenerateTest.lean b/tests/lean/EvalToolsTests/GenerateTest.lean
@@ -0,0 +1,158 @@
+import EvalTools.Generate
+
+open EvalTools
+
+set_option autoImplicit false
+
+private def assertEq {α : Type} [BEq α] [Repr α] (label : String)
+    (actual expected : α) : Option String :=
+  if actual == expected then none
+  else some s!"{label}: expected {repr expected}, got {repr actual}"
+
+private def check (label : String) (passes fails : IO.Ref Nat)
+    (f : IO (Option String)) : IO Unit := do
+  match ← f.toBaseIO with
+  | .ok none => IO.println s!"PASS: {label}"; passes.modify (· + 1)
+  | .ok (some reason) =>
+      IO.eprintln s!"FAIL: {label} — {reason}"
+      fails.modify (· + 1)
+  | .error err =>
+      IO.eprintln s!"FAIL: {label} — unexpected exception: {err}"
+      fails.modify (· + 1)
+
+def main : IO UInt32 := do
+  let passes ← IO.mkRef 0
+  let fails ← IO.mkRef 0
+
+  check "isScopedOpenLine: open Foo is top-level" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open Foo") false
+
+  check "isScopedOpenLine: open scoped Classical is top-level" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open scoped Classical") false
+
+  check "isScopedOpenLine: open Foo in is scoped" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open Foo in") true
+
+  check "isScopedOpenLine: open Foo in body is scoped" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open Foo in rfl") true
+
+  check "isScopedOpenLine: open scoped Classical in is scoped" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open scoped Classical in") true
+
+  check "isScopedOpenLine: open Foo.In is top-level" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "open Foo.In") false
+
+  check "isScopedOpenLine: non-open line is not scoped" passes fails do
+    pure <| assertEq "scoped" (isScopedOpenLine "theorem foo : True := trivial") false
+
+  -- A trailing `--` comment that happens to contain the word `in` must not
+  -- cause a top-level `open` to be misclassified as scoped.
+  check "isScopedOpenLine: trailing comment with 'in' is not scoped" passes fails do
+    pure <| assertEq "scoped"
+      (isScopedOpenLine "open Foo -- used in later declarations") false
+
+  check "isScopedOpenLine: real scoped open with comment is scoped" passes fails do
+    pure <| assertEq "scoped"
+      (isScopedOpenLine "open Foo in expr -- comment") true
+
+  -- Block comment containing `in` must not trigger a false positive.
+  check "isScopedOpenLine: block comment with 'in' is not scoped" passes fails do
+    pure <| assertEq "scoped"
+      (isScopedOpenLine "open Foo /- mentions in here -/") false
+
+  check "isScopedOpenLine: nested block comment is stripped" passes fails do
+    pure <| assertEq "scoped"
+      (isScopedOpenLine "open Foo /- outer /- inner in -/ still in -/") false
+
+  check "isScopedOpenLine: real scoped open with block comment is scoped" passes fails do
+    pure <| assertEq "scoped"
+      (isScopedOpenLine "open Foo /- note -/ in expr") true
+
+  -- Regression for https://github.com/leanprover/lean-eval/issues/277:
+  -- `open Classical in` inside an earlier def body must not leak into the
+  -- collected context-open block.
+  check "extractContextOpens skips open … in inside def bodies" passes fails do
+    let source :=
+      "import Mathlib\n" ++
+      "namespace LeanEval.Algebra\n" ++
+      "open Polynomial\n" ++
+      "\n" ++
+      "noncomputable def sturmAux : Nat → Nat\n" ++
+      "  | 0       => 0\n" ++
+      "  | (n + 1) =>\n" ++
+      "    open Classical in\n" ++
+      "    if n = 0 then 1 else sturmAux n\n" ++
+      "\n" ++
+      "theorem target : True := trivial\n" ++
+      "end LeanEval.Algebra\n"
+    let extracted : ExtractedTheorem := {
+      declarationName := "LeanEval.Algebra.target"
+      module := "LeanEval.Algebra"
+      startLine := 11, startColumn := 0
+      endLine := 11, endColumn := 30
+      sameModuleDependencies := #[]
+      kind := "theorem"
+    }
+    let block ← extractContextOpens "demo" "demo.lean" source (some extracted)
+      (includeNamespaces := true)
+    -- The block should mention top-level opens but not the scoped `open Classical in`.
+    let hasOpenPolynomial := (block.find? "open Polynomial").isSome
+    let hasOpenClassicalIn := (block.find? "open Classical in").isSome
+    pure <| assertEq "top-level open kept" hasOpenPolynomial true |>.or
+      (assertEq "scoped open dropped" hasOpenClassicalIn false)
+
+  -- Multi-line scoped open: `open Foo` on one line, `in` on the next.
+  -- The whole thing is scoped to one command and must not be hoisted out.
+  check "extractContextOpens skips multi-line open … in" passes fails do
+    let source :=
+      "import Mathlib\n" ++
+      "namespace Demo\n" ++
+      "open Polynomial\n" ++
+      "\n" ++
+      "noncomputable def helper : Nat :=\n" ++
+      "  open Classical\n" ++
+      "    in if 0 = 0 then 1 else 2\n" ++
+      "\n" ++
+      "theorem target : True := trivial\n" ++
+      "end Demo\n"
+    let extracted : ExtractedTheorem := {
+      declarationName := "Demo.target"
+      module := "Demo"
+      startLine := 9, startColumn := 0
+      endLine := 9, endColumn := 30
+      sameModuleDependencies := #[]
+      kind := "theorem"
+    }
+    let block ← extractContextOpens "demo" "demo.lean" source (some extracted)
+      (includeNamespaces := true)
+    let hasOpenPolynomial := (block.find? "open Polynomial").isSome
+    let hasOpenClassical := (block.find? "open Classical").isSome
+    pure <| assertEq "top-level open kept" hasOpenPolynomial true |>.or
+      (assertEq "scoped open (multi-line) dropped" hasOpenClassical false)
+
+  -- A real top-level `open` whose trailing comment mentions `in` must be kept.
+  check "extractContextOpens keeps top-level open with 'in' in comment" passes fails do
+    let source :=
+      "import Mathlib\n" ++
+      "namespace Demo\n" ++
+      "open Polynomial -- used in later declarations\n" ++
+      "\n" ++
+      "theorem target : True := trivial\n" ++
+      "end Demo\n"
+    let extracted : ExtractedTheorem := {
+      declarationName := "Demo.target"
+      module := "Demo"
+      startLine := 5, startColumn := 0
+      endLine := 5, endColumn := 30
+      sameModuleDependencies := #[]
+      kind := "theorem"
+    }
+    let block ← extractContextOpens "demo" "demo.lean" source (some extracted)
+      (includeNamespaces := true)
+    let hasOpenPolynomial := (block.find? "open Polynomial").isSome
+    pure <| assertEq "top-level open with 'in' comment kept" hasOpenPolynomial true
+
+  let passCount ← passes.get
+  let failCount ← fails.get
+  IO.println s!"\n{passCount} passed, {failCount} failed."
+  return if failCount == 0 then 0 else 1