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

fix: add missing registerTraceClass `Meta.synthInstance.instances (#4151)

Browse source 
The trace class Meta.synthInstance.answer isn't registered, so it can't
be used.

I set `inherited := true`, because I think it is a useful trace to have.
In particular it tells you when an instance has been found that has a
too large size. This is very useful information.
This commit is contained in:
JovanGerb 2024-05-15 19:59:01 +01:00 • committed by GitHub
parent 82666e5e7c
commit c7741607fb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Meta/SynthInstance.lean
View file

@ -827,6 +827,7 @@ builtin_initialize
registerTraceClass `Meta.synthInstance
registerTraceClass `Meta.synthInstance.instances (inherited := true)
registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
registerTraceClass `Meta.synthInstance.answer (inherited := true)
registerTraceClass `Meta.synthInstance.resume (inherited := true)
registerTraceClass `Meta.synthInstance.unusedArgs
registerTraceClass `Meta.synthInstance.newAnswer

1
tests/lean/366.lean.expected.out
View file

@ -3,4 +3,5 @@
[Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
[Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
[Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
[Meta.synthInstance.answer] ✅ Inhabited Nat
[Meta.synthInstance] result instInhabitedNat

9
tests/lean/815b.lean.expected.out
View file

@ -27,6 +27,7 @@
[Meta.synthInstance.instances] #[inst✝]
[Meta.synthInstance] ✅ apply inst✝ to IsSmooth f
[Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f
[Meta.synthInstance.answer] ✅ IsSmooth f
[Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 1
[Meta.synthInstance.unusedArgs] α → IsSmooth f
@ -133,6 +134,7 @@
[Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
[Meta.synthInstance] ✅ apply @identity to IsSmooth fun g => g
[Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a
[Meta.synthInstance.answer] ✅ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun a =>
a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 1
@ -144,9 +146,11 @@
[Meta.synthInstance.resume] propagating α →
IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 2
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
[Meta.synthInstance.resume] size: 3
[Meta.synthInstance.answer] ✅ IsSmooth fun g => g
[Meta.synthInstance.resume] propagating IsSmooth fun b a =>
b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 4
@ -158,18 +162,23 @@
[Meta.synthInstance.resume] propagating α →
IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 8
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating α →
IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] size: 4
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a)
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] size: 5
[Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a) d
[Meta.synthInstance.resume] propagating ∀ (a : α),
IsSmooth fun a_1 =>
f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
[Meta.synthInstance.resume] size: 6
[Meta.synthInstance.answer] ✅ IsSmooth fun g a => f (g a) d
[Meta.synthInstance] result swap fun a g => f (g a) d