Zulip Chat Archive

Stream: new members

Topic: Mathlib and LEAN_PATH


view this post on Zulip Jean Lo (Jan 31 2019 at 20:12):

I'm sure I'm missing something really obvious here, but I haven't been able to figure it out:

I recently learnt that mathlib now lives under leanprover-communityand was trying to add it as a dependency to a package by doing leanpkg add leanprover-community/mathlib. That downloads the repository but ends with a message

cannot find revision lean-3.4.2 in repository _target/deps/mathlib

Later, attempting to import from mathlib in a file throws a file (filename) not found in LEAN_PATH. LEAN_PATH is unset, as I think it should be; and changing it to /usr/local/lib/lean/library results in the same behaviour.

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:16):

Do you use elan?

view this post on Zulip Jean Lo (Jan 31 2019 at 20:17):

Not yet, unfortunately.

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:19):

That will help. Install it, that may very well solve the issue.

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:20):

See: https://github.com/Kha/elan

view this post on Zulip Jean Lo (Jan 31 2019 at 20:22):

I've only recently built Lean from source and then immediately been told that it's a bad idea. Would it be important that I remove (how?) the current installation of Lean before I start using elan to manage it?

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:24):

Yes, that would be best. Are you on a Unix system? (Linux, Mac OS X, etc)

view this post on Zulip Jean Lo (Jan 31 2019 at 20:25):

Yes, I'm on a Linux machine.

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:26):

Here's how you do it:

which lean

Then you can delete lean as well as leanpkg at that location

view this post on Zulip Jean Lo (Jan 31 2019 at 20:27):

nice. That'd be /usr/local/bin/ for me — do I have to worry about /usr/local/lib/lean?

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:28):

I would delete it out of precaution but I think you only really need to delete it if which lean finds it

view this post on Zulip Jean Lo (Jan 31 2019 at 20:30):

will do. Thanks for the help! Will report back about whether elan fixes the issue.

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:31):

:+1:

view this post on Zulip Reid Barton (Jan 31 2019 at 20:33):

I think leanpkg add will always look for the branch corresponding to the version of Lean that you're using, so we just need to make a lean-3.4.2 branch on mathlib

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:34):

Is there a way to keep that branch up-to-date automatically?

view this post on Zulip Reid Barton (Jan 31 2019 at 20:37):

Not that we have found so far, see #365

view this post on Zulip Simon Hudon (Jan 31 2019 at 20:38):

I was thinking of making lean-3.4.2 a tag and getting Travis to push the tag on every successful build

view this post on Zulip Reid Barton (Jan 31 2019 at 20:43):

If we can make it reasonably secure then it sounds like a good option

view this post on Zulip Jean Lo (Jan 31 2019 at 20:48):

