Zulip Chat Archive

Stream: general

Topic: obviously


Reid Barton (Aug 23 2018 at 03:21):

@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 (Aug 24 2018 at 09:03):

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

Scott Morrison (Aug 25 2018 at 15:08):

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

Kevin Buzzard (Mar 31 2020 at 11:50):

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 (Mar 31 2020 at 11:51):

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 (Mar 31 2020 at 11:55):

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

Scott Morrison (Mar 31 2020 at 12:56):

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 (Mar 31 2020 at 13:06):

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

Scott Morrison (Mar 31 2020 at 13:40):

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

Scott Morrison (Mar 31 2020 at 13:40):

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

Scott Morrison (Mar 31 2020 at 14:19):

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 (Mar 31 2020 at 14:19):

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


Last updated: Dec 20 2023 at 11:08 UTC