Zulip Chat Archive

Stream: general

Topic: caching proofs


view this post on Zulip Scott Morrison (Sep 18 2018 at 07:25):

So I'm moving it here.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:25):

From https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/subject/caching.20proofs/near/134150221

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:25):

Thanks.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:26):

Yes, that second pass is just unavoidably slow.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:26):

So I'm fine if Travis does that, and I never do it.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:26):

But I think there's still useful information for the user in seeing the first pass succeed.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:26):

Or almost never...

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:26):

Yes.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:26):

What exactly are you guys referring to when you say “proof cache”?

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:26):

The point of course is to get back as quickly as possible to responsive editing.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:27):

(For us poor idiots who use interactive mode, and can't, like some people here, write Lean code while offline. :-)

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:27):

Of course, olean files _are_ a proof cache.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:28):

So the idea might be merely this:

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:28):

if Lean notices that an olean file is outdated (i.e. the source file, or a dependency source file, is newer)

view this post on Zulip Patrick Massot (Sep 18 2018 at 07:28):

Do you know about https://github.com/leanprover/lean/issues/1601? Fixing this issue is part of the Lean 4 plan ifI understand correctly

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:28):

before disposing of the olean file it loads it one last time

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:29):

and tries to use existing proofs for the current set of lemmas, ignoring on the first pass the actual proof term written in the source file (whether generated in term or tactic mode)

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:29):

but of course eventually there does have to be a second pass that reverifies what the user has written and constructs a new olean.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 07:30):

(For us poor idiots who use interactive mode, and can't, like some people here, write Lean code while offline. :-)

Q1 What's "offline"? Q2 why can't you write code offline? What is interactive mode?

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:32):

I think "offline" here means: Writing code without Lean responding to what you write. (Just using your internal elaborater/kernel to verify your own code.)

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 07:33):

eew.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:33):

In particular @Simon Hudon appears to have written working code for me without ever running Lean...!

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:34):

(Sometimes I've been able to tell because of some minor typo, meaning it just barely missed actually compiling. :-)

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:34):

In Orsay I witnessed Mario writing half a proof while Lean was thinking. He didn't need to go back and change those 5 lines after Lean caught up with him.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:34):

It's terrifying, isn't it? :-)

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:34):

Yellow bars just cause my brain to freeze up. :-)

view this post on Zulip Sean Leather (Sep 18 2018 at 07:36):

I don't use interactive mode, so I just see walls of errors, not yellow bars.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:37):

I don't use interactive mode, so I just see walls of errors, not yellow bars.

Wait... do you mean that you write Lean the way I would write C or Python?

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:38):

Edit file → Save → Compile/run the file in terminal → Parse errors → Go back to step 1

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:38):

Well... presumably he doesn't actually ever execute any code.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:38):

Yep.

view this post on Zulip Scott Morrison (Sep 18 2018 at 07:38):

Well, Sean might, actually. :-)

view this post on Zulip Sean Leather (Sep 18 2018 at 07:38):

:big_smile:

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:38):

Aaahrg... :scream: you guys are really crazy...

view this post on Zulip Sean Leather (Sep 18 2018 at 07:40):

Anyway, I'm not sure if it's the same problem as in interactive mode: I'd like to speed up lean --make.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:40):

So, it would be nice if I had all of the generated proof terms for, say, mathlib. So, if I make one change, lean doesn't have to recheck entire files.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:40):

I guess it is the same bottleneck that we are hitting.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:41):

On the other hand, as Scott said, one small change can change tactics. But I think that should be checked at “release” time.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:41):

... as opposed to “interactive” time.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:41):

So, at the very least, I know proof works. But I may need to go back and check a tactic somewhere afterwards.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:42):

I envision it like having a --fast mode and a --release mode. Names up for debate.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:43):

We already have trust levels...

view this post on Zulip Sean Leather (Sep 18 2018 at 07:43):

Or --fast and --full to use alliteration.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:43):

How do trust levels come into the picture here?

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:43):

Well, you are putting "trust" in the cache, right?

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:44):

I could envision a new trust level, that will trust cached proofs.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:44):

Does that make sense?

view this post on Zulip Sean Leather (Sep 18 2018 at 07:44):

Perhaps. I don't have a clear picture of what that means.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:45):

