## Stream: new members

### Topic: mathlib installation

#### Iocta (Mar 19 2020 at 03:03):

I have a file that contains only import data.set. Getting tons of these messages:

 lap.12.0.…     1   1 error           invalid import: tactic.library_note
excessive memory consumption detected at 'vm' (potential solution: increase memory consumption threshold) (lean-checker)
lap.12.0.…     1   1 error           invalid import: logic.basic
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold) (lean-checker)
lap.12.0.…     1   1 error           invalid import: data.dlist
excessive memory consumption detected at 'replace' (potential solution: increase memory consumption threshold) (lean-checker)


#### Iocta (Mar 19 2020 at 03:07):

maybe I have a broken library

#### Iocta (Mar 19 2020 at 03:11):

data.set is built-in, right? not in mathlib

#### Reid Barton (Mar 19 2020 at 03:25):

No, it is part of mathlib. Could it be that your mathlib has not been compiled? Are you opening your file in emacs?

#### Reid Barton (Mar 19 2020 at 03:25):

Your error message format is unfamiliar

#### Iocta (Mar 19 2020 at 03:52):

leanpkg help shows add <url> [branch] add a dependency from a git repository (uses latest upstream revision) but leanpkg add https://github.com/leanprover-community/mathlib.git master just gives me the help again

#### Iocta (Mar 19 2020 at 03:53):

and then if I don't specify master it says cannot find revision lean-3.7.0 in repository _target/deps/mathlib

#### Iocta (Mar 19 2020 at 04:06):

that feels like a cli-parsing bug to me. is there a maintained version of leanpkg somewhere?

#### Iocta (Mar 19 2020 at 04:07):

oh it's part of lean

#### Reid Barton (Mar 19 2020 at 04:07):

It's in lean, too, and not very large

#### Iocta (Mar 19 2020 at 04:18):

I don't understand why it just gives me the help again instead of accepting the revision https://github.com/leanprover-community/lean/blob/master/leanpkg/leanpkg/main.lean#L201

#### Iocta (Mar 19 2020 at 04:33):

Is leanproject a replacement for leanpkg?

#### Mario Carneiro (Mar 19 2020 at 04:40):

Reid Barton said:

Your error message format is unfamiliar

That's what a copy paste job from the problems window looks like

Right

#### Mario Carneiro (Mar 19 2020 at 04:44):

anyway, when you get those errors everywhere it means lean is running out of memory and you should restart lean

#### Reid Barton (Mar 19 2020 at 04:44):

And maybe run leanpkg build

#### Iocta (Mar 19 2020 at 04:48):

leanpkg build didn't help because I didn't have mathlib in the toml, which happened because leanpkg add failed to add it

#### Iocta (Mar 19 2020 at 04:50):

for now I can just leanpkg add a local path, ignoring the weirdness I mentioned above

#### Kevin Buzzard (Mar 19 2020 at 07:45):

I don't think leanpkg is designed to work with the modern set-up. If you have deviated from 3.4.2 then I think you need to be using leanproject. It's painless to install via pip and just works

#### Kevin Buzzard (Mar 19 2020 at 07:45):

And also elan. Note that mathlib master is on lean 3.7 right now

#### Dan Stanescu (Mar 25 2020 at 17:47):

I have mathlib, leanproject etc. reinstalled as per the community page and everything seems working. But I find no way to update lean itself. Running update-mathlib apparently brings in the nightlies, but lean --version keeps reporting 3.4.2. Lean was installed through VS Code + elan, and I think that same mechanism used to take care of updates. How does one update the Lean executable to the current community version? Am I missing something?

#### Patrick Massot (Mar 25 2020 at 17:47):

If you installed leanproject you don't need update-mathlib anymore.

#### Patrick Massot (Mar 25 2020 at 17:48):

Upgrading Lean will happen automatically, you don't have to worry about that.

#### Patrick Massot (Mar 25 2020 at 17:48):

Please tell us exactly what you want to do.

#### Dan Stanescu (Mar 25 2020 at 17:49):

Patrick Massot said:

Upgrading Lean will happen automatically, you don't have to worry about that.

Well, my concern is this: I see people talking about Lean version 3.7.something, but on my computer the reported version is 3.4.2.

#### Patrick Massot (Mar 25 2020 at 17:50):

Reported where? Do you want to create a new project? Work on an existing project? Update an existing project? What do you want to do. I guess running lean --version is not your end goal.

#### Dan Stanescu (Mar 25 2020 at 17:51):

