shortcut for `Seminorm.instMulAction`?

Stream: mathlib4

[Jireh Loreaux]

docs#Seminorm.instMulAction has the following very unfortunate behavior:

import Mathlib

open scoped NNReal

variable {𝕜 E : Type _} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

set_option synthInstance.maxHeartbeats 27000 in -- times out otherwise
#synth MulAction ℝ≥0 (Seminorm 𝕜 E) -- Seminorm.instMulAction

That is, it is timing out on what I believe is the most common use case. This doesn't show up in mathlib currently because, while it's relatively close to the heartbeat limit where it occurs, not enough of mathlib is imported to push it over the limit. However, various changes can push it over (e.g., #6310). So, what should we do about this? Should we add a shortcut instance for the usual case R := ℝ≥0 in docs#Seminorm.instMulAction ?

On a separate note, while writing down the mwe above, I came across something I don't know how to explain: adding explicit universe parameters allows us to the lower the heartbeat limit (both examples are taken to the nearest thousand). Is there a reason this should be the case?

variable {𝕜 : Type u} {E : Type v} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]

set_option synthInstance.maxHeartbeats 22000 in -- times out otherwise
#synth MulAction ℝ≥0 (Seminorm 𝕜 E) -- Seminorm.instMulAction

[Matthew Ballard]

Explicit universes have been seen to speed things up during the port. As to the exact reason...

[Matthew Ballard]

The term for Function.Injective.mulAction shrinks by about 25% (measured in terms of lines with pp.explicit) if you delete the smul field.

[Eric Wieser]

I think we should aim to replace X : Type _ with X : Type uX everywhere in mathlib (or write an elaborator to do it for us)

[Matthew Ballard]

Didn't @Kyle Miller do this?

[Matthew Ballard]

I agree that Type _ should disappear (as currently functioning).

[Eric Wieser]

Asking Lean to waste time solving universe constraints is kinda silly when maybe 95% of the time there is nothing to solve, of which maybe 1% it introduces actual bugs

