## Stream: new members

### Topic: Mathlib and LEAN_PATH

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

#### Simon Hudon (Jan 31 2019 at 20:16):

Do you use elan?

#### Jean Lo (Jan 31 2019 at 20:17):

Not yet, unfortunately.

#### Simon Hudon (Jan 31 2019 at 20:19):

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

#### 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?

#### Simon Hudon (Jan 31 2019 at 20:24):

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

#### Jean Lo (Jan 31 2019 at 20:25):

Yes, I'm on a Linux machine.

#### 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

#### 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?

#### 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

#### Jean Lo (Jan 31 2019 at 20:30):

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

:+1:

#### 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

#### Simon Hudon (Jan 31 2019 at 20:34):

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

#### Reid Barton (Jan 31 2019 at 20:37):

Not that we have found so far, see #365

#### 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

#### Reid Barton (Jan 31 2019 at 20:43):

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

#### 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?)

#### Reid Barton (Jan 31 2019 at 20:49):

I think you should unset lean-rootdir

#### 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

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


#### 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?)

#### 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

#### Reid Barton (Jan 31 2019 at 20:55):

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

#### Reid Barton (Jan 31 2019 at 20:56):

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

#### Reid Barton (Jan 31 2019 at 20:56):

(as in ~/.elan)

#### 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

#### Reid Barton (Jan 31 2019 at 20:59):

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

#### Reid Barton (Jan 31 2019 at 21:00):

you may need to restart emacs or something

#### Reid Barton (Jan 31 2019 at 21:00):

if it's a different error

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

#### Reid Barton (Jan 31 2019 at 21:04):

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

#### 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

#### Simon Hudon (Jan 31 2019 at 21:26):

I just created the branch. Can you try again?

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

Weird

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

:+1:

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

#### Simon Hudon (Jan 31 2019 at 22:43):

Did it eventually work?

#### 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?

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

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

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

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

#### 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

#### Simon Hudon (Feb 01 2019 at 00:42):

Have you tried today?

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

#### Simon Hudon (Feb 01 2019 at 00:51):

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

#### 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?

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

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

#### Scott Morrison (Feb 01 2019 at 01:00):

I can PR removing it again if no one objects.

#### Kevin Buzzard (Feb 01 2019 at 01:03):

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

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

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

#### Scott Morrison (Feb 01 2019 at 01:10):

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

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

#### 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

#### 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

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

#### Johan Commelin (Feb 02 2019 at 15:50):

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

#### Johan Commelin (Feb 04 2019 at 18:30):

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

#### Gabriel Ebner (Feb 04 2019 at 18:33):

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

#### Johan Commelin (Feb 04 2019 at 18:33):

Not too urgent I guess

#### 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

#### Johan Commelin (Feb 04 2019 at 18:39):

Ooh and enjoy the alps :skier: :snowy_mountain:

#### Johan Commelin (Feb 04 2019 at 18:40):

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

#### Johan Commelin (Feb 04 2019 at 18:40):

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

Aaah, sorry

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

#### Johan Commelin (Feb 04 2019 at 18:47):

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

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

#### 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