mathlib installation

Stream: new members

[Iocta]

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]

maybe I have a broken library

[Iocta]

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

[Reid Barton]

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]

Your error message format is unfamiliar

[Iocta]

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]

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

[Iocta]

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

[Iocta]

oh it's part of lean

[Reid Barton]

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

[Iocta]

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]

Is leanproject a replacement for leanpkg?

[Mario Carneiro]

Reid Barton said:

Your error message format is unfamiliar

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

[Iocta]

Right

[Mario Carneiro]

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

[Reid Barton]

And maybe run leanpkg build

[Iocta]

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

[Iocta]

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

[Kevin Buzzard]

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]

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

[Dan Stanescu]

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]

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

[Patrick Massot]

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

[Patrick Massot]

Please tell us exactly what you want to do.

[Dan Stanescu]

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]

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]

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

[Patrick Massot]

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

[Dan Stanescu]

Yes.

[Mario Carneiro]

Do you have elan installed?

[Dan Stanescu]

Yes.

[Mario Carneiro]

does whereis lean report the elan version of lean?

[Patrick Massot]

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

[Dan Stanescu]

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

[Patrick Massot]

Dan, you can run leanproject up inside your project.

[Dan Stanescu]

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]

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

[Dan Stanescu]

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]

And the content of the directory:

_target     leanpkg.path leanpkg.toml src

[Patrick Massot]

This is totally weird.

[Patrick Massot]

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

[Patrick Massot]

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

[Dan Stanescu]

Patrick Massot said:

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

Yes.

[Patrick Massot]

Could you run leanproject --debug up?

[Dan Stanescu]

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
    proj().upgrade_mathlib()
  File "//anaconda3/lib/python3.7/site-packages/mathlibtools/leanproject.py", line 40, in proj
    lean_upgrade)
  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
    project.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]

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]

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

[Dan Stanescu]

Right, that's what I thought.

[Dan Stanescu]

Thank you.

[Dan Stanescu]

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]

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]

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]

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

[Dan Stanescu]

You don't need it until you actually do.

[Kevin Buzzard]

Right :-)

[Dan Stanescu]

And then you scratch your head and ask yourself what all this is about.

[Dan Stanescu]

Being warned about it is nice.

[Dan Stanescu]

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

[Kevin Buzzard]

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]

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]

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

[Dan Stanescu]

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]

Oh OK! Well, things move on :-/

[Johan Commelin]

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

[Johan Commelin]

But I agree that we should list git as a dependency

[Patrick Massot]

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]

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]

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]

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

[Bryan Gin-ge Chen]

Here's a PR #2244.

[Scott Morrison]

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

[Patrick Massot]

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