Slight change to typeclass use slows down 15 seconds -> 5 minutes

philnguyen commented 1 year ago

Prerequisites

[x] Put an X between the brackets on this line if you have done all of the following:
- Check that your issue is not already filed.
- Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

Calling a function with lots of typeclass parameters following a specific pattern can significantly slow down build.

Context

I have a silly project (attached, not very minimal, but self-contained) that uses typeclass in a possibly wrong way that slows down the build from ~15 seconds to ~5 minutes on my M2 macbook air.

While it may be just me not knowing how to use typeclasses effectively, I wonder if this problem could also show up in other projects. I can reproduce this problem in Lean releases 4.0, 4.1, and the latest build at the time I report this.

Steps to Reproduce

Attached self-contained variants of the same project: slow-build.tgz fast-build.tgz

tar -zxvf fast-build.tgz && cd fast-build
time lake build
(This takes 15 seconds on an M2 macbook air, and about 30 seconds on an Intel desktop)
tar -zxvf slow-build.tgz && cd slow-build
time lake build
(This takes 5 minutes on an M2 macbook air, and about 12 minutes on an Intel desktop)

Expected behavior: Building project (about 1400 lines of Lean) should take reasonable time

Actual behavior: Building slow-build takes surprisingly long

Versions

Lean (version 4.3.0-nightly-2023-10-01, commit e6292bc0b890, Release)

Mac OS Ventura 13.5.2; also reproducible with Linux and Intel

Additional Information

The only differences in slow-build and fast-build are in the files Analyzer.lean and Main.lean. In fast-build, the typeclass parameters for analyze are kept more abstract for a bit longer and instantiated later in Main.lean.

Impact

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

kim-em commented 1 year ago

If you are able to minimize this down to a single file (ideally showing both variants in the same file) it is much more likely that someone can help you with this.

If you're having trouble minimizing, you might start by asking for help on zulip first.

philnguyen commented 1 year ago

Sorry for taking so long to get back!

I consolidated the project into 1 file Main.lean (plus lakefile.lean), and tried to stub it out with trivial values and sorry, and deleted as much as I could without shrinking the build time. The turnaround time was really long so I just left it run in a different computer during my day job.

The shrinked project (project.tgz) still isn't minimal at all (~800 lines), but I also took its profile, and the profile is very not flat (lots of time spent in compiling analyze at the end), so I think the experts will be able to tell the problem right away?

The file only has many uses of typeclasses, and no theorem proving. I didn't minimize the project further because if I replace most other definitions with sorry, they shrink the build time.

Below is an output from time lean --profile --stats Main.lean -o main:

compilation of _private.Main.0.inst_base took 1.56s
compilation of analyze took 108s
Main.lean:128:0: warning: declaration uses 'sorry'
Main.lean:130:0: warning: declaration uses 'sorry'
Main.lean:132:0: warning: declaration uses 'sorry'
Main.lean:338:0: warning: declaration uses 'sorry'
Main.lean:358:0: warning: declaration uses 'sorry'
Main.lean:359:0: warning: declaration uses 'sorry'
Main.lean:369:0: warning: declaration uses 'sorry'
Main.lean:370:0: warning: declaration uses 'sorry'
Main.lean:377:0: warning: declaration uses 'sorry'
Main.lean:378:0: warning: declaration uses 'sorry'
Main.lean:401:4: warning: declaration uses 'sorry'
Main.lean:402:4: warning: declaration uses 'sorry'
Main.lean:761:0: warning: declaration uses 'sorry'
direct imports:                        #[Init]
number of imported modules:            106
number of memory-mapped modules:       106
number of consts:                      71008
number of imported consts:             22997
number of local consts:                48011
number of buckets for imported consts: 65536
trust level:                           1025
number of extensions:                  84
extension 'Lean.namespacesExt'
  number of local entries: 26391
  number of imported entries: 11722
extension 'Lean.protectedExt'
  number of local entries: 92
  number of imported entries: 1247
extension 'Lean.aliasExtension'
  number of local entries: 0
  number of imported entries: 76
extension 'Lean.auxRecExt'
  number of local entries: 46
  number of imported entries: 518
extension 'Lean.noConfusionExt'
  number of local entries: 23
  number of imported entries: 230
extension 'Lean.attributeExtension'
  number of local entries: 0
  number of imported entries: 2
extension 'Lean.Compiler.inlineAttrs'
  enumeration attribute extension
  number of local entries: 86
  number of imported entries: 1164
extension 'Lean.classExtension'
  number of local entries: 13
  number of imported entries: 120
extension 'Lean.reducibilityAttrs'
  enumeration attribute extension
  number of local entries: 122
  number of imported entries: 1418
extension 'Lean.Compiler.nospecializeAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 5
extension 'Lean.Compiler.specializeAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 92
extension 'Lean.Compiler.specExtension'
  number of local entries: 1443
  number of imported entries: 3105
extension 'Lean.projectionFnInfoExt'
  number of local entries: 44
  number of imported entries: 365
extension 'Lean.externAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 358
extension 'Lean.Compiler.implementedByAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 33
extension 'Lean.neverExtractAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 9
extension 'Lean.IR.declMapExt'
  number of local entries: 34320
  number of imported entries: 12860
extension 'Lean.exportAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 42
extension 'Lean.IR.UnboxResult.unboxAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 4
extension 'Lean.IR.UnreachableBranches.functionSummariesExt'
  number of local entries: 31764
  number of imported entries: 10664
extension 'Lean.regularInitAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 1
extension 'Lean.builtinInitAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Compiler.CSimp.ext'
  number of local entries: 0
  number of imported entries: 10
extension 'Lean.noncomputableExt'
  number of local entries: 0
  number of imported entries: 19
