Extractor mis-handles `open … in` inside definitions, emitting dangling `open` lines in generated files

[kim-em]

Problem

When a problem module uses open … in attached to a definition (e.g. open Classical in on a def body), lake exe lean-eval generate collects those open … in lines and emits them into the generated Challenge.lean / Submission.lean as standalone lines — open Classical in with nothing following it. That is a syntax error, and it cascades into confusing downstream errors such as Missing name after 'end'.

Repro

A problem module of the form:

namespace LeanEval.Algebra
open Polynomial

noncomputable def sturmAux : ℝ[X] → ℝ[X] → ℕ → List ℝ[X]
  | a, _, 0       => [a]
  | a, b, (n + 1) =>
    open Classical in
    if b = 0 then [a] else a :: sturmAux b (-(a % b)) n

noncomputable def signChanges (xs : List ℝ) : ℕ :=
  open Classical in
  ...

builds fine as a source module, but the generated Submission.lean begins:

open LeanEval.Algebra
open Polynomial
    open Classical in
  open Classical in

namespace Submission
...

CI fails with:

error: Submission.lean:7:17: Missing name after `end`: Expected the current scope name `Submission`

Seen on PR #273 (the sturm problem).

Workaround

Use a file-level open scoped Classical (a standalone open command with no in) instead of per-definition open … in.

Suggested fix

The extractor should only collect top-level open commands, and should not copy the in-scoped form (open … in) at all — or, if it does, it must keep the in attached to the command it scopes rather than emitting it as a dangling line.