## Stream: general

### Topic: what does parsing mean?

#### Kenny Lau (Apr 12 2020 at 08:40):

Does parsing include typeclass resolution?

#### Kenny Lau (Apr 12 2020 at 08:41):

If I see parsing took 22.8s does that mean there are a lot of mega typeclass resolutions?

#### Mario Carneiro (Apr 12 2020 at 08:41):

I don't think it does

#### Mario Carneiro (Apr 12 2020 at 08:42):

I think typeclass resolution is part of elaboration

#### Kenny Lau (Apr 12 2020 at 08:43):

so it's mainly the tactics?

#### Kenny Lau (Apr 12 2020 at 08:44):

has the slow tactics parsing been solved in Lean 3.8?

#### Kenny Lau (Apr 12 2020 at 08:54):

can I make Lean tell me how much time it uses to parse each tactic?

#### Mario Carneiro (Apr 12 2020 at 08:56):

I think you already know all the profiling tricks

#### Mario Carneiro (Apr 12 2020 at 08:56):

you can try to incrementally add tactics to get a sense of the time of each

Last updated: May 11 2021 at 23:11 UTC