understanding profiler output

Stream: general

[Kevin Buzzard]

So I am 2/3 of the way through a pretty big proof which I am currently reluctant to break up into smaller pieces.

[Kevin Buzzard]

I might be pushing type class inference quite hard here, because it's a maths proof so everything is a group homomorphism and a ring homomorphism and I want Lean to infer everything.

[Kevin Buzzard]

It has got to the point when, whenever I type something, I get the orange "thinking" bars for 5 seconds.

[Kevin Buzzard]

I can live with this, but I wondered if there was an easy way to speed things up.

[Kevin Buzzard]

[I have other alternatives, such as "plough on" or "break the proof up into two pieces", which will be painful]

[Kevin Buzzard]

So I typed set_option profiler true

[Kevin Buzzard]

and now I can see a bunch of information and I realise I don't really understand it.

[Kevin Buzzard]

For example

[Kevin Buzzard]

it starts

[Kevin Buzzard]

elaboration: tactic execution took 4.96s
num. allocated objects:  5886
num. allocated closures: 6029
 4961ms   100.0%   _interaction._lambda_2
 4960ms   100.0%   tactic.istep
 4960ms   100.0%   scope_trace
 4959ms   100.0%   tactic.istep._lambda_1
 4959ms   100.0%   tactic.step
 3460ms    69.7%   tactic.to_expr
 1388ms    28.0%   tactic.interactive.have._lambda_1
 1055ms    21.3%   tactic.interactive.propagate_tags
 1007ms    20.3%   interaction_monad_orelse

[Kevin Buzzard]

so I would be quite happy to get the wait time down to 1 second

[Kevin Buzzard]

but I now see that the problem might be tactic.to_expr and tactic.step and this doesn't really help me at all in locating the problem

[Kevin Buzzard]

I am envisaging that the problem might be "this simp is taking forever", which I could fix by looking at the proof simp finds and then typing it in directly

[Kevin Buzzard]

or "this type class inference is taking forever", which again I feel like I might be able to help out with

[Kevin Buzzard]

How do I diagnose the issue further?

[Mario Carneiro]

The heavy hitters are the ones when the number of ms decreases significantly from the previous line

[Mario Carneiro]

so tactic.to_expr and tactic.interactive.have here

[Mario Carneiro]

Basically that means that elaboration is taking up all the time

[Kevin Buzzard]

so how can I help?

[Kevin Buzzard]

Can I see explicitly which lines of code are causing the problem?

[Kevin Buzzard]

ooh I just got an achievement

[Kevin Buzzard]

"type of sorry macro is not a sort"

[Kevin Buzzard]

new error message

[Kevin Buzzard]

heh

[Kevin Buzzard]

it should have said "you put an extra bracket on that line you dimwit"

[Kevin Buzzard]

OK so it might be the case that I can help the elaborator out. I have 500 lines of code. Where do I start?

[Kevin Buzzard]

elaboration of zariski.sheaf_of_types_on_standard_basis_for_finite_covers took 20.3s

[Kevin Buzzard]

finished :-)

[Kenny Lau]

wonderful

[Kevin Buzzard]

set_option class.instance_max_depth 75

[Kevin Buzzard]

This is just for one lemma.#

[Kevin Buzzard]

Obviously my code might be crappy

[Kevin Buzzard]

Will this whole system really scale?

[Kevin Buzzard]

max depth 72 is the min for which the code compiles

[Kevin Buzzard]

It's the proof that an affine scheme satisfies the sheaf axiom for finite covers of basic opens by basic opens

[Kevin Buzzard]

I've been putting it off for weeks, I knew it would be horrible, but I didn't know it would be this horrible.

[Andrew Ashworth]

Big proofs are quite wobbly... there's no way you can split the lemma up into something shorter and less complicated?

[Kevin Buzzard]