Reported at the terminal command line if the command is run in an (older) project folder.

#### Patrick Massot (Mar 25 2020 at 17:52):

If this is an old project then you want to upgrade the project. Does it use mathlib?

Yes.

#### Mario Carneiro (Mar 25 2020 at 17:52):

Do you have elan installed?

Yes.

#### Mario Carneiro (Mar 25 2020 at 17:52):

does whereis lean report the elan version of lean?

#### Patrick Massot (Mar 25 2020 at 17:53):

Mario, don't talk about elan, you'll confuse people.

#### Dan Stanescu (Mar 25 2020 at 17:54):

whereis lean reports nothing. which lean reports /Users/danstanescu/.elan/bin/lean

#### Patrick Massot (Mar 25 2020 at 17:54):

Dan, you can run leanproject up inside your project.

#### Dan Stanescu (Mar 25 2020 at 17:58):

Patrick Massot said:

Dan, you can run leanproject up inside your project.

Thank you, I think this may be what I was in need of. Although at this point it tells me that This project does not depend on mathlib although I'm using it actively. But it may have something to do with my git files, which I can probably figure out.

#### Patrick Massot (Mar 25 2020 at 18:00):

Could you paste the content of leanpkg.toml and list the content of the top-level folder of your project?

#### Dan Stanescu (Mar 25 2020 at 18:23):

Here is my .toml file:

[package]
name = "LearnBasics"
version = "0.1"
lean_version = "3.4.2"
path = "src"

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


#### Dan Stanescu (Mar 25 2020 at 18:24):

And the content of the directory:

_target     leanpkg.path leanpkg.toml src


#### Patrick Massot (Mar 25 2020 at 18:26):

This is totally weird.

#### Patrick Massot (Mar 25 2020 at 18:26):

Are you in the folder containing this leanpkg.toml when you run leanproject up?

#### Patrick Massot (Mar 25 2020 at 18:27):

If I create a folder containing only you leanpkg.toml then leanproject up works.

#### Dan Stanescu (Mar 25 2020 at 18:27):

Patrick Massot said:

Are you in the folder containing this leanpkg.toml when you run leanproject up?

Yes.

#### Patrick Massot (Mar 25 2020 at 18:28):

Could you run leanproject --debug up?

#### Dan Stanescu (Mar 25 2020 at 18:29):

The result is a little longer:

configuring _user_local_packages 1
WARNING: leanpkg configurations not specifying path = "src" are deprecated.
Traceback (most recent call last):
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/lib.py", line 233, in from_path
repo = Repo(path, search_parent_directories=True)
File "/Users/danstanescu/.local/lib/python3.7/site-packages/git/repo/base.py", line 184, in __init__
raise InvalidGitRepositoryError(epath)
git.exc.InvalidGitRepositoryError: /Users/danstanescu/Programming/Lean/LearnBasics

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 92, in upgrade_mathlib
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 40, in proj
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/lib.py", line 235, in from_path
raise InvalidLeanProject('Invalid git repository')
mathlibtools.lib.InvalidLeanProject: Invalid git repository

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
File "//anaconda3/bin/leanproject", line 8, in <module>
sys.exit(safe_cli())
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 256, in safe_cli
handle_exception(err, str(err))
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 51, in handle_exception
raise exc
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 254, in safe_cli
cli()
File "//anaconda3/lib/python3.7/site-packages/click/core.py", line 764, in __call__
return self.main(*args, **kwargs)
File "//anaconda3/lib/python3.7/site-packages/click/core.py", line 717, in main
rv = self.invoke(ctx)
File "//anaconda3/lib/python3.7/site-packages/click/core.py", line 1137, in invoke
return _process_result(sub_ctx.command.invoke(sub_ctx))
File "//anaconda3/lib/python3.7/site-packages/click/core.py", line 956, in invoke
return ctx.invoke(self.callback, **ctx.params)
File "//anaconda3/lib/python3.7/site-packages/click/core.py", line 555, in invoke
return callback(*args, **kwargs)
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 97, in upgrade_mathlib
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/lib.py", line 479, in upgrade_mathlib
self.get_mathlib_olean()
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/lib.py", line 361, in get_mathlib_olean
unpack_archive(get_mathlib_archive(self.mathlib_rev, self.cache_url,
File "//anaconda3/lib/python3.7/site-packages/mathlibtools/lib.py", line 311, in mathlib_rev
raise InvalidMathlibProject('This project does not depend on mathlib')
mathlibtools.lib.InvalidMathlibProject: This project does not depend on mathlib


#### Dan Stanescu (Mar 25 2020 at 18:36):

Patrick Massot said:

This is totally weird.

So, after creating a new Lean project, I now get Lean version 3.7.2. But only if I type lean --version in the new project directory, while in the old project directory it still reports 3.4.2.

#### Patrick Massot (Mar 25 2020 at 18:39):

It looks like your LearnBasics folder is not a valid git repository, which is clearly unsupported.

#### Dan Stanescu (Mar 25 2020 at 18:40):

Right, that's what I thought.

Thank you.

#### Dan Stanescu (Mar 25 2020 at 19:27):

Wouldn't it be a good idea for the mathlib installation page to have some pointers to why using git is needed/desirable and a modicum of information on how to keep repositories in sync etc. for non-computer scientists? After all, I suppose it's to be used by mathematicians.

#### Kevin Buzzard (Mar 25 2020 at 19:30):

Conversely one might argue that just saying "click here and do this stuff and don't ask any questions" might be the perfect approach for mathematicians that have no idea what git is :-)

#### Kevin Buzzard (Mar 25 2020 at 19:31):

I never teach my students about git, those that want to learn it or know it already just learn it by googling for git.

#### Kevin Buzzard (Mar 25 2020 at 19:32):

Your point is that we should flag that git is necessary though, which I guess we could do.

#### Dan Stanescu (Mar 25 2020 at 19:32):

You don't need it until you actually do.

Right :-)

