Zulip Chat Archive

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

Kevin Buzzard (Apr 12 2020 at 08:43):

What about coercions?

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: Dec 20 2023 at 11:08 UTC