Animation of elaboration

Stream: general

[Heather Macbeth]

For a talk, I made an animation of the elaboration of this definition (which is a toy model for Mathlib's docs#ContinuousLinearMap.adjoint). It is a time-lapse of the assignment of metavariables.

elaboration.gif

[Bhavik Mehta]

This is really nice! Is the information about how elaboration proceeds here extracted from something Lean is actually doing? If so, can you share how you extracted it?

[Heather Macbeth]

Thanks! Yes, I went through the output of trace.profiler to get this. The information isn't available directly but I was able to guess it. For example, from

[Elab.step] [0.001040] expected type: LinearIsometryEquiv ?m.1450 ?m.1451 ?m.1453, term
    postcompose _ _ (compose (riesz F) (postcompose _ _ conj))

...

  [Meta.isDefEq] [0.000073] ✅️ LinearIsometryEquiv ?m.1450 ?m.1451
        ?m.1453 =?= LinearIsometryEquiv (LinearMap ?m.1465 ?m.1466 ?m.1468) (LinearMap ?m.1465 ?m.1467 ?m.1470)
        ?m.1469

(which was the first appearance of the metavariables ?m.1465, ?m.1466, ?m.1467, ?m.1468, ?m.1469 and ?m.1470) I guessed that those metavariables were created as placeholders on the top left usage of postcompose, and that the first thing happening there was that it was being unified with the pattern coming from its parent in the tree. Same ideas to guess the "position" for all the other metavariables.

A few lines later we have

[Meta.isDefEq.assign] [0.000006] ✅️ ?m.1465 := E
[Meta.isDefEq.assign] [0.000005] ✅️ ?m.1466 := F
[Meta.isDefEq.assign] [0.000005] ✅️ ?m.1468 := pos
[Meta.isDefEq.assign] [0.000012] ✅️ ?m.1451 := LinearMap ?m.1465 ?m.1467 ?m.1470
[Meta.isDefEq.assign] [0.000005] ✅️ ?m.1453 := ?m.1469

showing that that particular unification step resulted in the assignment of the metavariables ?m.1465, ?m.1466, ?m.1468, ?m.1451, ?m.1453. I tracked this kind of thing throughout by extracting the full list of Meta.isDefEq.assign steps.

Finally I subtracted 1450 from every metavariable's name so that the numbers were smaller :-)

[Heather Macbeth]

I had asked last week about tracing this, and it indeed seems that there is no direct tool, but I got a lot of hints about using the profiler better.