Not really. I could break it into some smaller pieces, but the problem is that the pieces other than the "main" piece would have really really complicated statements. Even the statement of the result whose hypotheses are so painful to check involves 13 groups / group homomorphisms which are inferred by type class inference, and the actual groups and homomorphisms involved are very elaborate, coming from some technical ring theory which I built up within the proof. Taking this stuff out into another lemma would involve making some very convoluted definitions and very long statements. On the other hand this is a snapshot of what "deep" mathematics looks like -- when one moves away from stuff like finite groups it does get complicated. Formalising graduate level real analysis (standard results in Hardy and Sobolev spaces) will I imagine be much worse.

[Mario Carneiro]

If you yearn for the day of explicit is_group_hom assumptions, why don't you make the type group_hom A B of all functions that are group homs between groups A and B? That will make the typeclass problem trivial

[Mario Carneiro]

It's not clear to me that this is the real issue, but it might help

[Mario Carneiro]

I am not convinced that the problems you are discovering are unavoidable, but I haven't had much time to look at your formalization in depth

[Johan Commelin]

@Kevin Buzzard Wow! Congratulations! That must have been a major road block.

[Johan Commelin]

Can someone explain to me what the pros and cons are of having a type group_hom A B like Mario suggested?

[Kevin Buzzard]

I personally don't understand the subtleties between the different possibilities for doing this - you could have a definition, or a structure, or a class. If you have a class then you want type class inference to do the donkeywork for you -- you seem to be making a commitment of the form "it should be easy to work out when something is a group hom so we'll make a machine do it for you". Unfortunately as I found out in my scheme work, life is not always so easy: I had a situation with a map f of (finite) types J -> I, groups G i and H j, and group homs c j from G (f j) to H j, and then wanted to define a map from Pi_i G i to Pi_j H j sending (g i) to the element which was c j (g (f j)) at j, and I thought I would be clogging up the type class inference system to write some explicit instance which was supposed to spot this, so I proved it by hand and then had to feed it into the type class inference system manually -- as I'm sure you'll agree Johan, a mathematician would note that this was obviously a group homomorphism -- "none of the G i or H j know anything about each other so they can't interfere with each other" -- and move on.

[Patrick Massot]

I think this scheme theory effort could be important for the future of maths in Lean. I can't wait to see how Mario or Johannes will clean it

[Patrick Massot]

I don't believe this monster proof cannot be cut in pieces

[Patrick Massot]

The issue is to figure out what is the right infrastructure

[Patrick Massot]

It's not about stating a lemma for each quarter of the proof (which would indeed give very technical statements)

[Patrick Massot]

It's like my problem with the chain rule, compared to the new Coq proof

[Patrick Massot]

In this case part of the infrastructure is a clever way of handling little o notations

[Patrick Massot]

I think figuring out the infrastructure is really a core skill for non-trivial math formalization, and it's certainly normal that we don't get it right on our first try (especially for people with no CS background)

[Kevin Buzzard]

I just did this scheme thing for fun. I have no idea whether they're interested in it for mathlib. I know that various bits should go in there, like the universal property of localization etc, but I don't know if they want all this sheaf stuff. My impression is that Mario is not that interested in definitions, he would rather have lemmas. I'm of a very different opinion but I was not going to be pushing for schemes to go into mathlib because of this. Mario was like "yeah but what the theorem?" when we talked about it and I was just going "it's schemes, there is no theorem, there are 1000 theorems but the fundamental thing is the definition". Well we'll have a theorem soon, but I'm not sure he'll be interested in it. I must say that this experience has made me deeply skeptical about stuff like https://blog.deepsense.ai/machine-learning-application-in-automated-reasoning/

[Johan Commelin]

