fix(generate): skip leading copyright block in import prelude

[BoltonBailey]

Disclaimer: Claude identified this as an issue as I was asking it to assemble another PR, which included files with both copyright headers and definitional dependencies to the main theorem. I asked Claude to write and PR this fix - it wrote it itself but I have checked it over and it looks OK to me.

Claude's description of the problem below:

---

Problem

generate produces a standalone, Mathlib-only workspace per problem. When a problem has a same-module helper declaration (a non-hole dependency), the helper is factored into ChallengeDeps.lean. That file must not import EvalTools.Markers (which doesn't exist in the standalone workspace).

For source files that use Mathlib's copyright-block-then-imports layout, the generated ChallengeDeps.lean instead retained the copyright block and import EvalTools.Markers, so the workspace failed to build:

error: unknown module prefix 'EvalTools'

Root cause

importPreludeLength only consumed leading import/blank lines, so a leading /- … -/ copyright block made it return 0. renderChallengeDepsCore then sliced the body from offset 0, and on the kept-declarations path (which, unlike the local-imports path, never calls stripProblemMarkers) the copyright block and import EvalTools.Markers were copied verbatim into the output.

This only bites problems that are both copyright-first and have a non-hole same-module dependency (so a ChallengeDeps.lean is generated at all). Import-first problems are unaffected, which is why it went unnoticed.

Fix

Teach importPreludeLength to skip a leading block comment that precedes the first import (nesting-aware), treating the copyright header as part of the prelude. Comments appearing after an import are left untouched, so import-first files generate byte-identically.

Verification

• Builds cleanly.
• lake exe lean-eval generate --check reports no changes to the committed (import-first) problems → no regression.
• Regenerating a copyright-first problem (anderson_theorem) now yields a clean ChallengeDeps.lean starting with import Mathlib / namespace AndersonTheorem, with no EvalTools import.

🤖 Generated with Claude Code