Using analysis/calculus/deriv.lean a bottleneck

Stream: new members

[Daniel Keys]

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?

[Johan Commelin]

Probably you haven't compiled mathlib

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Daniel Keys]

@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!

[Daniel Keys]

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

[Daniel Keys]

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.

[Rob Lewis]

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

[Rob Lewis]

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

[Daniel Keys]

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.

[Daniel Keys]

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.

[Rob Lewis]

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.

[Daniel Keys]

Even then, I was only using the same file

[Rob Lewis]

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

[Daniel Keys]

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

[Daniel Keys]

Maybe set up a new, fresh directory?

[Rob Lewis]

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?

[Rob Lewis]

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

[Daniel Keys]

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"}

[Rob Lewis]

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

[Rob Lewis]

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

[Daniel Keys]

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...

[Rob Lewis]

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

[Rob Lewis]

Then restart the Lean server in VSCode.

[Daniel Keys]

Run this in the terminal?

[Rob Lewis]

Yep.

[Daniel Keys]

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

[Rob Lewis]

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.

[Johan Commelin]

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

[Rob Lewis]

Sometimes the timestamps end up wrong after unpacking.

[Daniel Keys]

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

[Rob Lewis]

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

[Rob Lewis]

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.

[Daniel Keys]

Thank you all!

[Kevin Buzzard]

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 :-)

[Daniel Keys]

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.

[Floris van Doorn]

It's an unfortunate "feature."

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

[Floris van Doorn]

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

[Rob Lewis]

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

[Rob Lewis]

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