have now followed instructions and installed elan. (I'm also using lean-mode — had to set lean-rootdir by hand on the last install, and the path is no longer accurate. Is setting it now to $HOME/.elan the correct thing to do?)

Also, the cannot find revisionissue persists. (I'm supposing it's because this 'leanpkg-add looks for the corresponding branch' thing?)

view this post on Zulip Reid Barton (Jan 31 2019 at 20:49):

I think you should unset lean-rootdir

view this post on Zulip Reid Barton (Jan 31 2019 at 20:50):

If elan is on your path, then you should not need any configuration, and setting variables might break the way that elan automatically selects the correct version of lean to use for each project

view this post on Zulip Jean Lo (Jan 31 2019 at 20:52):

That was the first thing I attempted, but that just made lean-mode throw an error about

Lean was not found in the ’exec-path’ and ’lean-rootdir’ is not defined. Please set it via M-x customize-variable RET lean-rootdir RET.

view this post on Zulip Reid Barton (Jan 31 2019 at 20:54):

Put the elan bin directory on your path instead (I think the elan installation should have printed instructions on how to do this?)

view this post on Zulip Reid Barton (Jan 31 2019 at 20:54):

then make sure your emacs has the new path, that is, it was started from a new shell

view this post on Zulip Reid Barton (Jan 31 2019 at 20:55):

You want this anyways so that leanpkg will work on the command line

view this post on Zulip Reid Barton (Jan 31 2019 at 20:56):

It looks like setting lean-rootdir to the elan directory would also make emacs work

view this post on Zulip Reid Barton (Jan 31 2019 at 20:56):

(as in ~/.elan)

view this post on Zulip Jean Lo (Jan 31 2019 at 20:57):

I thiiink I followed the instructions given by the elan installation, and leanpkg does work on the command line. Setting lean-rootdir to the elan directory makes the lean-rootdir error go away but it still can't seem to figure out how to import stuff from mathlib

view this post on Zulip Reid Barton (Jan 31 2019 at 20:59):

is this the cannot find revision lean-3.4.2 error, or something else?

view this post on Zulip Reid Barton (Jan 31 2019 at 21:00):

you may need to restart emacs or something

view this post on Zulip Reid Barton (Jan 31 2019 at 21:00):

if it's a different error

view this post on Zulip Jean Lo (Jan 31 2019 at 21:01):

Yeah, it's that. cannot find revision lean-3.4.2 is printed by leanpkg add leanprover-community/mathlib; and attempting anything like import data.real.basic gives me the not found in the LEAN_PATH error.

view this post on Zulip Reid Barton (Jan 31 2019 at 21:04):

Right, so that's because the branch doesn't exist

view this post on Zulip Reid Barton (Jan 31 2019 at 21:05):

Maybe you can use leanpkg add leanprover-community/mathlib master, or the low-tech solution is just to copy the line from somewhere like https://github.com/rwbarton/lean-homotopy-theory/blob/lean-3.4.2/leanpkg.toml and put whatever commit you want to use there

view this post on Zulip Simon Hudon (Jan 31 2019 at 21:26):

I just created the branch. Can you try again?

view this post on Zulip Jean Lo (Jan 31 2019 at 21:28):

hnh. leanpkg add leanprover-community/mathlib master just ... prints the usage page and does nothing, even though the usage page suggests that add <url> [branch]is the way to write it so I don't really know what's happening.

the low-tech solution seems to have gotten it working though.

view this post on Zulip Reid Barton (Jan 31 2019 at 21:31):

Weird

view this post on Zulip Jean Lo (Jan 31 2019 at 22:01):

just tried to add mathlib as a dependency again, everything seems to work fine now that the branch exists. Thanks so much for the help.

view this post on Zulip Simon Hudon (Jan 31 2019 at 22:01):

:+1:

view this post on Zulip Kevin Buzzard (Jan 31 2019 at 22:36):

One of my students ran into a serious issue today and I am wondering whether the installation procedure is now broken. She was doing a fresh Lean install on a mac. She got VS Code working fine. In @Scott Morrison 's description of what to do next it says "you could install elan by hand with curl ... but actually let's use VS Code; open up a file called test.lean and watch the magic happen". She opened test.lean and the magic did not happen (the "Oh! You have no lean! Let's install elan!" box never appeared). That was problem 1. And problem 2 was that once we had got elan installed, she got this cannot find revision lean-3.4.2 error. Like Jean, we muddled through, because I knew what the end result was supposed to look like (e.g. I had to edit her leanpkg.path at some point) but we are currently at another low point for installation ease, and I suspect that some docs might now need to be changed.

view this post on Zulip Simon Hudon (Jan 31 2019 at 22:43):

Did it eventually work?

view this post on Zulip Simon Hudon (Jan 31 2019 at 22:45):

I'm wondering if the difficulties are temporary because of the transfer of ownership of mathlib. Can you try once again and see if it's fixed?

view this post on Zulip Kevin Buzzard (Jan 31 2019 at 22:45):

Yes, it took me about 15 minutes but she now has a working Lean and mathlib. I thought I'd seen all the errors but I am fairly new to elan myself and I did not understand the cannot find revision lean-3.4.2 error, I don't think I'd seen it before. I am also now unclear which of the three of so versions of mathlib on github is the one we're supposed to be adding as a dependency for a generic user who just wants things working so they can do elementary stuff.

view this post on Zulip Kevin Buzzard (Jan 31 2019 at 22:47):

I can't try it now because our meeting finished several hours ago and I'm not going to see her again until next week; I'm also reluctant to fiddle with her installation because we got it working now. I guess if she runs into problems I'll hear from her. She's going to make a start on group cohomology but I don't know how far we'll get.

view this post on Zulip Simon Hudon (Jan 31 2019 at 22:49):

With regards to the right version, leanprover/mathlib and leanprover-community/mathlib now refer to the same library and that's the one we use. The actual location is leanprover-community/mathlib but doing things as before (i.e. using leanprover/mathlib) should still work.

view this post on Zulip Simon Hudon (Jan 31 2019 at 22:49):

A few hours ago, I added a lean-3.4.2 branch which might resolve part or all the issues.

view this post on Zulip Andrew Ashworth (Feb 01 2019 at 00:23):

but actually let's use VS Code; open up a file called test.lean and watch the magic happen". She opened test.lean and the magic did not happen (the "Oh! You have no lean! Let's install elan!" box never appeared). That was problem 1.

if this is supposed to happen, then I'll also confirm its not working on most recent version of windows and vscode as of yesterday

view this post on Zulip Simon Hudon (Feb 01 2019 at 00:42):

Have you tried today?

view this post on Zulip Scott Morrison (Feb 01 2019 at 00:46):

I just tried today, on a mac, and indeed the magic "let's install elan" box is not working. at the moment.

view this post on Zulip Simon Hudon (Feb 01 2019 at 00:51):

Ok, that's useful to know. Beside installing elan, what is it supposed to do?

view this post on Zulip Simon Hudon (Feb 01 2019 at 00:52):

What I mean to ask is, beside executing curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh does it do anything? And what happens if you write that line in a terminal?

view this post on Zulip Scott Morrison (Feb 01 2019 at 00:56):

Sorry, @Simon Hudon , what is _what_ supposed to do? I didn't follow. The vscode-lean extension is no longer offering to install elan if no usable copy of lean is found. I think I understand why, and am testing a fix.

view this post on Zulip Scott Morrison (Feb 01 2019 at 01:00):

@Bryan Gin-ge Chen, you added the line: https://github.com/leanprover/vscode-lean/blob/master/src/server.ts#L71 a while back. Could you explain why? I think it is incorrect, and it broke the "offer to install elan if lean is not available" functionality.

view this post on Zulip Scott Morrison (Feb 01 2019 at 01:00):

I can PR removing it again if no one objects.

view this post on Zulip Kevin Buzzard (Feb 01 2019 at 01:03):

The curl thing installs elan just fine, it's vs code that doesn't

view this post on Zulip Simon Hudon (Feb 01 2019 at 01:05):

Ok @Scott Morrison it looks like you're on top of it. Let me know you need something.

view this post on Zulip Scott Morrison (Feb 01 2019 at 01:10):

Okay, I tested that removing that line causes vscode to offer to install elan, and then not offer again after it succeeds. I didn't attempt to test other situations carefully (where people have lean installed elsewhere, perhaps they'll still get the offer if something goes wrong?).

