elan

Stream: general

[Scott Morrison]

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

[Scott Morrison]

I found

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

[Scott Morrison]

Is there anything simpler?

[Gabriel Ebner]

You could do leanpkg +nightly new my_playground.

[Scott Morrison]

Fantastic, thanks!

[Scott Morrison]

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]

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

[Scott Morrison]

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]

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]

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

[Sebastian Ullrich]

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

[Eric Rodriguez]

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

[Alex J. Best]

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

[Martin Dvořák]

I had similar issues.

[Gabriel Ebner]

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]

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

[Winston Yin]

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]

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