Yes... there is something of a gap to bridge (-; You don't get there with just a bit of NLP.

[Johan Commelin]

Nevertheless, I sincerely hope that throwing some AI into the mix, the computer can take some of the tedious bits of work out of our hands...

[Johan Commelin]

And basically this is what we try to do with some tactics...

[Johan Commelin]

But one could imagine a rigged up version.

[Kevin Buzzard]

Having spent several days wrestling with a 500 line proof which was of the form "this is completely trivial", it is now a joy to be back writing short proofs of non-trivial statements -- "continuous image of compact is compact", "we already proved a lemma saying what the image of Spec(f) was in this case", "compact iff every open cover has a finite subcover" etc etc -- I feel like I'm making rapid progress in every line now.

[Patrick Massot]

I really really think you should try to get schemes in mathlib

[Patrick Massot]

Otherwise we'll never know whether Lean can handle it without type class depth 100

[Patrick Massot]

And I also think like https://blog.deepsense.ai/machine-learning-application-in-automated-reasoning/ looks like crackpot science

[Patrick Massot]

Clearly writing this paper without first trying to translate the scheme definition by hand is either stupid or fraud

[Kevin Buzzard]

In this thread (at the bottom of a big post containing lots of code) I was bemoaning the fact that the Lean code I enjoy writing best is very different (and in particular much longer) to the kind of Lean code which is mathlib-acceptable; I have no instinct to optimise and part of me actually thinks it's a step in the wrong direction because it makes proofs less readable.

I thought I would do some experiments trying to shorten my code and seeing if it made any difference to how quickly it compiled. But I've realised that the profiler output I'm seeing is so chaotic that I am not sure I will be able to draw any sensible conclusions from any experiment I do. With set_option profiler true set I restarted Lean 10 times and looked at how long it took to elaborate my proof that if $X$ is compact then $X\times Y\to Y$ is closed for all $Y$, and I got this:

elaboration of closed_pr2_of_compact took 186ms
elaboration of closed_pr2_of_compact took 192ms
elaboration of closed_pr2_of_compact took 169ms
elaboration of closed_pr2_of_compact took 227ms
elaboration of closed_pr2_of_compact took 92.1ms
elaboration of closed_pr2_of_compact took 195ms
elaboration of closed_pr2_of_compact took 254ms
elaboration of closed_pr2_of_compact took 287ms
elaboration of closed_pr2_of_compact took 256ms
elaboration of closed_pr2_of_compact took 262ms

The quickest run was about 1/3 the time of the longest. I should say that by "I restarted Lean" I mean various things, e.g. sometimes "I typed some characters into the file and then deleted them, forcing recompilation in VS Code" and sometimes "I hit ctrl-shift-P and restarted Lean".

Is there any way I can get a more meaningful answer to the question "exactly how many computer science units of time did it take to completely compile my current proof of this result"? Preferably one which bears some relation to wall clock time on a machine with nothing else running, but ideally is constant over restarts?

[Sebastian Ullrich]

That quickest run is definitely curious (assuming it wasn't a run where the proof was simply broken). You could try running Lean from the cmdline using lean -j0 to get hopefully more stable timings. You can also set profiler from there: lean -j0 -Dprofiler=true.

[Kevin Buzzard]

Even with my more unscientific method I can see the difference after just changing a bunch of apply h1, exact h2 to exact h1 h2 and split, exact h3, exact h4 to exact ⟨h3, h4⟩.

/-
elaboration of closed_pr2_of_compact took 150ms
elaboration of closed_pr2_of_compact took 80.6ms
elaboration of closed_pr2_of_compact took 93.1ms
elaboration of closed_pr2_of_compact took 89.5ms
elaboration of closed_pr2_of_compact took 111ms
elaboration of closed_pr2_of_compact took 137ms
elaboration of closed_pr2_of_compact took 135ms
elaboration of closed_pr2_of_compact took 168ms
elaboration of closed_pr2_of_compact took 177ms
elaboration of closed_pr2_of_compact took 168ms
-/

Does each tactic come with some sort of overhead which really means that e.g. rw X, rw Y is appreciably slower than rw [X,Y]?