view this post on Zulip Scott Morrison (Feb 01 2019 at 01:10):

@Bryan Gin-ge Chen if I missed something, please let me know.

view this post on Zulip Bryan Gin-ge Chen (Feb 01 2019 at 01:48):

@Scott Morrison Hmm, I was trying to address this: https://github.com/leanprover/vscode-lean/issues/95 I think you might be right that I did something wrong.

view this post on Zulip Bryan Gin-ge Chen (Feb 01 2019 at 02:08):

I added a comment at the PR https://github.com/leanprover/vscode-lean/pull/111

view this post on Zulip Scott Morrison (Feb 01 2019 at 19:27):

Okay, I've just PR'd a better fix. Hopefully VSCode will prompt to install elan if it can't find a copy of Lean, exactly once, and will not do so if the server crashes and needs to be restarted.

https://github.com/leanprover/vscode-lean/pull/112/files

view this post on Zulip Johan Commelin (Feb 02 2019 at 07:33):

I have a laptop without Lean. Once this is merged, I'll test it on that laptop.

view this post on Zulip Johan Commelin (Feb 02 2019 at 15:50):

@Raymond This also explains why VScode didn't do anything when you tried to install Lean.

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:30):

@Gabriel Ebner Do you think you have time to merge this somewhere soon?

view this post on Zulip Gabriel Ebner (Feb 04 2019 at 18:33):

I'm currently on a skiing vacation in Austria's beautiful alps. How urgent is it?

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:33):

Not too urgent I guess

view this post on Zulip Patrick Massot (Feb 04 2019 at 18:39):

Do I understand correctly that the extension currently works, but Scott proposes a more elegant fix? If yes then I would say we can afford to wait until Gabriel breaks his leg and goes back to TypeScript

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:39):

Ooh and enjoy the alps :skier: :snowy_mountain:

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:40):

I was under the impression that it the auto-installer part is currently broken.

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:40):

So maybe this isn't urgent for me, but it is urgent for newbies?

view this post on Zulip Patrick Massot (Feb 04 2019 at 18:41):

Even after https://github.com/leanprover/vscode-lean/pull/111 ?

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:41):

Aaah, sorry

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:41):

I hadn't seen that one. Never mind. I'll shut up. Let me try it now.

view this post on Zulip Johan Commelin (Feb 04 2019 at 18:47):

@Gabriel Ebner It is not urgent. The auto-installer works perfectly.

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2019 at 19:28):

The auto-installer is back to working at the moment, but if lean has to restart, the extension will ask you if you want to install lean via elan. The unmerged PR #112 fixes that.

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2019 at 19:28):

I agree that this is less than urgent.


Last updated: May 14 2021 at 22:15 UTC