Zulip Chat Archive

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.

Sebastian Ullrich (Apr 20 2018 at 12:15):

And thank you for testing and writing this!

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.

Johan Commelin (Apr 20 2018 at 12:23):

Ok, elan is magic to me.

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

Johan Commelin (Apr 20 2018 at 12:23):

And I have two instances of vscode open

Johan Commelin (Apr 20 2018 at 12:24):

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

Johan Commelin (Apr 20 2018 at 12:24):

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

Johan Commelin (Apr 20 2018 at 12:24):

I assumed via some PWD in the env

Johan Commelin (Apr 20 2018 at 12:25):

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

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.

Johan Commelin (Apr 20 2018 at 12:26):

Aah, wonderful

Sebastian Ullrich (Apr 20 2018 at 12:26):

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

Johan Commelin (Apr 20 2018 at 12:26):

Fantastic

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

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

Johan Commelin (Apr 20 2018 at 13:15):

Thanks, great ideas!

Johan Commelin (Apr 20 2018 at 13:15):

Do you plan to work on this soon?

Johan Commelin (Apr 20 2018 at 13:16):

Because then I will postpone my howto for a little bit

Patrick Massot (Apr 20 2018 at 19:45):

Nice work Johan!

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

Johan Commelin (Apr 20 2018 at 19:46):

Hmm, that's true

Patrick Massot (Apr 20 2018 at 19:47):

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

Johan Commelin (Apr 20 2018 at 19:47):

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

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.

Johan Commelin (Apr 23 2018 at 05:45):

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

Johan Commelin (Apr 23 2018 at 05:46):

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

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

Johan Commelin (Apr 23 2018 at 05:47):

Or should we just link to it from several READMEs?

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.

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.

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

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.

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.

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.

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

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

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 (-;

Patrick Massot (Apr 23 2018 at 12:17):

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

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?

Patrick Massot (Apr 23 2018 at 12:36):

fork

Patrick Massot (Apr 23 2018 at 12:37):

This sounds aggressive but that's the usual procedure

Johan Commelin (Apr 23 2018 at 12:37):

okido

Patrick Massot (Apr 23 2018 at 12:37):

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

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.

Patrick Massot (Apr 23 2018 at 12:38):

Any news about 3.4.1?

Patrick Massot (Apr 23 2018 at 12:39):

I guess you wait for Mario here

Sebastian Ullrich (Apr 23 2018 at 12:39):

yes

Patrick Massot (Apr 23 2018 at 12:40):

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

Patrick Massot (Apr 23 2018 at 12:40):

Otherwise 3.4.1 is pointless

Johan Commelin (Apr 23 2018 at 14:44):

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

Patrick Massot (Apr 23 2018 at 14:46):

Thanks! I wrote a tiny comment

Johan Commelin (Apr 23 2018 at 14:51):

Fixed

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

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.

Patrick Massot (Apr 23 2018 at 15:14):

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

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

Simon Hudon (Apr 23 2018 at 15:16):

Do we get royalties? :D

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

Simon Hudon (Apr 23 2018 at 15:32):

Sounds like you win twice

Patrick Massot (Apr 23 2018 at 15:32):

I love this negociation

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.

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?

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

Sebastian Ullrich (Dec 12 2018 at 08:33):

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

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
        }

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: Dec 20 2023 at 11:08 UTC