From 1cb22b6801dafa5f8ae81994bcb0d3f8e39ca218 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Nov 2018 14:30:44 -0800 Subject: [PATCH] perf(library/init/lean/parser/command): move common command parsers to the beginning of the list MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit @kha This modification saved 150k object allocations on my machine. BTW, the function ``` def command_parser.run (commands : list command_parser) (p : command_parser) : parser_t command_parser_config id syntax := λ cfg, (p.run cfg).run_parsec $ λ _, any_of $ commands.map (λ p, p.run cfg) ``` is also affected by the problem I described at Zulip. It is another example where eager eta-expansion is bad. Every time we call it, we will create approx. 20 closures and 20 cons memory cells. We have at least 600 commands in core.lean. So, just the `map` nested there will generate 24k memory allocations. Moreover, the problem will get worse as we add more commands. --- library/init/lean/parser/command.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean index ff2a9cf8ce..6a50497784 100644 --- a/library/init/lean/parser/command.lean +++ b/library/init/lean/parser/command.lean @@ -98,10 +98,10 @@ node! «attribute» [ @[derive has_tokens] def builtin_command_parsers : list command_parser := [ + declaration.parser, variable.parser, variables.parser, namespace.parser, end.parser, open.parser, section.parser, universe.parser, notation.parser, reserve_notation.parser, - mixfix.parser, reserve_mixfix.parser, check.parser, declaration.parser, attribute.parser, - export.parser, namespace.parser, end.parser, variable.parser, variables.parser, include.parser, - omit.parser] + mixfix.parser, reserve_mixfix.parser, check.parser, attribute.parser, + export.parser, include.parser, omit.parser] end «command» def command_parser.run (commands : list command_parser) (p : command_parser)