fix: synchronize standalone generator with LeanEval

[kim-em]

Summary

Synchronize the standalone generator with fixes already merged in LeanEval,
then layer the two small package fixes on top so the complete downstream
contract is tested together.

• port LeanEval fixes #543, #546, #547, and #550: lexer-aware
  @[eval_problem] removal and block-aware context/open scanning;
• include active set_option preservation from generator PR Preserve active options around extracted syntax context #1;
• include quoted Lean-name path handling from generator PR Fix quoted Lean module path resolution #2;
• reject inline scoped context commands without reverting the newer block
  scanner; and
• use explicit generator schema-version terminology without changing the
  frozen request/response contract.

PRs #1 and #2 remain the small independently reviewable changes. After they
merge, this branch will be synchronized with main so this PR contains only
the LeanEval-to-standalone synchronization.

Current verification

Final combined head: d04b83e63e41f5a08076c569943326f793529333.

• standalone lake build and hosted generator CI pass;
• generator contract, module-path executable, context, Python byte-compilation,
  actionlint, and diff checks pass;
• theorem-hole and definition-hole workspaces remain byte-identical across all
  10 generated files in each fixture;
• downstream LeanEval consumer PR #553 is green across repository checks,
  security/scoring smoke, all eight catalog shards, manifest aggregation, and
  artifact verification at 1ed9b188d7a1c58c51fb06af204429c5acadd3d9;
• the combined downstream corpus builds at the reviewed pins; and
• Formal Conjectures PR #4951 imports, verifies, generates, and compiles all
  FC100 declarations with its hosted audit green at
  2654e42de2026de6cdb248ad5ed0f1c7d659c8fa.

Independent review of PRs #1, #2, and this synchronization remains required
before the generator pin and LeanEval consumer are advanced.

[kim-em]

Downstream verification against exact head 62b38001bff98e4110081261ae7c466183204b60: LeanEval builds the generator consumer targets cleanly; the full generator regression suite passes 136/136, module-coverage suite 19/19, and the compatibility-marker environment regression now passes. The all-problem generated-catalog check is still traversing the 128-problem corpus; I will post its final result separately.

[kim-em]

Terminology-only follow-up d04b83e reserves bare v1/v2 for LeanEval problem sets: prose now says generator schema version 1, while frozen filenames such as request-v1.schema.json remain unchanged. Runtime generator behavior and emitted file bytes are unchanged; package CI is green. The downstream 128-problem check is running against prior head 62b3800, whose executable source is byte-identical apart from this documentation/comment/schema-title update.

[kim-em]

Additional full-corpus consumer evidence: the standalone generator completed an unsharded traversal of the LeanEval corpus. It correctly exposed 34 stale Annals workspaces whose committed outputs predated preservation of set_option autoImplicit false; the consumer PR has now mechanically regenerated those outputs in lean-eval#553 commit 1ed9b18. Per-problem generate --check then passed for all 50 Annals workspaces. This is consistent with the option-preservation coverage in this repository; no additional generator defect was found.