refactor: remove embedded generator core

[kim-em]

Summary

Remove the duplicated ~4,200-line generator core from LeanEval and make the four EvalTools compatibility modules thin imports of the standalone lean-eval-generator package.

• pin exact merged standalone generator main commit 77373a539b31f8f304c852f288d7d8469cceebff;
• keep the EvalTools import surface for existing problem modules and callers;
• preserve the trusted environment behind EvalTools.Markers without exposing the generator package to generated workspaces;
• update remaining consumer namespaces explicitly; and
• regenerate the Annals workspaces affected by active option preservation.

Generator PRs #1, #2, and #3 are merged. This consumer is now pinned to their final main-branch result.

Verification

Current consumer head: 98c7da8.

• lake build test_generate test_module_coverage lean-eval;
• generator regression suite: 136/136;
• module-coverage suite: 19/19;
• Python catalog/selection suite: 28/28;
• theorem-hole and definition-hole byte parity: 10/10 files each;
• previous hosted eight-shard/corpus run 32551999841 was fully green; and
• fresh hosted checks are running against the final exact generator pin.

No project linter warnings were introduced.

[kim-em]

Hosted CI is fully green at consumer head 305da307 (run 32549264988): repository checks, security/scoring smoke, all eight catalog-validation shards, manifest inventory aggregate, and final verify passed. The PR remains draft because generator #3 still needs independent approval and its final merged-main SHA; the local unsharded generated-catalog check continues in parallel.

[kim-em]

Full unsharded validation follow-up:

• lake exe lean-eval generate --check traversed the complete corpus and found one coherent stale-output class: 34 Annals problems (102 generated Challenge.lean, Solution.lean, and Submission.lean files) were missing the standalone generator's preserved set_option autoImplicit false.
• Regenerated all 50 Annals workspaces with the PR's pinned standalone generator. The resulting diff is mechanical: 102 set_option autoImplicit false insertions plus surrounding blank lines, with no removals or unrelated output changes.
• Re-ran lake exe lean-eval generate --check --problem <id> for every one of the 50 Annals problems: all reported up to date.
• git diff --check is clean.

The generated-output fix is commit 1ed9b18; hosted corpus CI is rerunning on that head. This does not change the dependency gate: the PR remains draft until the standalone generator sequence is independently reviewed/merged and this consumer is pinned to the final main SHA.

[kim-em]

Hosted validation is now fully green on 1ed9b18 (run 32551999841): repository checks, security/scoring smoke, all 8 catalog shards, manifest inventory aggregate, and final workflow conclusion all succeeded. Together with the targeted freshness checks for all 50 Annals workspaces, this closes the stale-output discrepancy found by the unsharded run. The PR remains draft for the independent standalone-generator review/merge and final main SHA pin.