chore: don't fail on running build bench on built stage3 (#13467)

This PR applies two minor tweaks:
- `tests/bench/sym/simp_1.lean`: share-common the proof term before
counting objects in `getProofSize`, so the reported size reflects the
shared representation.
- `tests/elab/sym_simp_3.lean`: use `>>` instead of `.andThen` when
composing `Sym.Simp` methods.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

.github/workflows/ci.yml

@@ -279,7 +279,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`
                 "test-bench": large && level >= 2,
@@ -291,7 +292,8 @@ jobs:
                 "os": large ? "nscloud-ubuntu-24.04-amd64-8x16-with-cache" : "ubuntu-latest",
                 "enabled": true,
                 "check-rebootstrap": level >= 1,
-                "check-stage3": level >= 2,
+                // Done as part of test-bench
+                //"check-stage3": level >= 2,
                 "test": true,
                 "secondary": true,
                 // NOTE: `test-bench` currently seems to be broken on `ubuntu-latest`

tests/bench/build/run_bench.sh

@@ -23,6 +23,8 @@ echo ">"
 echo "> Building $STAGE_NEXT..."
 echo ">"
 
+make -C "$BUILD_NEXT" clean-stdlib
+
 LAKE_OVERRIDE_LEAN=true LEAN="$(realpath fake_root/bin/lean)" \
 WRAPPER_PREFIX="$(realpath fake_root)" WRAPPER_OUT="$OUT" \
   lakeprof record -- \

tests/bench/sym/simp_1.lean

@@ -10,7 +10,9 @@ namespace SimpBench
 def getProofSize (r : Sym.Simp.Result) : MetaM Nat :=
   match r with
   | .rfl _ _ => return 0
-  | .step _ p _ _ => p.numObjs
+  | .step _ p _ _ =>
+    let p := ShareCommon.shareCommon' p
+    p.numObjs
 
 def checkWithKernel (r : Sym.Simp.Result) : MetaM Float := do
   match r with

tests/elab/sym_simp_3.lean

@@ -5,7 +5,7 @@ elab "sym_simp" "[" declNames:ident,* "]" : tactic => do
   let rewrite ← Sym.mkSimprocFor (← declNames.getElems.mapM fun s => realizeGlobalConstNoOverload s.raw) Sym.Simp.dischargeSimpSelf
   let methods : Sym.Simp.Methods := {
     pre  := Sym.Simp.simpControl
-    post := Sym.Simp.evalGround.andThen rewrite
+    post := Sym.Simp.evalGround >> rewrite
   }
   liftMetaTactic1 fun mvarId => Sym.SymM.run do
     let mvarId ← Sym.preprocessMVar mvarId