Tips how to speed up elaboration

Stream: general

[Kevin Buzzard]

If, on average, I have to wait 10 seconds after writing every line of proof,

If my students are waiting 10 seconds after writing every line of proof, I tell them that they're probably doing it wrong. There is a possibility that you're doing it right, but the common errors I see with my students which cause this are: (1) writing one 100 line long proof instead of ten 10 line long proofs (i.e. not refactoring out as much as possible) (2) using expensive tactics early on in a proof rather than to finish it (common culprits are finish, and non-terminal simps which should be squeezed).

[Martin Dvořák]

Kevin Buzzard said:

(1) writing one 100 line long proof instead of ten 10 line long proofs (i.e. not refactoring out as much as possible)
(2) using expensive tactics early on in a proof rather than to finish it (common culprits are finish, and non-terminal simps which should be squeezed).

I'm guilty of (1) but I definitely avoid (2).

[Kevin Buzzard]

In Lean 4 I think there's some kind of way of freezing state in the middle of a proof and always starting there (the way the Coq people work). If you insist on writing long proofs and you're using Lean 4 then you might want to figure out how to do this.

[Martin Dvořák]

I haven't needed to write long proofs in Lean 4 yet, but I wrote a lot of long proofs in Lean 3.

[Martin Dvořák]

For me, the price of refactoring is sometimes too high. Especially when the statement itself takes like 4 lines to write.

[Sebastien Gouezel]

You can obtain a big boost by sorrying intermediate statements in long proof. Say you have a proof with

  have A : foo = bar,
  { ...
    a pretty complicated proof of 20 lines },
  have B : baz = tue,
  { ...
     another long proof },
  have C : ...

and you feel that you editor is not really responsive when proving C. Change for the time being your proof to

  have A : foo = bar,
  sorry { ...
    a pretty complicated proof of 20 lines },
  have B : baz = tue,
  sorry { ...
     another long proof },
  have C : ...

and when you're done with your proof, remove the sorry.

[Kevin Buzzard]

Are you suggesting that I cannot get significantly better performance than I currently have?

If you're writing 100 line proofs in Lean 3 then yes I'm suggesting that.

[Martin Dvořák]

I believe the best approach is to:
(1) refactor everything that can be refactored easily;
(2) when waiting too long, sorry the parts that can be sorried easily;
(3) have a strong computer that makes the remaining situations less painful.

I don't think I can do any of the above so well (to such extend) that it would suffice on its own.

[Martin Dvořák]

Kevin Buzzard said:

one 100 line long proof

In extreme cases, my proof can have 666 lines!
https://github.com/madvorak/grammars/blob/163b666befa19092a0f44527e95aabf25aba289f/src/classes/unrestricted/closure_properties/star.lean#L2267

[Martin Dvořák]

Kevin Buzzard said:

If you're writing 100 line proofs in Lean 3 then yes I'm suggesting that.

I want to point out that keeping long proofs (mostly in computer science theory) without refactoring them into many small proofs is not always a symptom of laziness. Sometimes I end up deciding between three options, all of which are bad:
(a) keeping one very long proof
(b) repeating long-to-state assumptions over and over again, in order to have many small proofs
(c) creating a lot of ad-hoc definitions that I have to unfold later

[Junyan Xu]

repeating long-to-state assumptions over and over again

can you not use variables and include for those?

[Eric Wieser]

666 lines feels awfully long

[Reid Barton]

I feel like long proofs are maybe a sign of not enough laziness

[Martin Dvořák]

Junyan Xu said:

can you not use variables and include for those?

Good idea! I will try to refactor that very long proof using variables and include as an exercise. I am not going to keep it in my "production code" because include goes against my coding standards, but it might be interesting to see whether my proof becomes more readable.

[Eric Wieser]

That seems like a pretty arbitrary standard to hold

[Eric Wieser]

If you dislike the action at a distance, you could use

section
include h

lemma my_lemma := by rw h
end

That way the scope of the include is just one lemma

[Eric Wieser]

But also #lint will tell you if you included things you didn't need anyway

[Martin Dvořák]

We talked about it before. I don't want to have variables (stuff) because then I don't see everything that has to be explicitly passed to a lemma in its declaration.

[Martin Dvořák]

I allow myself only variables {stuff} and variables [stuff] for this reason.

[Alex J. Best]

It will show up with the full info in docs or when hovering over the lemma in another proof, so it still seems quite a lot of extra work to only make things more explicit when looking at the source as a text file.

[Eric Wieser]

Frankly, a 666-line proof is likely much more of an impediment to text readability (assuming you care about that in the first place) than use of variables

[Eric Wieser]

I can point you to how to set up a docs webpage for your own repo if you're interested in that

[Martin Dvořák]

