Timing differences between #eval and native_decide

Stream: lean4

[Alain Chavarri Villarello]

Yesterday, @Assia Mahboubi , @Sander Dahmen and I were playing around with lists and indexing. I have a question about something that we noticed. 

Consider, for example, a list L of natural numbers of length 200.

set_option trace.profiler true
set_option trace.profiler.threshold 1

def L : List Nat := [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1,
2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9,
10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

#eval L.get! 198

example: L.get! 198 = 9 := by native_decide

The timing of [Elab.command] in the profiling output for #eval L.get! 198 seems to be consistently higher —by a factor of around 2 or 3 — than for example: L.get! 198 = 9 := by native_decide. My understanding is that native_decide also uses the code compiler (#eval) to evaluate the corresponding decidable instance. So I was wondering, why is there such a noticeable time difference? 

Furthermore, after importing Mathlib, the time spent in #eval L.get! 198 seems to increase (at least 3x). Does anyone know why this happens? Thanks!

[Sebastian Ullrich]

I would suggest to ignore differences on the millisecond level, that can likely be explained by other differences between the two commands such as #eval needing to format the output and doing some typeclass synthesis for that