## Stream: new members

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

#### 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?

#### Johan Commelin (Feb 11 2020 at 18:53):

Probably you haven't compiled mathlib

#### Johan Commelin (Feb 11 2020 at 18:54):

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

#### 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?

#### Johan Commelin (Feb 11 2020 at 18:55):

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

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

#### Daniel Keys (Feb 11 2020 at 19:10):

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

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

#### Rob Lewis (Feb 11 2020 at 19:16):

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

#### 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").

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

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

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

#### Daniel Keys (Feb 11 2020 at 20:20):

Even then, I was only using the same file

#### 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?

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

#### Daniel Keys (Feb 11 2020 at 20:21):

Maybe set up a new, fresh directory?

#### 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?

#### Rob Lewis (Feb 11 2020 at 20:22):

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

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


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

#### Rob Lewis (Feb 11 2020 at 20:26):

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

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


#### Rob Lewis (Feb 11 2020 at 20:29):

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

#### Rob Lewis (Feb 11 2020 at 20:29):

Then restart the Lean server in VSCode.

#### Daniel Keys (Feb 11 2020 at 20:29):

Run this in the terminal?

Yep.

#### Daniel Keys (Feb 11 2020 at 20:31):

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

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

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

#### Rob Lewis (Feb 11 2020 at 20:36):

Sometimes the timestamps end up wrong after unpacking.

#### Daniel Keys (Feb 11 2020 at 20:37):

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

#### Rob Lewis (Feb 11 2020 at 20:37):

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

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

Thank you all!

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

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

#### 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?

#### 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?

#### Rob Lewis (Feb 11 2020 at 23:32):

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

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