#### Dan Stanescu (Mar 25 2020 at 19:33):

Being warned about it is nice.

#### Dan Stanescu (Mar 25 2020 at 19:33):

Doesn't need to be extensive, maybe just a pointer and a link to further info.

#### Kevin Buzzard (Mar 25 2020 at 19:35):

I definitely don't think that it's our job to tell our users how to use git. But I agree that we should learn from the fact that you thought you had a lean project but it wasn't because it wasn't a git project. On the other hand, if you'd created it in the official way then I guess this wouldn't have happened?

#### Dan Stanescu (Mar 25 2020 at 19:35):

There are videos etc. on the net, but let's not forget many in math are so afraid of computers they still write transparencies. And some of the best minds at that!

#### Kevin Buzzard (Mar 25 2020 at 19:35):

Part of the problem is that all the tooling changed recently.

#### Dan Stanescu (Mar 25 2020 at 19:36):

Kevin Buzzard said:

I definitely don't think that it's our job to tell our users how to use git. But I agree that we should learn from the fact that you thought you had a lean project but it wasn't because it wasn't a git project. On the other hand, if you'd created it in the official way then I guess this wouldn't have happened?

Actually I did create it according to the instructions. It was just some time ago.

#### Kevin Buzzard (Mar 25 2020 at 19:36):

Oh OK! Well, things move on :-/

#### Johan Commelin (Mar 25 2020 at 19:36):

leanpkg new foobar always created a git repo as far as I know

#### Johan Commelin (Mar 25 2020 at 19:37):

But I agree that we should list git as a dependency

#### Patrick Massot (Mar 25 2020 at 21:15):

Dan Stanescu said:

There are videos etc. on the net, but let's not forget many in math are so afraid of computers they still write transparencies. And some of the best minds at that!

But those people won't try Lean any time soon.

#### Patrick Massot (Mar 25 2020 at 21:16):

I also don't know how we could say more clearly that git is required. This is mentioned in all our installations pages.

#### Dan Stanescu (Mar 25 2020 at 21:30):

Patrick Massot said:

I also don't know how we could say more clearly that git is required. This is mentioned in all our installations pages.

You are right, Patrick. But it can be read as "you need git to install mathlib" everywhere. What is not clear is that you have to keep working on your files in a git repository, for mathlib to work as expected. Not big deal in the long run, but doesn't cost much to add that information there either.

#### Patrick Massot (Mar 25 2020 at 21:50):

Good point. More precisely you need git if you want to update mathlib in your projects.

#### Bryan Gin-ge Chen (Mar 25 2020 at 21:56):

Here's a PR #2244.

#### Scott Morrison (Mar 25 2020 at 23:04):

@Patrick Massot is there room for leanproject giving a useful warning if called in a directory which is not a git repository?

#### Patrick Massot (Mar 25 2020 at 23:06):

Sure. It already gives such a warning in certain circumstances. I'll try to add more when I'll have time (but feel free to PR).

Last updated: May 17 2021 at 22:15 UTC