Zulip Chat Archive

Stream: general

Topic: elan

Scott Morrison (Oct 10 2018 at 09:36):

What is the best way to create a new project folder, using a nightly version?

Scott Morrison (Oct 10 2018 at 09:36):

I found

elan run --install nightly-2018-08-23 leanpkg new my_playground

Scott Morrison (Oct 10 2018 at 09:36):

Is there anything simpler?

Gabriel Ebner (Oct 10 2018 at 09:40):

You could do leanpkg +nightly new my_playground.

Scott Morrison (Oct 10 2018 at 09:41):

Fantastic, thanks!

Scott Morrison (Oct 07 2021 at 04:15):

Is there an elan command which simply reports the toolchain being used in the current directory? It seems simple functionality, but I can't find it. I could parse the output of elan which lean, but this seems messy.

Bryan Gin-ge Chen (Oct 07 2021 at 04:29):

elan show also displays info about the active toolchain, but it may also require parsing.

Scott Morrison (Oct 07 2021 at 06:58):

Yes, that was the sort of parsing I wanted to avoid: I'd have to look for the first line in the "Active toolchain" section, then take up to the first space.

Gabriel Ebner (Oct 07 2021 at 07:33):

I second your request for a better informational API that returns machine-readable data. I believe elan which lean has another issue, namely that it will also download the toolchain, which can cause unpredictable delays.

Gabriel Ebner (Oct 07 2021 at 07:34):

Have you tried using a regex on leanpkg.toml instead?

Sebastian Ullrich (Oct 07 2021 at 08:04):

PRs adding --json to any commands are welcome :)

Eric Rodriguez (Nov 15 2022 at 17:43):

Is anyone else having macos issues on the latest version of Lean? I get this error whenever I try and use it:

Alex J. Best (Nov 15 2022 at 17:48):

I just tested and it works fine for me, did you try reinstalling elan? (or what elan version do you have)

Martin Dvořák (Nov 15 2022 at 17:51):

I had similar issues.

Gabriel Ebner (Nov 15 2022 at 17:58):

If you search zulip for your error message, then you'll find lots of similar threads. Github changed the (inofficial, unsupported) API used by elan to query the files in a release. The latest elan version contains a fix, you just need to upgrade.

Eric Rodriguez (Nov 15 2022 at 18:49):

ahh, many thanks, I didn't know this happened again. it stopped working for me only for 3.49!

Winston Yin (Nov 16 2022 at 01:38):

I had this issue on my intel mac and just fixed it. elan should be installed and updated through homebrew, but it turns out there is an old version (1.0.7) hiding in ~/.elan. The solution is to remove ~/.elan/bin from PATH in ~/.bash_profile, and then delete ~/.elan altogether

Winston Yin (Nov 16 2022 at 01:38):

which elan may help you find old versions that shouldn't be there

Last updated: Aug 03 2023 at 10:10 UTC