Zulip Chat Archive

Stream: general

Topic: what does parsing mean?


view this post on Zulip Kenny Lau (Apr 12 2020 at 08:40):

Does parsing include typeclass resolution?

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:41):

I don't think it does

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:42):

I think typeclass resolution is part of elaboration

view this post on Zulip Kevin Buzzard (Apr 12 2020 at 08:43):

What about coercions?

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:43):

so it's mainly the tactics?

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:44):

has the slow tactics parsing been solved in Lean 3.8?

view this post on Zulip Kenny Lau (Apr 12 2020 at 08:54):

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

view this post on Zulip Mario Carneiro (Apr 12 2020 at 08:56):

I think you already know all the profiling tricks

view this post on Zulip 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