Alex J. Best said:

It will show up with the full info in docs or when hovering over the lemma in another proof, so it still seems quite a lot of extra work to only make things more explicit when looking at the source as a text file.

I always look at the source code. These auto-generated docs (if we are talking about the docs pages we usually refer to here) are hard for me to understand.

[Martin Dvořák]

Eric Wieser said:

Frankly, a 666-line proof is likely much more of an impediment to text readability (assuming you care about that in the first place) than use of variables

I care a lot about the readability on the outside.

[Martin Dvořák]

Eric Wieser said:

I can point you to how to set up a docs webpage for your own repo if you're interested in that

OK, I'll give it a try! Maybe it's time to change my working habits...

[Eric Wieser]

Martin Dvořák said:

These auto-generated docs (if we are talking about the docs pages we usually refer to here) are hard for me to understand.

This surprises me: the doc page is just the source code with the variables inlined and proof removed!

[Eric Wieser]

Isn't that what you mean by "the outside"?

[Kyle Miller]

I think Martin's mainly expressing a preference. I myself don't really like reading types in the generated docs either -- most times I find something relevant in the docs and then type it into my editor and use the mouseover to study it.

[Kyle Miller]

Regarding variables, I usually use them for implicit variables, and maybe have one or two explicit variables if I'm defining definitions/lemmas meant to be used with dot notation.

If there are complicated hypotheses that occur repeatedly, that for me is a signal that I need to rethink what I'm doing.

[Kyle Miller]

There's that joke about how mathematicians go to great lengths to be lazy (which I think Reid was referring to), but it's a lot of work to be lazy -- you have to come up with a whole theory so that what you want to say takes little effort.

[Eric Wieser]

Kyle Miller said:

I myself don't really like reading types in the generated docs either -- most times I find something relevant in the docs and then type it into my editor and use the mouseover to study it.

I often use the docs over vscode due to them not having as much [_inst_n : _] clutter. Is there something you can pinpoint your dislike of reading types on, that could be changed for the better?

[Kyle Miller]

Maybe it's two things, all the colors from the links make it visually busy, and the fact it's the "wrong" font (there's nothing actually wrong with it, it's just not the one in my editor).

[Kyle Miller]

Would there be a way to highlight the parentheses? Given what I know about the pretty printer, I don't think it would be straightforward, but it could help with scanning the type to know where each argument starts and ends.

[Kyle Miller]

I do like how the implicit arguments are in gray in the docs, and how the types are laid out with indentation.

[Martin Dvořák]

Kyle Miller said:

Regarding variables, I usually use them for implicit variables, and maybe have one or two explicit variables if I'm defining definitions/lemmas meant to be used with dot notation.

How can they be two?

[Martin Dvořák]

Kyle Miller said:

If there are complicated hypotheses that occur repeatedly, that for me is a signal that I need to rethink what I'm doing.

In computer science, you often have complicated invariants to describe what an arbitrary moment during your computation looks like.
There is not always an opportunity to rethink that (I mean, you can rethink whatever you want to rethink, but there might be nothing to gain from rethinking it). Sometimes you can choose a different algorithm to solve the problem. Sometimes you can simplify the invariant. However, in most remaining cases, you just have to prove that every operation preserves the invariant. That takes time (and lines) to do.

For this reason, I don't think that repeating complicated hypotheses is immediately a code smell.

[Martin Dvořák]

Kyle Miller said:

Maybe it's two things, all the colors from the links make it visually busy, and the fact it's the "wrong" font (there's nothing actually wrong with it, it's just not the one in my editor).

This is probably my problem as well. Thank you for putting your finger on it!

Even if I can parse the docs, it feels a bit "unreal". So I rather open the Lean code. If I see the same thing written in Lean, it feels more real/believable and makes me confident that I can refer to it from my code. This is clearly an irrational feeling. Nevertheless, it makes me uncomfortable to the extend that I prefer to read the Lean code even if it means much more scrolling than getting the same info from the docs.

[Eric Wieser]

Perhaps you're already aware of this, but; the feeling of unrealness reduces slightly if you use the dark-mode docs (assuming you use the dark vscode theme)

[Martin Dvořák]

I had no idea I can change color of the docs page!

[Martin Dvořák]

Kyle Miller said:

There's that joke about how mathematicians go to great lengths to be lazy (which I think Reid was referring to), but it's a lot of work to be lazy -- you have to come up with a whole theory so that what you want to say takes little effort.

On the same note: https://www.techinasia.com/talk/3-great-virtues-of-a-programmer-laziness-impatience-and-hubris

[Eric Wieser]

Martin Dvořák said:

I had no idea I can change color of the docs page!

For anytime else reading; the option is at the bottom of the left sidebar