From dfaf9c6ebded4338e760963d1a13832d773bef50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Nov 2022 13:32:50 -0800 Subject: [PATCH] chore: register missing trace options, and fix `inherited` parameter The current setting was bad for debugging `isDefEq` issues. --- src/Lean/Meta/ExprDefEq.lean | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index bb57345edb..50eadbb60f 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -1756,11 +1756,23 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD builtin_initialize registerTraceClass `Meta.isDefEq - registerTraceClass `Meta.isDefEq.foApprox - registerTraceClass `Meta.isDefEq.constApprox - registerTraceClass `Meta.isDefEq.delta (inherited := true) + registerTraceClass `Meta.isDefEq.stuck + registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true) + registerTraceClass `Meta.isDefEq.cache + registerTraceClass `Meta.isDefEq.foApprox (inherited := true) + registerTraceClass `Meta.isDefEq.onFailure (inherited := true) + registerTraceClass `Meta.isDefEq.constApprox (inherited := true) + registerTraceClass `Meta.isDefEq.delta + registerTraceClass `Meta.isDefEq.delta.unfoldLeft (inherited := true) + registerTraceClass `Meta.isDefEq.delta.unfoldRight (inherited := true) + registerTraceClass `Meta.isDefEq.delta.unfoldLeftRight (inherited := true) registerTraceClass `Meta.isDefEq.assign registerTraceClass `Meta.isDefEq.assign.checkTypes (inherited := true) + registerTraceClass `Meta.isDefEq.assign.outOfScopeFVar (inherited := true) + registerTraceClass `Meta.isDefEq.assign.beforeMkLambda (inherited := true) + registerTraceClass `Meta.isDefEq.assign.typeError (inherited := true) + registerTraceClass `Meta.isDefEq.assign.occursCheck (inherited := true) + registerTraceClass `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx (inherited := true) registerTraceClass `Meta.isDefEq.eta.struct end Lean.Meta