Zulip Chat Archive

Stream: new members

Topic: Using analysis/calculus/deriv.lean a bottleneck


view this post on Zulip Daniel Keys (Feb 11 2020 at 18:52):

Hi all: I've been trying to get started using this:

import data.real.basic
import analysis.calculus.deriv

def twoX (x : ) :  := x + x
#check twoX
#check has_deriv_at
#check has_deriv_at twoX (2:)

Lean seems to become angry. It took several good minutes for the imports to load on a Macbook (one could easily get fried eggs on it after that), then for a couple seconds I did see the check passed, then I got this:

checkDerivatives.lean:6:0: error
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold)

Should I increase that memory threshold - and if yes how?

view this post on Zulip Johan Commelin (Feb 11 2020 at 18:53):

Probably you haven't compiled mathlib

view this post on Zulip Johan Commelin (Feb 11 2020 at 18:54):

So it's starting to do a whole bunch of compilations when you open that file.

view this post on Zulip Johan Commelin (Feb 11 2020 at 18:54):

@Daniel Keys Is this file in a project that depends on mathlib? Or are you working directly on a clone of mathlib?

view this post on Zulip Johan Commelin (Feb 11 2020 at 18:55):

In the first case, run update-mathlib. In the second case cache-olean --fetch.

view this post on Zulip Daniel Keys (Feb 11 2020 at 19:06):

@Johan Commelin I did set up the project directory with mathlib. So I suppose I should do update-mathlib. I did do that a couple of times in the directory though, but it was some time ago. How often does it need to be done? Thank you!

view this post on Zulip Daniel Keys (Feb 11 2020 at 19:10):

@Johan Commelin Actually just did it again and still have the same problem.

view this post on Zulip Daniel Keys (Feb 11 2020 at 19:14):

And when trying the other command I get: Your repo is dirty; fetching in this state could cause you to lose data.
Which I don't understand, since all my editors are closed. I'm not too much of a GitHub user, maybe there's something I need to do regularly when editing or creating new files.

view this post on Zulip Rob Lewis (Feb 11 2020 at 19:16):

When you see this message in VSCode, what files do you have open in tabs?

view this post on Zulip Rob Lewis (Feb 11 2020 at 19:17):

Try closing everything besides the file you're working on, and restart the Lean server (ctrl-shift-p, start typing "lean: restart").

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:14):

I didn't see this in Lean, but at the terminal prompt upon typing cache-olean --fetch. My VS Code was closed, and I had no files open in other editors.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:18):

Now I just restarted, I have only one file open in Lean which reads:

import data.real.basic
import analysis.calculus.deriv

def twoX (x : ) :  := x + x
#check twoX
#check has_deriv_at
#check has_deriv_at twoX (2:)

and my computer is going nuts again.

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:20):

I meant for the original issue with the recompiling, not the cache-olean error. If you're not working directly in a mathlib repository, cache-olean isn't the right script to use.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:20):

Even then, I was only using the same file

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:20):

Delete everything after the imports and restart the server like I described above. Is the CPU still going at it?

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:21):

And I do work in a mathlib directory. Yes, I just did that and it's going crazy

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:21):

Maybe set up a new, fresh directory?

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:22):

You said before

I did set up the project directory with mathlib

Is the repository you're working in a clone of mathlib, or is it using mathlib as a dependency?

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:22):

i.e., what's in the leanpkg.toml file?

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:23):

I didn't know of a difference between the two. Here's the .toml:

[package]
name = "ProofByInduction"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "585e107f9811719832c6656f49e1263a8eef5380"}

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:26):

That's fine. You're just using mathlib as a dependency. cache-olean is for when you're working directly on mathlib.

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:26):

What's the output when you run update-mathlib?

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:27):

Here it is:

update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Reusing cached olean archive
Extracting nightly...

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:29):

Try running find _target | grep "[.]olean$" | xargs touch

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:29):

Then restart the Lean server in VSCode.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:29):

Run this in the terminal?

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:29):

Yep.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:31):

OK. Seems to work. Can you elaborate a bit on what was happening?

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:35):

Ugh. It's an unfortunate "feature." olean files are compiled versions of lean files. The update-mathlib script downloads olean files for all of mathlib so you don't need to compile it yourself, which takes ages. But there's one olean per lean file, and one of the tests Lean does to make sure olean files are compatible is to check the timestamps. If file 2 imports file 1 but olean 2 is older than olean 1, olean 2 (and the olean for any lean file that imports lean 2) is invalid.

view this post on Zulip Johan Commelin (Feb 11 2020 at 20:36):

Somehow your system must have updated timestamps on your lean files, or given the olean files old timestamps.

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:36):

Sometimes the timestamps end up wrong after unpacking.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:37):

OK. So if this happens again, the same solution, right?

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:37):

Yes, but there really needs to be a more permanent solution, it's super annoying.

view this post on Zulip Rob Lewis (Feb 11 2020 at 20:38):

I'm actually not certain if the problem is with comparing .olean timestamps with each other, or comparing the .olean timestamps to the corresponding .lean timestamps.

view this post on Zulip Daniel Keys (Feb 11 2020 at 20:39):

Thank you all!

view this post on Zulip Kevin Buzzard (Feb 11 2020 at 23:15):

Remember -- Lean is a project, not a product. We work around things. Over the last couple of years the community has seen a lot of funny little issues, most have been fixed, and those that haven't have now got workarounds. I appreciate it can be daunting for the beginner. But the software is usable once you get to know its quirks :-)

view this post on Zulip Daniel Keys (Feb 11 2020 at 23:17):

Agreed. It's lots of fun too! I just wish I could devote more time, but either way I'd be blown away without the help here.

view this post on Zulip Floris van Doorn (Feb 11 2020 at 23:31):

It's an unfortunate "feature."

Would it be possible to just remove this feature in the community fork?

view this post on Zulip Floris van Doorn (Feb 11 2020 at 23:32):

Or is this same feature responsible for recompiling the library if I change a .lean file?

view this post on Zulip Rob Lewis (Feb 11 2020 at 23:32):

https://github.com/leanprover-community/lean/issues/112

view this post on Zulip Rob Lewis (Feb 11 2020 at 23:32):

I don't know the details myself, hoping someone more familiar will chime in.


Last updated: May 13 2021 at 17:42 UTC