checking imports

Stream: general

[Jakob von Raumer]

whenever I open vscode, lean seems to re-check all imported files... wasn't this better some time ago?

[Jakob von Raumer]

(my issue here is that I need to close all other programs, to check some imports from the hott3 library, they use up almost all of my RAM)

[Chris Hughes]

Did you run leanpkg build in the appropriate directory?

[Jakob von Raumer]

Nope, shame on my, kind of assumed that vscode would somehow invoke that... :grinning_face_with_smiling_eyes:

[Jakob von Raumer]

Uhm, and leanpkg build also doesn't eat all of my RAMs :ram:

[Jakob von Raumer]

But unfortunately it doesn't change the fact that vscode checks everything at startup, even after a successful leanpkg build...

[Johan Commelin]

Are you using elan? Did you run leanpkg build in the root of your project, or in a subdir?

[Jakob von Raumer]

In the root dir... What is elan?

[Johan Commelin]

Ok, you are not using elan.

[Johan Commelin]

Kevin wrote this page today: https://xenaproject.wordpress.com/installing-lean-and-mathlib/

[Johan Commelin]

Jakob, how did you install lean and mathlib?

[Jakob von Raumer]

Lean: Using the sources

[Jakob von Raumer]

Mathlib: Not sure if I have it at all... but hott3 doesn't depend on it, does it?

[Jakob von Raumer]

Oh, there's a global installation of mathlib at ~/.lean/_target/deps

[Johan Commelin]

Hmmm... I don't really know enough to help you here.

[Rob Lewis]

You have fresh .olean files in your Lean root directory, right? What exactly are you opening in VS Code?

[Jakob von Raumer]

What's my lean root directory? I'm opening the folder of a project of mine in VS, which references hott3 in its .toml

[Rob Lewis]

Wherever you built the executable. If the executable lies in lean/bin/, then you should also have lean/library/ with the core lib. The .lean files there should have fresh .olean files. In your project folder, do you have _target/deps/hott3? Are there olean files in there?

[Rob Lewis]

And are there compilation errors when you run leanpkg build?

[Jakob von Raumer]

Yes there's .olean files in _target/deps/hott3 and not so fresh ones in lean/library... leanpkg buid goes through with warning but no errors.

[Jakob von Raumer]

Hm, but if I run leanpkg build in ~/.lean, I get loads of errors

[Jakob von Raumer]

Oh, that's because stuff is not in LEAN_PATH

[Jakob von Raumer]

Hu, but lean --path gives all I would expect...

[Jakob von Raumer]

Should leanpkg build build all the deps or just the files needed?

[Patrick Massot]

only needed

[Jakob von Raumer]

Thanks.

[Jakob von Raumer]

And should it build files that haven't changed since the last build?

[Jakob von Raumer]

If there's only deps and no actual content in ~/.lean, how come leanpkg build does anything at all, if I execute it there? :confused:

[Gabriel Ebner]

Forget about ~/.lean, it's independent and not used in this case (check lean -p, if it doesn't appear you don't need to worry about it).
The easiest way to ensure all olean files are built is to run lean --make in the project folder.
(You should also open the project folder in vscode (not a subfolder or superfolder), but I don't think that's the problem here.)

[Jakob von Raumer]

Now it works :shrug: Not sure what was wrong. I did a rebuild of lean itself

[Patrick Massot]

Why do you build Lean?

[Jakob von Raumer]

I noticed it's been a while since I last built it

[Patrick Massot]

Why building it at all? What's wrong with the distributed binaries? Are you modifying Lean?

[Jakob von Raumer]

I used to, ages ago. Before most of the library was moved to mathlib... I guess I could as well use the binaries now.

[Scott Morrison]

Yeah, while Lean itself is stable at the moment, all the instructions people are giving assume you're using a binary (ideally provided by elan). lean --make in the library/ directory of a built-from-sources copy of Lean can help with the issue you were experiencing.