Zulip Chat Archive

Stream: general

Topic: howto lean with elan


view this post on Zulip Johan Commelin (Apr 20 2018 at 12:03):

https://gist.github.com/jcommelin/1d45a0ea7a84a87db8a28a12e93cac32
This is still WIP. I did not test it yet.

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:04):

Posting it here, because I gotta go now.

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:06):

Then add source .elan/env to your shell initialization script, say ~/.bashrc

Does this part not work out of the box via the elan installer?

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:07):

elan run nightly-2018-04-06 leanpkg new my_playground

You can do elan run --install ... to skip step 1

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:09):

Scenario 2: build implies configure

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:12):

Thanks for the feedback!

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:13):

Then add source .elan/env to your shell initialization script, say ~/.bashrc

Does this part not work out of the box via the elan installer?

Not for me. It edited .profile and .bash_profile but those files do nothing for me.

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:15):

Launch VScode from the terminal, while you are inside the directory lean-stacks-project. (This will make sure that VScode knows about the right version of Lean.)

The location from where you start VS Code should not be relevant, as long as elan is in your PATH. Actually, I would recommend configuring the path in the VS Code settings rather than bothering with the terminal. You should open an issue in the plugin repo about ~ not being accepted.

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:15):

And thank you for testing and writing this!

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:22):

It edited .profile and .bash_profile but those files do nothing for me.

It should after you log out and back in (i.e. in a new login shell). Actually, your desktop environment should usually read .profile as well next time, so you shouldn't have to configure VS Code at all. This should probably be tested by multiple people on different configurations.

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:23):

Ok, elan is magic to me.

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:23):

If I have two folders a/ and b/, and I have to different toml files in them

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:23):

And I have two instances of vscode open

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:24):

In one I navigate to a/, in the other to b/

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:24):

How will they call the right version of Lean?, How does elan figure this out?

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:24):

I assumed via some PWD in the env

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:25):

But if you don't call vscode from the terminal, that won't work

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:26):

It sure does. The vscode plugin takes care to set the cwd of the server process to the opened directory.

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:26):

Aah, wonderful

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:26):

Which automatically makes elan work, without either of the two knowing about the other tool :)

view this post on Zulip Johan Commelin (Apr 20 2018 at 12:26):

Fantastic

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 12:40):

elan 0.5.0 will make leanpkg +nightly-2018-04-06work even if it's not installed yet btw

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 13:02):

I've opened an issue about what I imagine would be a nicer elan+mathlib workflow: https://github.com/Kha/elan/issues/7

view this post on Zulip Johan Commelin (Apr 20 2018 at 13:15):

Thanks, great ideas!

view this post on Zulip Johan Commelin (Apr 20 2018 at 13:15):

Do you plan to work on this soon?

view this post on Zulip Johan Commelin (Apr 20 2018 at 13:16):

Because then I will postpone my howto for a little bit

view this post on Zulip Patrick Massot (Apr 20 2018 at 19:45):

Nice work Johan!

view this post on Zulip Patrick Massot (Apr 20 2018 at 19:46):

I think you could do the small corrections suggested by Sebastian without waiting so that we can point new users to this while Sebastian works on elan

view this post on Zulip Johan Commelin (Apr 20 2018 at 19:46):

Hmm, that's true

view this post on Zulip Patrick Massot (Apr 20 2018 at 19:47):

@Sebastian Ullrich what about VScode open folder operation? Is it no longer relevant?

view this post on Zulip Johan Commelin (Apr 20 2018 at 19:47):

I'll see if I can find some time on Monday

view this post on Zulip Sebastian Ullrich (Apr 20 2018 at 21:54):

@Patrick Massot You still need it, I think? You should use it anyway for easier navigation etc. Note that vscode-lean doesn't seem to support the new multi-root workspaces yet.

view this post on Zulip Johan Commelin (Apr 23 2018 at 05:45):

Voila, an update:
https://gist.github.com/jcommelin/1d45a0ea7a84a87db8a28a12e93cac32
This incorporates the suggestions by @Sebastian Ullrich

view this post on Zulip Johan Commelin (Apr 23 2018 at 05:46):

What would be the proper place to post this how to?

view this post on Zulip Johan Commelin (Apr 23 2018 at 05:46):

I'm fine with leaving it as a gist right now, but that isn't very visible to newcomers

view this post on Zulip Johan Commelin (Apr 23 2018 at 05:47):

Or should we just link to it from several READMEs?

view this post on Zulip Patrick Massot (Apr 23 2018 at 07:59):

I think you can PR it to mathlib/docs/elan.md and link to it from mathlib main README.

view this post on Zulip Patrick Massot (Apr 23 2018 at 08:00):

I would add that you can put the source .elan/env in your .bashrc or .zshrc instead of .profile if you want to enjoy it from terminal immediately. Reading "It is recommended that you re-login, so that your environment knows about Elan." would be extremely off-putting for me.

