Mathlib and LEAN_PATH

Stream: new members

[Jean Lo]

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]

Do you use elan?

[Jean Lo]

Not yet, unfortunately.

[Simon Hudon]

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

[Simon Hudon]

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

[Jean Lo]

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]

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

[Jean Lo]

Yes, I'm on a Linux machine.

[Simon Hudon]

Here's how you do it:

which lean

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

[Jean Lo]

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

[Simon Hudon]

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

[Jean Lo]

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

[Simon Hudon]

:+1:

[Reid Barton]

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]

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

[Reid Barton]

Not that we have found so far, see #365

[Simon Hudon]

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

[Reid Barton]

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

[Jean Lo]

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]

I think you should unset lean-rootdir

[Reid Barton]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

(as in ~/.elan)

[Jean Lo]

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]

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

[Reid Barton]

you may need to restart emacs or something

[Reid Barton]

if it's a different error

[Jean Lo]

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]

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

[Reid Barton]

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]

I just created the branch. Can you try again?

[Jean Lo]

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.

[Reid Barton]

Weird

[Jean Lo]

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.

[Simon Hudon]

:+1:

[Kevin Buzzard]

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]

Did it eventually work?

[Simon Hudon]

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]

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]

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]

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]

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

[Andrew Ashworth]

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]

Have you tried today?

[Scott Morrison]

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

[Simon Hudon]

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

[Simon Hudon]

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]

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]

@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]

I can PR removing it again if no one objects.

[Kevin Buzzard]

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

[Simon Hudon]

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

[Scott Morrison]

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]

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

[Bryan Gin-ge Chen]

@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]

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

[Scott Morrison]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Gabriel Ebner]

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

[Johan Commelin]

Not too urgent I guess

[Patrick Massot]

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]

Ooh and enjoy the alps :skier: :snowy_mountain:

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

Aaah, sorry

[Johan Commelin]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

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]

I agree that this is less than urgent.