obviously

Stream: general

[Reid Barton]

@Scott Morrison How can I recover the old behavior of obviously which did not trace the steps it took?
Perhaps the replaceable thing ought to be called cat_tactic or something, and obviously should return to its old behavior?

[Scott Morrison]

@Reid Barton, I've silenced the trace messages from obviously.

[Scott Morrison]

Moreover, yesterday Mario and I overhauled tidy from top to bottom. The code is much shorter and saner now. :-)

[Kevin Buzzard]

OK so there is something annoying about obviously. I've now used the category theory library a fair bit so I can say it's (a) good at closing the goals it should be closing and (b) slow. I've seen it take a minute to construct a tactic proof which runs in a second. Is it possible to somehow completely "factor out" obviously in a safe way? I want to be able to import a compiled file obviously.lean whose data changes if I change a file containing obviously or something, and which contains certificates for all the goals that obviously closes (maybe as axioms or something). And then you can occasionally obviously_check your file where it actually uses the tactic to generate all the proofs. If I want to restart Lean for some reason when working on a file with lots of obviouslys it's going to take some time, but Scott really doesn't want them visible to mathematicians because these goals really are obvious to mathematicians -- these are things a mathematician would not bother to justify in a blackboard lecture.

[Kevin Buzzard]

Can obviously say "Oh, you gave me this once before -- here's the answer I came up with last time and it worked fine. Do you want me to run it again? (y/N)"

[Patrick Massot]

This was all dreamed of before, but it requires deep changes to Lean. Maybe in Lean 4?

[Scott Morrison]

Keeley actually got exactly this to work in a (hacked) version of Lean 3... It's not that deep. He just needed fast io to a file.

[Mario Carneiro]

in that case, we may be in luck since we're rebranding "hacking lean" as "lean development"

[Scott Morrison]

Oh.. Keeley has already merged his hacks. They're officially not hacks anymore. :-)

[Scott Morrison]

Let me see if I can run his tactic block caching trickery now.

[Scott Morrison]

Okay, it's shockingly easy to use. Checkout #2300, and add import tactic.tcache.enable at the top of one of your files, and magically everything appears to compile faster.

[Scott Morrison]

(There's a bug: by X; Y blocks seem to make it choke.)