Zulip Chat Archive

Stream: general

Topic: checking imports


Jakob von Raumer (Oct 10 2018 at 16:59):

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

Jakob von Raumer (Oct 10 2018 at 17:01):

(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 (Oct 10 2018 at 17:09):

Did you run leanpkg build in the appropriate directory?

Jakob von Raumer (Oct 10 2018 at 17:24):

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

Jakob von Raumer (Oct 10 2018 at 17:25):

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

Jakob von Raumer (Oct 10 2018 at 17:30):

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

Johan Commelin (Oct 10 2018 at 17:31):

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

Jakob von Raumer (Oct 10 2018 at 17:33):

In the root dir... What is elan?

Johan Commelin (Oct 10 2018 at 17:35):

Ok, you are not using elan.

Johan Commelin (Oct 10 2018 at 17:35):

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

Johan Commelin (Oct 10 2018 at 17:35):

Jakob, how did you install lean and mathlib?

Jakob von Raumer (Oct 10 2018 at 17:45):

Lean: Using the sources

Jakob von Raumer (Oct 10 2018 at 17:45):

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

Jakob von Raumer (Oct 10 2018 at 17:46):

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

Johan Commelin (Oct 10 2018 at 17:54):

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

Rob Lewis (Oct 10 2018 at 18:00):

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

Jakob von Raumer (Oct 10 2018 at 18:31):

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 (Oct 10 2018 at 18:44):

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 (Oct 10 2018 at 18:44):

And are there compilation errors when you run leanpkg build?

Jakob von Raumer (Oct 10 2018 at 19:09):

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 (Oct 10 2018 at 19:11):

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

Jakob von Raumer (Oct 10 2018 at 19:12):

Oh, that's because stuff is not in LEAN_PATH

Jakob von Raumer (Oct 10 2018 at 19:18):

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

Jakob von Raumer (Oct 10 2018 at 19:29):

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

Patrick Massot (Oct 10 2018 at 19:30):

only needed

Jakob von Raumer (Oct 10 2018 at 19:32):

Thanks.

Jakob von Raumer (Oct 10 2018 at 19:33):

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

Jakob von Raumer (Oct 10 2018 at 19:39):

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 (Oct 10 2018 at 20:00):

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 (Oct 10 2018 at 20:20):

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

Patrick Massot (Oct 10 2018 at 20:21):

Why do you build Lean?

Jakob von Raumer (Oct 10 2018 at 20:23):

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

Patrick Massot (Oct 10 2018 at 20:25):

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

Jakob von Raumer (Oct 10 2018 at 20:27):

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 (Oct 10 2018 at 22:08):

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.


Last updated: Dec 20 2023 at 11:08 UTC