diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 630a941..85aaea2 100644 --- 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 index 6ca13cd..11d4a86 100644 --- 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 ` 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 index 1cade09..4b82e23 100644 --- 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 new file mode 100644 index 0000000..9b70336 --- /dev/null +++ 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