From c0a53ffe9749ada0887cbb98c1bab5051029dbef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Apr 2026 23:11:30 +0200 Subject: [PATCH] chore: minor tweaks to `Sym.simp` test and benchmark (#13468) 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) --- tests/bench/sym/simp_1.lean | 4 +++- tests/elab/sym_simp_3.lean | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/tests/bench/sym/simp_1.lean b/tests/bench/sym/simp_1.lean index b128e587bd..b5bc23ac42 100644 --- a/tests/bench/sym/simp_1.lean +++ b/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 diff --git a/tests/elab/sym_simp_3.lean b/tests/elab/sym_simp_3.lean index 7062859f45..014290f987 100644 --- a/tests/elab/sym_simp_3.lean +++ b/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