[Kyle Miller]

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/function.2Ecombine/near/362309752 is an elaborator for Type* and Sort* (and just a day or two ago I was trying to remember the name of levelMVarToParam and where I'd last used it).

[Kyle Miller]

I'm happy to make a PR if we think using these in mathlib is a good idea, versus using explicit universe variables or some other solution.

[Matthew Ballard]

I would be interested in seeing the benchmark results from a large-scale swap.

[Kyle Miller]

It'd be neat if we could have Type* mean Type ?u for some unspecified universe parameter (not an expression, but an actual parameter). That is, have a new kind of level metavariable that can only unify with level parameters or other such metavariables. I feel like this is what I'd expect out of Type*, where writing (X Y : Type*) doesn't mean that X and Y are definitely in different universes.

[Eric Wieser]

I don't think that's a problem we really have. The big problem is that no one wants to write out the word Type u$n 10 times, so falls back on Type _

[Eric Wieser]

In the rare case where we actually do want to constrain the variables I think spelling things out the long way is fine.

[Kyle Miller]

I'm thinking about variable lines where some lemmas along the way are specialized to some of the types being in the same universe

[Jireh Loreaux]

I think that's relatively uncommon (at least in my part of mathlib)

[Notification Bot]

A message was moved from this topic to #maths > Proving extentionality for a category structure by Kyle Miller.

[Eric Wieser]

I'd rather see a very explicit marker on the lemma that something fishy is happening with universes

[Kyle Miller]

Eric Wieser said:

I think spelling things out the long way is fine.

When you say "is fine" do you mean "is better" or "is acceptable"?

Haven't you ever had bunch of type arguments and you decide you want to give them explicit universe levels, and it's a little annoying to split up the binder and maybe permute some of the arguments?

[Eric Wieser]

It's extraordinarily rare that I don't want to put all my types in different and unrelated universes

[Matthew Ballard]

The current situation is bad enough that I now instinctively want to break out X ... Z : Type _ whenever I see it. I think a change will have noticeable effect.

[Jireh Loreaux]

So, does anyone have an answer to the first part of my question?

[Matthew Ballard]

I took Kyle's Type* and tried to ruthlessly uproot Type _ from mathlib in #6370.

It had noticeable effect.

[Matthew Ballard]

Probably quite a few heart beat bumps can now be excised.

[Matthew Ballard]

An example: I deleted both bumps in RingTheory.ClassGroup.

[Sebastien Gouezel]

There's a lot of green there (really a lot!), but maxrss goes up by 192.3% which is a little bit surprising to me.

[Scott Morrison]

-1.37% wall clock!

[Matthew Ballard]

Another surprising things: Lean is working surprisingly hard on universe unification.

Maybe @Sebastian Ullrich can help us interpret the results.

[Matthew Ballard]

There are also some big outliers amongst the files. Analysis.InnerProductSpace.Basic is +128.2%. These are probably our fault but I can’t explain it at the moment

[Sebastian Ullrich]

It would be interesting to analyze these outliers, say with something like \time -v lake env lean --profile $FILE before and after the change. I can only assume that the maxrss increase is driven by a compilation regression in one of these files. Which in itself is surprising as compilation should not really care about universes.

[Matthew Ballard]

Before

interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 155ms
import took 376ms
typeclass inference of CoeFun took 105ms
typeclass inference of CoeFun took 112ms
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 103ms
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 100ms
simp took 163ms
simp took 164ms
simp took 1.55s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 122ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 153ms
compilation of Orthonormal.equiv took 131ms
simp took 104ms
compilation of innerSL took 374ms
typeclass inference of CoeFun took 758ms
type checking took 165ms
compilation of innerSLFlip took 2.29s
typeclass inference of TopologicalSpace took 118ms
typeclass inference of AddCommMonoid took 305ms
typeclass inference of Module took 322ms
typeclass inference of Module took 778ms
typeclass inference of Module took 777ms
typeclass inference of CoeT took 398ms
typeclass inference of CoeT took 397ms
typeclass inference of CoeT took 398ms
typeclass inference of CoeFun took 1.03s
typeclass inference of TopologicalSpace took 198ms
typeclass inference of AddCommMonoid took 368ms
typeclass inference of Module took 447ms
typeclass inference of CoeT took 4.75s
type checking took 678ms
elaboration took 1.28s
typeclass inference of CoeFun took 616ms
type checking took 137ms
typeclass inference of CoeFun took 615ms
typeclass inference of CoeFun took 145ms
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 100ms
typeclass inference of CoeFun took 101ms
typeclass inference of CoeFun took 101ms
elaboration took 287ms
cumulative profiling times:
attribute application 17.1ms
compilation 3.12s
compilation new 243ms
dsimp 0.313ms
elaboration 3.69s
import 376ms
initialization 14.5ms
interpretation 3.26s
linting 372ms
norm_num 83ms
parsing 70.1ms
ring 159ms
simp 4.38s
tactic execution 1.62s
type checking 2.26s
typeclass inference 36.2s
Command being timed: "lake env lean --profile Mathlib/Analysis/InnerProductSpace/Basic.lean"
User time (seconds): 55.37
System time (seconds): 1.37
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.80
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1600640
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 90
Minor (reclaiming a frame) page faults: 487274
Voluntary context switches: 44
Involuntary context switches: 411
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

After

interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.364._spec_1 took 172ms
import took 1.41s
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 105ms
typeclass inference of CoeFun took 104ms
typeclass inference of CoeFun took 101ms
simp took 170ms
simp took 170ms
simp took 1.62s
compilation of Orthonormal.equiv took 137ms
simp took 107ms
compilation of innerSL took 811ms
typeclass inference of CoeFun took 270ms
type checking took 171ms
compilation of innerSLFlip took 3.38s
typeclass inference of AddCommMonoid took 151ms
typeclass inference of Module took 170ms
typeclass inference of Module took 331ms
typeclass inference of Module took 329ms
typeclass inference of CoeT took 139ms
typeclass inference of AddCommMonoid took 152ms
typeclass inference of Module took 159ms
typeclass inference of CoeT took 134ms
typeclass inference of CoeT took 134ms
typeclass inference of CoeFun took 328ms
typeclass inference of AddCommMonoid took 176ms
typeclass inference of Module took 220ms
typeclass inference of CoeT took 1.87s
type checking took 635ms
compilation of ContinuousLinearMap.toSesqForm took 75.7s
elaboration took 596ms
typeclass inference of CoeFun took 628ms
type checking took 144ms
typeclass inference of CoeFun took 617ms
typeclass inference of CoeFun took 145ms
typeclass inference of CoeFun took 101ms
typeclass inference of CoeFun took 102ms
typeclass inference of CoeFun took 101ms
typeclass inference of CoeFun took 104ms
typeclass inference of CoeFun took 103ms
elaboration took 285ms
cumulative profiling times:
attribute application 20.2ms
compilation 80.4s
compilation new 295ms
dsimp 0.322ms
elaboration 2.77s
import 1.41s
initialization 14.4ms
interpretation 3.51s
linting 379ms
norm_num 85.9ms
parsing 70.3ms
ring 170ms
simp 4.48s
tactic execution 1.45s
type checking 2.28s
typeclass inference 27.9s
Command being timed: "lake env lean --profile Mathlib/Analysis/InnerProductSpace/Basic.lean"
User time (seconds): 122.32
System time (seconds): 2.96
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 2:06.54
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 13291168
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 25800
Minor (reclaiming a frame) page faults: 1211348
Voluntary context switches: 1707
Involuntary context switches: 13411
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

[Matthew Ballard]

Key line:

compilation of ContinuousLinearMap.toSesqForm took 75.7s

[Matthew Ballard]

But you can also see how the changes cut into the time for tc inference

[Sebastian Ullrich]

Also a 10x maxrss increase, which matches the overall maxrss of the run. So indeed it must be the runaway compilation step.

[Sebastian Ullrich]

I took a quick look, there is no trace.compiler.input output at all on master. Could it be that the change suddenly made the definition computable?

[Eric Wieser]

Does docs#ContinuousLinearMap.toSesqForm claim it's currently computable? (Edit: yes)

[Matthew Ballard]

The one above it is being compiled in both versions.

[Matthew Ballard]

Would code not get generated without a warning?

[Matthew Ballard]

The universe signatures of the two versions of the declaration are fairly different I think. Perhaps something computable is synthesized where before it wasn’t

[Matthew Ballard]

The other def’s also are compiled more slowly. Just not as huge a difference

[Eric Wieser]

What's the new set of universes? The current one looks correct in the docs.

[Matthew Ballard]

Hmm. Let me retract that. I don’t see how this could get generalized. I am remembering other declarations I looked at

[Matthew Ballard]

But perhaps it still possible that something computable is synthesized where it wasn’t before.

[Matthew Ballard]

There are also other outliers. The worst of the remaining:

• RingTheory.Noetherian
• Analysis.NormedSpace.Dual
• Algebra.Category.ModuleCat.Monoidal.Basic

[Matthew Ballard]

When I get a chance, I can profile them also. But that might not be for a bit

[Matthew Ballard]

Generating code for anything with an IsROrC instance seems strange to me.

[Matthew Ballard]

RingTheory.Noetherian

Before

import took 298ms
dsimp took 231ms
dsimp took 230ms
interpretation of Std.Tactic.Ext._aux_Std_Tactic_Ext___elabRules_Std_Tactic_Ext_tacticExt___:__1 took 122ms
interpretation of Std.Tactic._aux_Std_Tactic_RCases___elabRules_Std_Tactic_rcases_1 took 393ms
type checking took 108ms
elaboration took 11.3s
cumulative profiling times:
attribute application 2.04ms
compilation 1.32ms
compilation new 3.46ms
dsimp 518ms
elaboration 11.6s
import 298ms
initialization 14.2ms
interpretation 1.65s
linting 150ms
norm_num 4.29ms
parsing 13.3ms
ring 13.6ms
simp 155ms
tactic execution 361ms
type checking 202ms
typeclass inference 2.22s
Command being timed: "lake env lean --profile Mathlib/RingTheory/Noetherian.lean"
User time (seconds): 17.58
System time (seconds): 0.51
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:18.14
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1109040
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 224
Minor (reclaiming a frame) page faults: 194988
Voluntary context switches: 321
Involuntary context switches: 361
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

After

import took 308ms
dsimp took 134ms
dsimp took 137ms
interpretation of Std.Tactic.Ext._aux_Std_Tactic_Ext___elabRules_Std_Tactic_Ext_tacticExt___:__1 took 131ms
interpretation of Std.Tactic.Ext._aux_Std_Tactic_Ext___elabRules_Std_Tactic_Ext_tacticExt___:__1 took 119ms
interpretation of Std.Tactic._aux_Std_Tactic_RCases___elabRules_Std_Tactic_rcases_1 took 610ms
type checking took 104ms
linting took 3.86s
elaboration took 13.5s
cumulative profiling times:
attribute application 2.05ms
compilation 1.31ms
compilation new 3.45ms
dsimp 328ms
elaboration 13.8s
import 308ms
initialization 14.1ms
interpretation 1.94s
linting 3.93s
norm_num 4.2ms
parsing 13.4ms
ring 13.6ms
simp 132ms
tactic execution 440ms
type checking 197ms
typeclass inference 1.91s
Command being timed: "lake env lean --profile Mathlib/RingTheory/Noetherian.lean"
User time (seconds): 23.32
System time (seconds): 0.65
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:24.07
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1727696
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 332
Minor (reclaiming a frame) page faults: 236052
Voluntary context switches: 216
Involuntary context switches: 775
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

[Matthew Ballard]

Algebra.Category.ModuleCat.Monoidal.Basic

Before

import took 722ms
compilation of ModuleCat.MonoidalCategory.tensorHom took 170ms
typeclass inference of CoeT took 215ms
typeclass inference of CoeT took 184ms
type checking took 162ms
compilation of ModuleCat.MonoidalCategory.associator took 1.86s
tactic execution of Lean.Parser.Tactic.refl took 249ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1 took 591ms
elaboration took 174ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1 took 29.7s
type checking took 177ms
elaboration took 739ms
compilation of ModuleCat.MonoidalCategory.leftUnitor took 142ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 273ms
elaboration took 105ms
compilation of ModuleCat.MonoidalCategory.rightUnitor took 339ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 172ms
elaboration took 106ms
tactic execution of Lean.Parser.Tactic.apply took 2.24s
elaboration took 1.2s
typeclass inference of CoeT took 106ms
elaboration took 288ms
typeclass inference of CoeT took 138ms
typeclass inference of CoeT took 143ms
elaboration took 114ms
typeclass inference of CoeT took 101ms
typeclass inference of CoeT took 101ms
elaboration took 115ms
cumulative profiling times:
attribute application 4.14ms
compilation 2.52s
compilation new 20.8ms
dsimp 2.01ms
elaboration 3.26s
import 722ms
initialization 14.6ms
interpretation 31s
linting 56.1ms
parsing 7.85ms
simp 109ms
tactic execution 3.72s
type checking 760ms
typeclass inference 7.98s
Command being timed: "lake env lean --profile Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean"
User time (seconds): 49.67
System time (seconds): 1.08
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:51.18
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1353632
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 5732
Minor (reclaiming a frame) page faults: 178011
Voluntary context switches: 661
Involuntary context switches: 6428
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

After

import took 603ms
compilation of ModuleCat.MonoidalCategory.tensorHom took 173ms
typeclass inference of CoeT took 199ms
typeclass inference of CoeT took 175ms
type checking took 153ms
compilation of ModuleCat.MonoidalCategory.associator took 1.77s
tactic execution of Lean.Parser.Tactic.refl took 234ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1 took 715ms
elaboration took 173ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Convert___elabRules_Mathlib_Tactic_convert_1 took 36s
type checking took 3.8s
elaboration took 787ms
compilation of ModuleCat.MonoidalCategory.leftUnitor took 141ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 271ms
elaboration took 107ms
compilation of ModuleCat.MonoidalCategory.rightUnitor took 339ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 171ms
elaboration took 106ms
tactic execution of Lean.Parser.Tactic.apply took 2.31s
elaboration took 1.22s
typeclass inference of CoeT took 111ms
elaboration took 297ms
typeclass inference of CoeT took 147ms
typeclass inference of CoeT took 151ms
elaboration took 118ms
typeclass inference of CoeT took 101ms
typeclass inference of CoeT took 103ms
typeclass inference of CoeT took 102ms
typeclass inference of CoeT took 105ms
elaboration took 120ms
typeclass inference of CoeT took 103ms
typeclass inference of CoeT took 104ms
typeclass inference of CoeT took 100ms
typeclass inference of CoeT took 101ms
typeclass inference of CoeT took 103ms
typeclass inference of CoeT took 103ms
typeclass inference of CoeT took 104ms
typeclass inference of CoeT took 106ms
typeclass inference of CoeT took 100ms
typeclass inference of CoeT took 102ms
typeclass inference of CoeT took 101ms
typeclass inference of CoeT took 105ms
typeclass inference of CoeT took 101ms
cumulative profiling times:
attribute application 4.61ms
compilation 2.44s
compilation new 22.3ms
dsimp 2.12ms
elaboration 3.35s
import 603ms
initialization 13.9ms
interpretation 37.4s
linting 58.2ms
parsing 7.95ms
simp 115ms
tactic execution 3.79s
type checking 4.41s
typeclass inference 8.25s
Command being timed: "lake env lean --profile Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean"
User time (seconds): 59.60
System time (seconds): 1.45
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 1:01.39
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1558576
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 5512
Minor (reclaiming a frame) page faults: 191001
Voluntary context switches: 383
Involuntary context switches: 7297
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

[Matthew Ballard]

Analysis.NormedSpace.Dual

Before

interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.251._spec_1 took 186ms
import took 590ms
compilation of NormedSpace.inclusionInDoubleDual took 1.39s
elaboration took 388ms
elaboration took 142ms
compilation of NormedSpace.inclusionInDoubleDualLi took 3.18s
elaboration took 153ms
typeclass inference of CoeT took 185ms
cumulative profiling times:
attribute application 2.9ms
compilation 4.62s
compilation new 24.1ms
dsimp 0.483ms
elaboration 949ms
import 590ms
initialization 14ms
interpretation 957ms
linting 25.6ms
parsing 7.16ms
simp 169ms
tactic execution 239ms
type checking 249ms
typeclass inference 2.12s
Command being timed: "lake env lean --profile Mathlib/Analysis/NormedSpace/Dual.lean"
User time (seconds): 10.11
System time (seconds): 0.56
Percent of CPU this job got: 97%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:10.91
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 1763488
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 3868
Minor (reclaiming a frame) page faults: 219615
Voluntary context switches: 556
Involuntary context switches: 2067
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

After

interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.364._spec_1 took 168ms
import took 902ms
compilation of NormedSpace.inclusionInDoubleDual took 1.7s
elaboration took 167ms
elaboration took 132ms
compilation of NormedSpace.inclusionInDoubleDualLi took 6.85s
elaboration took 156ms
typeclass inference of CoeT took 176ms
cumulative profiling times:
attribute application 2.89ms
compilation 8.6s
compilation new 24.3ms
dsimp 0.462ms
elaboration 668ms
import 902ms
initialization 14.3ms
interpretation 960ms
linting 25.2ms
parsing 7.07ms
simp 163ms
tactic execution 230ms
type checking 247ms
typeclass inference 1.84s
Command being timed: "lake env lean --profile Mathlib/Analysis/NormedSpace/Dual.lean"
User time (seconds): 13.42
System time (seconds): 0.69
Percent of CPU this job got: 96%
Elapsed (wall clock) time (h:mm:ss or m:ss): 0:14.64
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 2327680
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 3953
Minor (reclaiming a frame) page faults: 256349
Voluntary context switches: 425
Involuntary context switches: 3514
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

[Matthew Ballard]

Dual seems closest to InnerProductSpace.Basic. The other two each seem different from all others

[Matthew Ballard]

Adding noncomputable to toSesqForm on master seems to have no effect on performance in terms of heart beats. Whereas, with the universe changes, it is lightning quick. You can remove the maxHeartbeats bump overall (though no the synth one)

[Matthew Ballard]

Also, replacing all Type* with Type _ just in the file cuts the compilation time and maxrss

output

interpretation of Lean.mkStateFromImportedEntries._at.Mathlib.Prelude.Rename.initFn._@.Mathlib.Mathport.Rename._hyg.364._spec_1 took 160ms
import took 365ms
typeclass inference of CoeFun took 101ms
simp took 166ms
simp took 166ms
simp took 1.57s
tactic execution of Lean.Parser.Tactic.rewriteSeq took 120ms
tactic execution of Lean.Parser.Tactic.rewriteSeq took 154ms
compilation of Orthonormal.equiv took 131ms
simp took 103ms
compilation of innerSL took 778ms
typeclass inference of CoeFun took 758ms
type checking took 166ms
compilation of innerSLFlip took 3.23s
typeclass inference of TopologicalSpace took 117ms
typeclass inference of AddCommMonoid took 310ms
typeclass inference of Module took 324ms
typeclass inference of Module took 792ms
typeclass inference of Module took 795ms
typeclass inference of CoeT took 405ms
typeclass inference of TopologicalSpace took 121ms
typeclass inference of AddCommMonoid took 311ms
typeclass inference of Module took 317ms
typeclass inference of CoeT took 401ms
typeclass inference of CoeT took 400ms
typeclass inference of CoeFun took 1.06s
typeclass inference of TopologicalSpace took 195ms
typeclass inference of AddCommMonoid took 367ms
typeclass inference of Module took 448ms
typeclass inference of CoeT took 4.66s
type checking took 642ms
compilation of ContinuousLinearMap.toSesqForm took 50.2s
elaboration took 1.28s
typeclass inference of CoeFun took 625ms
type checking took 143ms
typeclass inference of CoeFun took 631ms
typeclass inference of CoeFun took 144ms
elaboration took 292ms
cumulative profiling times:
attribute application 16.6ms
compilation 54.7s
compilation new 277ms
dsimp 0.31ms
elaboration 3.67s
import 365ms
initialization 14ms
interpretation 3.27s
linting 369ms
norm_num 82.6ms
parsing 66.6ms
ring 160ms
simp 4.39s
tactic execution 1.6s
type checking 2.25s
typeclass inference 36.8s
Command being timed: "lake env lean --profile Mathlib/Analysis/InnerProductSpace/Basic.lean"
User time (seconds): 106.97
System time (seconds): 2.06
Percent of CPU this job got: 99%
Elapsed (wall clock) time (h:mm:ss or m:ss): 1:49.07
Average shared text size (kbytes): 0
Average unshared data size (kbytes): 0
Average stack size (kbytes): 0
Average total size (kbytes): 0
Maximum resident set size (kbytes): 8888080
Average resident set size (kbytes): 0
Major (requiring I/O) page faults: 90
Minor (reclaiming a frame) page faults: 942795
Voluntary context switches: 42
Involuntary context switches: 659
Swaps: 0
File system inputs: 0
File system outputs: 0
Socket messages sent: 0
Socket messages received: 0
Signals delivered: 0
Page size (bytes): 16384
Exit status: 0

[Sebastian Ullrich]

It has something to do with the heartbeat timeout. Perhaps on master the timeout makes the compiler abort early, which makes the noncomputable section mark the definition as noncomputable. But in your PR, the compiler passes that stage without running into the timeout, and then does the actual, long compilation that does not check the timeout.

[Matthew Ballard]

It was non computable in mathlib3.

[Eric Wieser]

Lean 3 was much worse at deciding computability; it could be poisoned by typeclass assumptions used only for proofs

[Matthew Ballard]

So is this a bug or a feature?

[Matthew Ballard]

Matthew Ballard said:

So is this a bug or a feature?

By “this”, I mean that we’ve made Lean so fast it thinks it should start doing other things :)

