Skip to content

perf: try reverting #21330 #25475

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
grunweg wants to merge 3 commits into from
Closed

perf: try reverting #21330 #25475

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2256a1e
perf: try reverting #21330
grunweg Jun 5, 2025
162d86a
wip/hack: fix
grunweg Jun 5, 2025
8277e45
fix
JovanGerb Jun 5, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -715,6 +715,7 @@ open IdealSheafData in
noncomputable
def kerAdjunction (Y : Scheme.{u}) : (subschemeFunctor Y).rightOp ⊣ Y.kerFunctor where
unit.app I := eqToHom (by simp)
unit.naturality _ _ _ := rfl
counit.app f := (Over.homMk f.unop.hom.toImage f.unop.hom.toImage_imageι).op
counit.naturality _ _ _ := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
left_triangle_components I := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
Expand Down
25 changes: 2 additions & 23 deletions Mathlib/CategoryTheory/Category/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,27 +107,6 @@ open Lean Meta Elab.Tactic in
else
throwError "The goal does not contain `sorry`"

/--
`rfl_cat` is a macro for `intros; rfl` which is attempted in `aesop_cat` before
doing the more expensive `aesop` tactic.

This gives a speedup because `simp` (called by `aesop`) is too slow.
There is a fix for this slowness in https://github.com/leanprover/lean4/pull/7428.
So, when that is resolved, the performance impact of `rfl_cat` should be measured again.

Implementation notes:
* `refine id ?_`:
In some cases it is important that the type of the proof matches the expected type exactly.
e.g. if the goal is `2 = 1 + 1`, the `rfl` tactic will give a proof of type `2 = 2`.
Starting a proof with `refine id ?_` is a trick to make sure that the proof has exactly
the expected type, in this case `2 = 1 + 1`. See also https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof
* `apply_rfl`:
`rfl` is a macro that attempts both `eq_refl` and `apply_rfl`. Since `apply_rfl`
subsumes `eq_refl`, we can use `apply_rfl` instead. This fails twice as fast as `rfl`.

-/
macro (name := rfl_cat) "rfl_cat" : tactic => do `(tactic| (refine id ?_; intros; apply_rfl))

/--
A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and
allows `aesop` to look through semireducible definitions when calling `intros`.
Expand All @@ -136,7 +115,7 @@ use in auto-params.
-/
macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
`(tactic|
first | sorry_if_sorry | rfl_cat |
first | sorry_if_sorry |
aesop $c* (config := { introsTransparency? := some .default, terminal := true })
(rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))

Expand All @@ -145,7 +124,7 @@ We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop
-/
macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
`(tactic|
first | sorry_if_sorry | try_this rfl_cat |
first | sorry_if_sorry |
aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
(rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
/--
Expand Down
6 changes: 4 additions & 2 deletions Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,8 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgCat R where
ext : 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
refine TensorProduct.ext ?_
rfl }
rfl
one_hom := by rfl } -- simp fails with an error "maximum recursion depth reached"
inv :=
{ hom := ofHom
{ toFun := _root_.id
Expand All @@ -186,7 +187,8 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgCat R where
ext : 1
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
refine TensorProduct.ext ?_
rfl } })
rfl
one_hom := by rfl } }) -- simp fails with an error "maximum recursion depth reached"
counitIso :=
NatIso.ofComponents
(fun A =>
Expand Down
Loading