extension 'Lean.Meta.globalInstanceExtension'
  number of local entries: 69
  number of imported entries: 878
extension 'Lean.structureExt'
  number of local entries: 16
  number of imported entries: 191
extension 'Lean.Meta.Match.Extension.extension'
  number of local entries: 64
  number of imported entries: 597
extension 'Lean.matchPatternAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 9
extension 'Lean.Meta.instanceExtension'
  number of local entries: 69
  number of imported entries: 878
extension 'Lean.Meta.defaultInstanceExtension'
  number of local entries: 0
  number of imported entries: 17
extension 'Lean.Compiler.LCNF.baseExt'
  number of imported entries: 3168
extension 'Lean.Compiler.LCNF.monoExt'
  number of imported entries: 3635
extension 'Lean.Meta.coeDeclAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 14
extension 'Lean.Linter.deprecatedAttr'
  parametric attribute
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.declRangeExt'
  number of local entries: 272
  number of imported entries: 4986
extension 'Lean.docStringExt'
  number of local entries: 0
  number of imported entries: 1485
extension 'Lean.moduleDocExt'
  number of local entries: 0
  number of imported entries: 72
extension 'Lean.Parser.parserExtension'
  number of local entries: 38
  number of imported entries: 13250
extension 'Lean.PrettyPrinter.parenthesizerAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.categoryParenthesizerAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.mkCombinatorParenthesizerAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.formatterAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.mkCombinatorFormatterAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Elab.macroAttribute'
  number of local entries: 11
  number of imported entries: 227
extension 'Lean.Elab.Term.termElabAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.Delaborator.delabAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute'
  number of local entries: 10
  number of imported entries: 91
extension 'Lean.Compiler.LCNF.Simp.ConstantFold.folderExt'
  number of imported entries: 0
extension 'Lean.Compiler.LCNF.specExtension'
  number of local entries: 152
  number of imported entries: 662
extension 'Lean.Compiler.LCNF.Specialize.specCacheExt'
  number of local entries: 13
  number of imported entries: 109
extension 'Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt'
  number of local entries: 215
  number of imported entries: 3354
extension 'Lean.Compiler.LCNF.passManagerExt'
  number of imported entries: 0
extension 'Lean.Elab.Term.Quotation.precheckAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Elab.Tactic.tacticElabAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Elab.Command.commandElabAttribute'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Meta.customEliminatorExt'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Elab.Term.elabWithoutExpectedTypeAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Elab.Term.elabAsElim'
  tag attribute
  number of local entries: 0
  number of imported entries: 11
extension 'Lean.Meta.recursorAttribute'
  parametric attribute
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Meta.simpExtension'
  number of local entries: 52
  number of imported entries: 519
extension 'Lean.Meta.congrExtension'
  number of local entries: 0
  number of imported entries: 2
extension 'Lean.Elab.WF.eqnInfoExt'
  number of local entries: 4
  number of imported entries: 40
extension 'Lean.Elab.ComputedFields.computedFieldAttr'
  tag attribute
  number of local entries: 0
  number of imported entries: 1
extension 'Lean.Elab.Structural.eqnInfoExt'
  number of local entries: 6
  number of imported entries: 188
extension 'Lean.Linter.MissingDocs.missingDocsExt'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Meta.unificationHintExtension'
  number of local entries: 0
  number of imported entries: 1
extension 'Lean.Linter.unusedVariablesIgnoreFnsExt'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Server.Completion.completionBlackListExt'
  number of local entries: 24
  number of imported entries: 240
extension 'Lean.Server.userRpcProcedures'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Server.codeActionProviderExt'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Widget.userWidgetRegistry'
  number of local entries: 0
  number of imported entries: 0
extension 'Lean.Widget.widgetSourceRegistry'
  number of local entries: 0
  number of imported entries: 0
.olean serialization took 2.41s
cumulative profiling times:
    .olean serialization 2.41s
    attribute application 4.28ms
    compilation 110s
    compilation new 577ms
    elaboration 499ms
    import 19.2ms
    initialization 23.3ms
    interpretation 30ms
    linting 24.1ms
    parsing 20.7ms
    simp 34.8ms
    tactic execution 103ms
    type checking 60.9ms
    typeclass inference 253ms
lean --profile --stats Main.lean -o main  113.75s user 0.52s system 99% cpu 1:54.29 total

When I build using lake it takes about twice that time. During the second half, when I looked at the process monitor, clang takes a lot of time too:

[0/2] Building Main
stdout:
./././Main.lean:128:0: warning: declaration uses 'sorry'
./././Main.lean:130:0: warning: declaration uses 'sorry'
./././Main.lean:132:0: warning: declaration uses 'sorry'
./././Main.lean:338:0: warning: declaration uses 'sorry'
./././Main.lean:358:0: warning: declaration uses 'sorry'
./././Main.lean:359:0: warning: declaration uses 'sorry'
./././Main.lean:369:0: warning: declaration uses 'sorry'
./././Main.lean:370:0: warning: declaration uses 'sorry'
./././Main.lean:377:0: warning: declaration uses 'sorry'
./././Main.lean:378:0: warning: declaration uses 'sorry'
./././Main.lean:401:4: warning: declaration uses 'sorry'
./././Main.lean:402:4: warning: declaration uses 'sorry'
./././Main.lean:761:0: warning: declaration uses 'sorry'
[1/2] Compiling Main
[2/2] Linking prototype
lake build  310.77s user 3.41s system 99% cpu 5:14.53 total

Many thanks!!

philnguyen commented 1 year ago

Any chance the "awaiting author" tag can be lifted? I'm happy to do whatever profiling work that would help

Kha commented 1 year ago

Thanks for the profiling, that it is time spent in the old code generator is the important clue. However, as such it is also unlikely to be fixed until the new code generator is finished.

leanprover / lean4