max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: grind build times (#10127)

Browse source
This commit is contained in:
Leonardo de Moura 2025-08-25 23:01:50 -07:00 • committed by GitHub
parent 5478dcf373
commit 3ff195f7b2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 11 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Meta/Tactic/Grind/AC/Internalize.lean
View file

@ -15,7 +15,8 @@ private def isParentSameOpApp (parent? : Option Expr) (op : Expr) : GoalM Bool :
unless e.isApp && e.appFn!.isApp do return false
return isSameExpr e.appFn!.appFn! op
def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
@[export lean_grind_ac_internalize]
def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
unless (← getConfig).ac do return ()
unless e.isApp && e.appFn!.isApp do return ()
let op := e.appFn!.appFn!

1
src/Lean/Meta/Tactic/Grind/Arith.lean
View file

@ -16,5 +16,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing
public import Lean.Meta.Tactic.Grind.Arith.Linear
public import Lean.Meta.Tactic.Grind.Arith.Simproc
public import Lean.Meta.Tactic.Grind.Arith.VarRename
public import Lean.Meta.Tactic.Grind.Arith.Internalize
public section

3
src/Lean/Meta/Tactic/Grind/Arith/Internalize.lean
View file

@ -15,7 +15,8 @@ public section
namespace Lean.Meta.Grind.Arith
def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
@[export lean_grind_arith_internalize]
def internalizeImpl (e : Expr) (parent? : Option Expr) : GoalM Unit := do
Offset.internalize e parent?
Cutsat.internalize e parent?
CommRing.internalize e parent?

3
src/Lean/Meta/Tactic/Grind/EMatch.lean
View file

@ -6,9 +6,6 @@ Authors: Leonardo de Moura
module
prelude
public import Lean.Meta.Tactic.Grind.Types
import Lean.Meta.Tactic.Grind.Intro
import Lean.Meta.Tactic.Grind.MatchDiscrOnly
import Lean.Meta.Tactic.Grind.MatchCond
import Lean.Meta.Tactic.Grind.Core
public section
namespace Lean.Meta.Grind

8
src/Lean/Meta/Tactic/Grind/Internalize.lean
View file

@ -17,12 +17,16 @@ public import Lean.Meta.Tactic.Grind.Types
public import Lean.Meta.Tactic.Grind.Util
public import Lean.Meta.Tactic.Grind.Beta
public import Lean.Meta.Tactic.Grind.MatchCond
public import Lean.Meta.Tactic.Grind.Arith.Internalize
public import Lean.Meta.Tactic.Grind.AC.Internalize
public section
namespace Lean.Meta.Grind
@[extern "lean_grind_ac_internalize"] -- forward definition
opaque AC.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
@[extern "lean_grind_arith_internalize"] -- forward definition
opaque Arith.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit
/-- Adds `e` to congruence table. -/
def addCongrTable (e : Expr) : GoalM Unit := do
if let some { e := e' } := (← get).congrTable.find? { e } then

6
src/Lean/Meta/Tactic/Grind/Types.lean
View file

@ -10,17 +10,11 @@ public import Init.Grind.Tactics
public import Init.Data.Queue
public import Std.Data.TreeSet.Basic
public import Lean.HeadIndex
public import Lean.Meta.Basic
public import Lean.Meta.CongrTheorems
public import Lean.Meta.AbstractNestedProofs
public import Lean.Meta.Tactic.Simp.Types
public import Lean.Meta.Tactic.Util
public import Lean.Meta.Tactic.Ext
public import Lean.Meta.Tactic.Grind.ExprPtr
public import Lean.Meta.Tactic.Grind.AlphaShareCommon
public import Lean.Meta.Tactic.Grind.Attr
public import Lean.Meta.Tactic.Grind.ExtAttr
public import Lean.Meta.Tactic.Grind.Cases
public import Lean.Meta.Tactic.Grind.Arith.Types
public import Lean.Meta.Tactic.Grind.AC.Types
public import Lean.Meta.Tactic.Grind.EMatchTheorem