fix: pin shared-package workspaces with the root lake manifest

[kim-em]

This PR makes scripts/evaluate_submission.py copy the benchmark checkout's root lake-manifest.json into each per-submission workspace whose .lake/packages is symlinked to the shared lean-eval/.lake/packages, instead of running lake update and lake exe cache get there, and makes the evaluation workflows download TauCeti's build outputs instead of compiling them. Running lake update against the shared directory can re-resolve transitive dependencies and check out different revisions inside it, corrupting the tree for every other workspace and for the benchmark root; the root manifest already pins every package any generated workspace requires, and Lake ignores entries a workspace does not require. This matches what lean-eval's own CI and reuseRootPackages do, and is needed for leanprover/lean-eval#649 (feat: add the classification of finite simple groups to v2), whose workspace requires TauCeti as well as Mathlib.

Because Lake only warns when a require's rev differs from the manifest and then uses the manifest, the copy is refused unless every [[require]] of the workspace's lakefile.toml is a git require whose name, URL (up to a trailing .git), rev and subDir match the root manifest's entry, and unless the workspace's lean-toolchain equals the root's (a different toolchain would recompile every shared dependency inside the sandbox). Either mismatch fails the evaluation with an error naming it, so stale generated workspaces are caught before anything is scored.

In submission.yml and public-replay-smoke.yml, lean-action no longer builds the benchmark root. A trusted step runs the new scripts/build_benchmark_root.py lean-eval instead. For a benchmark whose manifest pins TauCeti it requires scripts/fetch_dependency_caches.sh (added by leanprover/lean-eval#650, chore: download TauCeti's build outputs instead of compiling them), runs it without $GITHUB_ENV so the Lake cache settings stay inside that step, then runs lake build TauCeti (the whole library, so a submission may import any TauCeti module) and lake build with LAKE_RESTORE_ARTIFACTS=true. Every downloaded output is copied into the shared package build directories, and the first Built TauCeti... line stops the build and fails it, so a cache miss is an error rather than a silent compile. Later workspace builds, including comparator's sandboxed build (whose environment is reduced to PATH, HOME and LEAN_ABORT_ON_PANIC), find TauCeti up to date and need neither the artifact cache nor the network. Benchmarks that pin no TauCeti get a plain lake build as before. lake exe cache get is dropped on the shared workspace path because Mathlib's decompressed cache also lives in the shared tree, which lean-action primes at the root.

The manifest comes only from --repo-root (the trusted benchmark checkout). Submitter content is still limited to Submission.lean and Submission/**/*.lean, so a submission cannot supply a lake-manifest.json, and a missing, non-regular or symlinked root manifest fails closed. Workspaces that do not share packages (including when sharing fails) keep the existing lake update + lake exe cache get priming, and --preprimed-workspaces replays keep their baked manifests.

🤖 Prepared with Claude Code