Zulip Chat Archive

Stream: new members

Topic: mathlib installation


view this post on Zulip 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)

view this post on Zulip Iocta (Mar 19 2020 at 03:07):

maybe I have a broken library

view this post on Zulip Iocta (Mar 19 2020 at 03:11):

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

view this post on Zulip 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?

view this post on Zulip Reid Barton (Mar 19 2020 at 03:25):

Your error message format is unfamiliar

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Iocta (Mar 19 2020 at 04:06):

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

view this post on Zulip Iocta (Mar 19 2020 at 04:07):

oh it's part of lean

view this post on Zulip Reid Barton (Mar 19 2020 at 04:07):

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

view this post on Zulip 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

view this post on Zulip Iocta (Mar 19 2020 at 04:33):

Is leanproject a replacement for leanpkg?

view this post on Zulip 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

view this post on Zulip Iocta (Mar 19 2020 at 04:42):

Right

view this post on Zulip 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

view this post on Zulip Reid Barton (Mar 19 2020 at 04:44):

And maybe run leanpkg build

view this post on Zulip 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

view this post on Zulip Iocta (Mar 19 2020 at 04:50):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 19 2020 at 07:45):

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Mar 25 2020 at 17:47):

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

view this post on Zulip Patrick Massot (Mar 25 2020 at 17:48):

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

view this post on Zulip Patrick Massot (Mar 25 2020 at 17:48):

Please tell us exactly what you want to do.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Mar 25 2020 at 17:51):

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

view this post on Zulip 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?

view this post on Zulip Dan Stanescu (Mar 25 2020 at 17:52):

Yes.

view this post on Zulip Mario Carneiro (Mar 25 2020 at 17:52):

Do you have elan installed?

view this post on Zulip Dan Stanescu (Mar 25 2020 at 17:52):

Yes.

view this post on Zulip Mario Carneiro (Mar 25 2020 at 17:52):

does whereis lean report the elan version of lean?

view this post on Zulip Patrick Massot (Mar 25 2020 at 17:53):

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

view this post on Zulip Dan Stanescu (Mar 25 2020 at 17:54):

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

view this post on Zulip Patrick Massot (Mar 25 2020 at 17:54):

Dan, you can run leanproject up inside your project.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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"}

view this post on Zulip Dan Stanescu (Mar 25 2020 at 18:24):

And the content of the directory:

_target     leanpkg.path leanpkg.toml src

view this post on Zulip Patrick Massot (Mar 25 2020 at 18:26):

This is totally weird.

view this post on Zulip Patrick Massot (Mar 25 2020 at 18:26):

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

view this post on Zulip Patrick Massot (Mar 25 2020 at 18:27):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 25 2020 at 18:28):

Could you run leanproject --debug up?

view this post on Zulip 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
    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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 25 2020 at 18:39):

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

view this post on Zulip Dan Stanescu (Mar 25 2020 at 18:40):

Right, that's what I thought.

view this post on Zulip Dan Stanescu (Mar 25 2020 at 18:40):

Thank you.

view this post on Zulip 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.

view this post on Zulip 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 :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Mar 25 2020 at 19:32):

You don't need it until you actually do.

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 19:32):

Right :-)

view this post on Zulip Dan Stanescu (Mar 25 2020 at 19:32):

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

view this post on Zulip Dan Stanescu (Mar 25 2020 at 19:33):

Being warned about it is nice.

view this post on Zulip Dan Stanescu (Mar 25 2020 at 19:33):

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

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 19:35):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 25 2020 at 19:36):

Oh OK! Well, things move on :-/

view this post on Zulip Johan Commelin (Mar 25 2020 at 19:36):

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

view this post on Zulip Johan Commelin (Mar 25 2020 at 19:37):

But I agree that we should list git as a dependency

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Mar 25 2020 at 21:50):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 25 2020 at 21:56):

Here's a PR #2244.

view this post on Zulip 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?

view this post on Zulip 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