view this post on Zulip Johan Commelin (Apr 23 2018 at 08:15):

But it already says:

(Alternatively, type source $HOME/.elan/env into your terminal. Now this terminal session knows about Elan.)

view this post on Zulip Patrick Massot (Apr 23 2018 at 08:19):

It still doesn't suggest the shell startup scripts. And I think this emphasis is currently much more on the relogging option.

view this post on Zulip Johan Commelin (Apr 23 2018 at 08:26):

I agree that the emphasis is on logging in again. You don't need the startup scripts after logging in. So if you don't want to relogin, I would just source it straight into the current terminal session.

view this post on Zulip Johan Commelin (Apr 23 2018 at 08:27):

The reason I put emphasis on the relogin is that you can just launch VScode from a GUI launcher afterwards. Which is nice.

view this post on Zulip Johan Commelin (Apr 23 2018 at 08:27):

Otherwise you have to launch it from a terminal... which some newcomers might not really be happy with...

view this post on Zulip Johan Commelin (Apr 23 2018 at 08:28):

But I agree that asking for a relogin is maybe also something that people are not happy with...

view this post on Zulip Johan Commelin (Apr 23 2018 at 12:16):

Ok, I just reinstalled the desktop pc in my office. I just tested the howto, and it seems to work (-;

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:17):

Nice! So you can PR it and then prove that Spec vs global section thing.

view this post on Zulip Johan Commelin (Apr 23 2018 at 12:36):

Ok, so to make a pull request, should I fork leanprover/mathlib? Or is there another way to do this?

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:36):

fork

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:37):

This sounds aggressive but that's the usual procedure

view this post on Zulip Johan Commelin (Apr 23 2018 at 12:37):

okido

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:37):

Then create a branch from master in your fork and PR from there

view this post on Zulip Sebastian Ullrich (Apr 23 2018 at 12:38):

Do you plan to work on this soon?

I don't think I will get to it before Lean 3.4.1 is released... so perhaps at that point you can just hard-code 3.4.1 as the Lean version to use, with or without elan.

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:38):

Any news about 3.4.1?

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:39):

I guess you wait for Mario here

view this post on Zulip Sebastian Ullrich (Apr 23 2018 at 12:39):

yes

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:40):

We need mathlib to work with nightly-2018-04-20

view this post on Zulip Patrick Massot (Apr 23 2018 at 12:40):

Otherwise 3.4.1 is pointless

view this post on Zulip Johan Commelin (Apr 23 2018 at 14:44):

A student popped in. But here is the PR: https://github.com/leanprover/mathlib/pull/113

view this post on Zulip Patrick Massot (Apr 23 2018 at 14:46):

Thanks! I wrote a tiny comment

view this post on Zulip Johan Commelin (Apr 23 2018 at 14:51):

Fixed

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:13):

I felt like I should double that effort. So I just opened another doc PR: https://github.com/leanprover/mathlib/pull/114

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:14):

Maybe this is a nice challenge for me: each time someone PRs some doc, I double it.

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:14):

Simon: if you PR something now, we hit the 20 mark

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:15):

@Gabriel Ebner @Kenny Lau @Simon Hudon I hope you don't mind I've stolen your explanations (with attribution) in the above PR

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:16):

Do we get royalties? :D

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:18):

Your royalty is writing this piece of doc didn't distracted you from writing your tactic writing tutorials

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:32):

Sounds like you win twice

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:32):

I love this negociation

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:33):

But actually I'm a bit serious. Gathering some Zulip explanations into mathlib doc is something I can do. And I'm very happy if this allows experts to work on expert stuff I couldn't do.

view this post on Zulip Simon Hudon (Dec 12 2018 at 00:50):

I'm trying to use a local version of lean and hoping elan will help me with that. I wrote elan toolchain link lean-tweaked ~/lean/lean-master but then elan crashes. Am I the only one with this issue?

view this post on Zulip Gabriel Ebner (Dec 12 2018 at 08:28):

I've run into this as well, something in elan panics and the error message is less than helpful. An easy workaround is to add the symlink manually:

ln -s ~/lean/lean-master ~/.elan/toolchains/lean-tweaked

view this post on Zulip Sebastian Ullrich (Dec 12 2018 at 08:33):

I haven't encountered that before, but I'm open to PRs

view this post on Zulip Simon Hudon (Dec 12 2018 at 12:25):

Basically, I'd change these lines https://github.com/Kha/elan/blob/master/src/elan/toolchain.rs#L150-L154 to

        match install_method {
            InstallMethod::Copy(_) |
            InstallMethod::Dist(..) => !self.is_custom(),
            InstallMethod::Link(_) => true
        }

view this post on Zulip Simon Hudon (Dec 12 2018 at 12:28):

I should probably keep testing it. My setup seems a bit broken and I'm not sure if it's because of what I did to Lean (which I think shouldn't break anything) or what I did to elan (which I don't think should break anything either)


Last updated: May 17 2021 at 22:15 UTC