[Matthew Ballard]

The whole file in mathlib3 was noncomputable theory.

[Matthew Ballard]

Yes, removing noncomputable section from the start of the file on master gives

▶ 1824:5-1824:15: error:
compiler IR check failed at 'TopologicalAddGroup.toUniformSpace._at.ContinuousLinearMap.toSesqForm._spec_9._rarg', error: unknown declaration 'ContinuousLinearMap.toSeminormedAddCommGroup'

[Matthew Ballard]

I get the same error on the PR branch so I don't think it is generating any code despite its serious efforts

[Matthew Ballard]

Also, trace.compiler.input reports nothing on the PR branch. Furthermore, it seems to short-circuit compilation of toSesqForm completely.

[Matthew Ballard]

I went through and poked at all the heart beat bumps with the fix to universes. Here is the diff between before and after

[Matthew Ballard]

Coarse count: 65/153 bumps (counting both types) were eliminated. The majority of the those not eliminated were decreased.

[Matthew Ballard]

About 30 out of 80 files became bump-free

[Matthew Ballard]

If anyone wants to help interpret the diff above, I would appreciate it. Some thoughts:

• You can get some incredible speed ups. One declaration lost 8000000 heart beats. Some in the millions were completely gone. Even million-level synthInstance.maxHeartbeats(almost) were wiped out. (Checkout our old friend OperatorNorm for fun.)
• Some other ones were completely inert to the change. (Though I think all increases are user-error.)
• It seems that synthInstance.maxHeartBeats were wiped at a higher rate than overall bumps. This comports with the 7.5% improvement in tc inference vs the overall 4% improvement in instructions.

As to an explanations, I have some thoughts but nothing I can really support with hard data.

[Eric Wieser]

Did we track down the increased memory usage? (or did it go away)

[Matthew Ballard]

Lean was trying to compile toSesqForm and spending lots of resources on it. It looks like it doesn't actually build anything -- just heats up your lap.

I don't know the exact reason for why it is happening.

But marking it noncomputable explicitly short circuits it and seems fine for the current purposes

[Matthew Ballard]

Matthew Ballard said:

Also, trace.compiler.input reports nothing on the PR branch. Furthermore, it seems to short-circuit compilation of toSesqForm completely.

This was weird

[Jireh Loreaux]

This thread got derailed (in a good way!), but does anyone have a suggestion for the original post in this thread?

[Matthew Ballard]

lean4#2451 ? It times out around 15000 on #6759 with Type*