import data.ratl OOM

Stream: new members

[Kunwar Shaanjeet Singh Grover]

Hi! I'm new to lean and I setup VScode with Lean extension. I have a program which only does

import data.rat

which causes VSCode to start multiple lean servers (I see multiple lean --server processes) for some reason, eventually going OOM. Is there anything I can do to fix this?

[Patrick Massot]

Hi. We'll need more information about what you did to setup everything. Did you follow the instructions at https://leanprover-community.github.io/get_started.html#regular-install or some other source?

[Kunwar Shaanjeet Singh Grover]

Thank you for the quick reply! I installed it using the script given here: https://leanprover-community.github.io/install/debian.html

[Kunwar Shaanjeet Singh Grover]

Im on Lean (version 3.38.0, commit a8cf8a0c9ea1, Release) if that's useful.

[Patrick Massot]

That's a very good first step. Did you then follow the link at the bottom of that page?

[Patrick Massot]

Leading to https://leanprover-community.github.io/install/project.html

[Kunwar Shaanjeet Singh Grover]

I did check it. Since I have an existing project, I just launched vscode and it told me "leanpkg.path" does not exist. So i clicked on "Run leanpkg configure". I think that installed mathlib in "_target" and it messed it up after that.

[Patrick Massot]

How did you get that existing project?

[Patrick Massot]

Or how did you create it?

[Kunwar Shaanjeet Singh Grover]

It's from a school project :) It has a leanpkg.toml file and a .lean file.

[Patrick Massot]

Could you paste leanpkg.toml here, just to make sure?

[Kunwar Shaanjeet Singh Grover]

sure!

[Kunwar Shaanjeet Singh Grover]

[package]
name = "basic"
version = "0.1"
lean_version = "leanprover-community/lean:3.38.0"
path = "src"

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

[Patrick Massot]

In the folder containing that file, please run leanproject get-mathlib-cache

[Patrick Massot]

And then try code . (still in that folder)

[Kunwar Shaanjeet Singh Grover]

Hey, that worked! Thank you!

[Kunwar Shaanjeet Singh Grover]

Any idea why the previous approach was not working?

[Patrick Massot]

Yes, it's partly our fault. The section "Working on an existing project" assumes you will get your project from GitHub using leanproject get. It seems that's no what you did.

[Patrick Massot]

So you didn't get a compiled mathlib

[Patrick Massot]

We should probably add explanations about this use case to this webpage.

[Patrick Massot]

Have fun with Lean!

[Kunwar Shaanjeet Singh Grover]

Thank you for the help!