max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf(library/init/lean/parser/command): move common command parsers to the beginning of the list

Browse source 
@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.
This commit is contained in:
Leonardo de Moura 2018-11-08 14:30:44 -08:00
parent ad9aa3bc19
commit 1cb22b6801
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/init/lean/parser/command.lean
View file

@ -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)