I'm not thinking of trust. I'm thinking of checking only what changed within a single file (to simplify the problem).

view this post on Zulip Sean Leather (Sep 18 2018 at 07:49):

Here's something that doesn't work for all changes, but might work for some: run a quick pass over the interfaces of a file's cached proof terms, check if they differ from the source file, build the ones that differ or are not found in the cache.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:50):

After that, perhaps you could more lazily regenerate the other proof terms of the file.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:52):

Also, perhaps the generated proof cache could keep track of failed proofs and Lean would try to rebuild those first.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:52):

That might improve interactive responsiveness.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:53):

I wouldn't mind if Lean did low-priority (in the sense of CPU scheduler) checks to see if my new @[simp] lemma broke a proof by tidy in some files that I didn't have open. But as soon as I make a change in my file the --fast Lean should do a high-priority check to get me back to responsive editing as soon as possible.

view this post on Zulip Sean Leather (Sep 18 2018 at 07:55):

Yeah, that's the idea, though I was actually thinking --fast wouldn't even try to check the effect of @[simp] lemmas or other things that change how tactics work. But I could see it going either way.

view this post on Zulip Johan Commelin (Sep 18 2018 at 07:55):

Do you know about https://github.com/leanprover/lean/issues/1601? Fixing this issue is part of the Lean 4 plan ifI understand correctly

That definitely looks relevant! Thanks @Patrick Massot

view this post on Zulip Sean Leather (Sep 18 2018 at 07:58):

Here are two possibilities:

1. An interactive mode that optimizes for checking work-in-progress proofs and reduces the priority of full-file and full-library builds.
2. A fast mode that only checks for work-in-progress proofs and builds a single file at a time and a full mode that builds everything.

view this post on Zulip Simon Hudon (Sep 18 2018 at 23:40):

@Sean Leather Isn't that already what the ideas do? I feel like lean-mode does it at least.

@Scott Morrison I do use the interactive modes but sometimes I'm too lazy to go back to emacs to write my code snippets. I'm glad I don't have too bad a track record :)

view this post on Zulip Sean Leather (Sep 19 2018 at 05:40):

Isn't that already what the ideas do? I feel like lean-mode does it at least.

@Simon Hudon What are “the ideas”?

I don't know exactly what does what, so I'm just throwing out some thoughts. I do know that if I make a change in a large file in mathlib and build with lean --make, I see that the entire file has to be built before it gets to my change. That's what I would propose improving.

As I said above, I don't use the interactive approach, and I don't know if the problem I have is the same problem others are discussing.

view this post on Zulip Simon Hudon (Sep 19 2018 at 06:25):

I misspelled IDE

view this post on Zulip Simon Hudon (Sep 19 2018 at 06:25):

So what is your workflow like if you don't use them?

view this post on Zulip Sean Leather (Sep 19 2018 at 06:26):

Edit in vim, run leanpkg build.

view this post on Zulip Simon Hudon (Sep 19 2018 at 06:52):

That sounds painful

view this post on Zulip Sean Leather (Sep 19 2018 at 06:53):

:shrug: Works well for me.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 06:55):

I print the files out, cross out some lines in pencil and add others in, then compile in my head.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 06:55):

that's how we did it in the old days before computers

view this post on Zulip Sean Leather (Sep 19 2018 at 06:56):

How did you print files without computers? :computer: :right: :printer:

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 06:56):

I use my typewriter

view this post on Zulip Sean Leather (Sep 19 2018 at 06:56):

Oh, they usually refer to that as typing, not printing, right?

view this post on Zulip Johan Commelin (Sep 19 2018 at 06:56):

He has a printing press à la Gutenberg in his cellar (-;

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 06:56):

I guess they call it that nowadays.

view this post on Zulip Simon Hudon (Sep 19 2018 at 06:58):

Amateurs. Here's my workflow: https://xkcd.com/378/

view this post on Zulip Johan Commelin (Sep 19 2018 at 07:03):

C-x M-c M-butterfly

view this post on Zulip Simon Hudon (Sep 19 2018 at 17:40):

@Sean Leather I think this is a case in which, before you see what you're missing out on, you don't know that you're missing out. I find it incredibly useful when writing tactic that, as I type and change my scripts, I can see the print out of the example I'm using the tactic on. That save a whole lot of time


Last updated: May 16 2021 at 20:13 UTC