unexpectedly long

Stream: general

[Kenny Lau]

import data.finset

open finset lattice

set_option profiler true

variables {α : Type*} {β : Type*} {s : finset β} {f : β → α} [semilattice_sup_bot α]

lemma sup_le {a : α} : (∀b ∈ s, f b ≤ a) → s.sup f ≤ a :=
by letI := classical.dec_eq β; from
finset.induction_on s (λ _, bot_le) (by simp {contextual := tt})
-- why so long?

[Kenny Lau]

takes somewhere between 5s and 30s to compile

[Simon Hudon]

Is the time spent on simp?

[Kenny Lau]

I think so

[Kenny Lau]

btw that's finset.sup_le

[Kenny Lau]

that's right, a 10s-lemma is inside mathlib

[Simon Hudon]

I'm planning on writing a tactic today squeeze_simp that will call simp and print a minimized simp only version. That might help in your endeavor

[Simon Hudon]

I can automate the application of the suggestion in emacs but I don't know how to do the same with VS code

[Johan Commelin]

Register it as a hole command, like tidy does.

[Simon Hudon]

Is that a mechanism of VS Code?

[Johan Commelin]

No, it's a Lean thing

[Johan Commelin]

I think it is a type class

[Johan Commelin]

But I guess IDE's also have to hook into it. But this is a one time thing that has been done already

[Simon Hudon]

Thanks! I'm looking at the tidy code, it's actually an attribute

[Simon Hudon]

Cool

[Reid Barton]

Simon have you determined yet whether the emacs mode already supports hole commands? I haven't looked

[Johan Commelin]

I thought emacs always supported the supremum of the features of all other IDE's
By definition

[Simon Hudon]

It is indeed emacs definition

[Simon Hudon]

It does support hole commands, at least three that I have seen

[Johan Commelin]

Since tidy there should be 4

[Simon Hudon]

I confirm that I can now see tidy in that list too

[Simon Hudon]

I like the idea of the type hole but it has a down side: if you're replacing simp in a file, you have to do it one at a time.

[Reid Barton]

Aha I see, I have to be inside the hole and then invoke lean-hole.

[Reid Barton]

I misunderstood the docstring "Ask Lean for a list of holes, then ask the user which to use."

[Johan Commelin]

@Simon Hudon Agreed. Still it could be nice for the future. Because then one can use it during the golfing phase of a proof that one just finished.

[Johan Commelin]

For squeezing entire files you might not even want to focus on editor integration.

[Simon Hudon]

I agree with your first point Johan. For the second point, the reason I'm thinking about editor integration is out of laziness. The slow files are really big and applications of simp vary a lot so search and replace alone doesn't cut it

[Johan Commelin]

Ok, fair enough

[Simon Hudon]

What I want to do is search and replace simp (not preceded by a square bracket) with squeeze_simp which will output all the required substitutions with line numbers and then emacs can do a very targeted replacement of all the squeeze_simp

[Simon Hudon]

But now that I know about hole_command attributes, I think I might start with that to test out my idea