Zulip Chat Archive

Stream: general

Topic: understanding profiler output


view this post on Zulip Kevin Buzzard (May 11 2018 at 07:44):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:45):

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.

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:45):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:46):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:47):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:47):

So I typed set_option profiler true

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:47):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:48):

For example

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:49):

it starts

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:50):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:50):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:50):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:51):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:51):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 07:51):

How do I diagnose the issue further?

view this post on Zulip Mario Carneiro (May 11 2018 at 07:55):

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

view this post on Zulip Mario Carneiro (May 11 2018 at 07:55):

so tactic.to_expr and tactic.interactive.have here

view this post on Zulip Mario Carneiro (May 11 2018 at 07:56):

Basically that means that elaboration is taking up all the time

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:15):

so how can I help?

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:15):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:16):

ooh I just got an achievement

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:16):

"type of sorry macro is not a sort"

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:16):

new error message

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:17):

heh

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:17):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 08:18):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:11):

elaboration of zariski.sheaf_of_types_on_standard_basis_for_finite_covers took 20.3s

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:11):

finished :-)

view this post on Zulip Kenny Lau (May 11 2018 at 22:12):

wonderful

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:13):

set_option class.instance_max_depth 75

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:13):

This is just for one lemma.#

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:13):

Obviously my code might be crappy

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:13):

Will this whole system really scale?

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:14):

max depth 72 is the min for which the code compiles

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:15):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 22:15):

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

view this post on Zulip Andrew Ashworth (May 11 2018 at 23:38):

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

view this post on Zulip Kevin Buzzard (May 11 2018 at 23:52):

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.

view this post on Zulip Mario Carneiro (May 11 2018 at 23:59):

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

view this post on Zulip Mario Carneiro (May 12 2018 at 00:00):

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

view this post on Zulip Mario Carneiro (May 12 2018 at 00:00):

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

view this post on Zulip Johan Commelin (May 12 2018 at 04:55):

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

view this post on Zulip Johan Commelin (May 12 2018 at 04:56):

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

view this post on Zulip Kevin Buzzard (May 12 2018 at 09:34):

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.

view this post on Zulip Patrick Massot (May 12 2018 at 15:00):

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

view this post on Zulip Patrick Massot (May 12 2018 at 15:00):

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

view this post on Zulip Patrick Massot (May 12 2018 at 15:00):

The issue is to figure out what is the right infrastructure

view this post on Zulip Patrick Massot (May 12 2018 at 15:01):

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

view this post on Zulip Patrick Massot (May 12 2018 at 15:01):

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

view this post on Zulip Patrick Massot (May 12 2018 at 15:02):

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

view this post on Zulip Patrick Massot (May 12 2018 at 15:04):

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)

view this post on Zulip Kevin Buzzard (May 12 2018 at 16:51):

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/

view this post on Zulip Johan Commelin (May 12 2018 at 17:24):

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

view this post on Zulip Johan Commelin (May 12 2018 at 17:24):

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...

view this post on Zulip Johan Commelin (May 12 2018 at 17:25):

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

view this post on Zulip Johan Commelin (May 12 2018 at 17:25):

But one could imagine a rigged up version.

view this post on Zulip Kevin Buzzard (May 12 2018 at 17:53):

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.

view this post on Zulip Patrick Massot (May 13 2018 at 20:11):

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

view this post on Zulip Patrick Massot (May 13 2018 at 20:11):

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

view this post on Zulip Patrick Massot (May 13 2018 at 20:12):

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

view this post on Zulip Patrick Massot (May 13 2018 at 20:13):

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

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 11:26):

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 XX is compact then X×YYX\times Y\to Y is closed for all YY, 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?

view this post on Zulip Sebastian Ullrich (Feb 29 2020 at 11:32):

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.

view this post on Zulip Kevin Buzzard (Feb 29 2020 at 12:23):

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]?


Last updated: May 18 2021 at 16:25 UTC