Stream: Coq users

Topic: Strange perf difference with name mangling


view this post on Zulip Ralf Jung (Sep 29 2023 at 16:44):

I discovered something odd... adding these flags to Iris:

#[export] Set Mangle Names.
#[export] Set Mangle Names Light.
#[export] Set Mangle Names Prefix "__".

makes the overall build 8% faster, some files become 40-60% faster!
Here's a file-by-file diff.

Something has to be very wrong here, right? Generating fresh names shouldn't have a noticeable impact on Coq's performance, at least not on this scale.

view this post on Zulip Ralf Jung (Sep 29 2023 at 16:45):

all our CI and timing builds (both the fast and the slow one) are done with COQEXTRAFLAGS="-mangle-names _", which might also play a role

view this post on Zulip Paolo Giarrusso (Sep 29 2023 at 20:03):

Let me add a question: The docs for Set Fast Name Printing imply it might be relevant — "deshadowing" has bad asymptotics, and name mangling clearly affects the inputs to deshadowing. Should we tune these options for performance, and how? More details would help.

From https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:flag.Fast-Name-Printing :

When this flag is turned on, Coq uses an asymptotically faster algorithm for the generation of unambiguous names of bound variables while printing terms. While faster, it is also less clever and results in a typically less elegant display, e.g. it will generate more names rather than reusing certain names across subterms. This flag is not enabled by default, because as Ltac observes bound names, turning it on can break existing proof scripts.

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:27):

so "Fast Name Printing" doesnt make printing faster, it makes name generation faster even when noting is printed?

view this post on Zulip Ralf Jung (Oct 02 2023 at 09:28):

the name indicates that the flag would be a NOP when one doesnt print anything, but the description says something else


Last updated: Jun 23 2024 at 04:03 UTC