Package Details: elan-lean 3.1.1-1

Git Clone URL: (read-only, click to copy)
Package Base: elan-lean
Description: A Lean version manager
Upstream URL:
Licenses: MIT, Apache
Conflicts: lean-bin, lean-community, lean-git, lean4
Provides: lean-community, lean4
Submitter: xuanruiqi
Maintainer: xuanruiqi
Last Packager: xuanruiqi
Votes: 6
Popularity: 0.23
First Submitted: 2021-01-30 07:36 (UTC)
Last Updated: 2024-06-09 20:25 (UTC)

Dependencies (3)

Required by (2)

Sources (1)

Latest Comments

Mapleleaf commented on 2023-07-03 07:08 (UTC) (edited on 2023-07-03 07:09 (UTC) by Mapleleaf)

I had some trouble using Lean after installing this package, and the Lean community suggested to add "lake" to the list of binaries to be linked, in the PKGBUILD:

_binlinks=('lean' 'leanchecker' 'leanpkg' 'lake')

champignoom commented on 2023-01-08 10:49 (UTC)

It would be nice to have the package officially supported on ARM. There seems already to be no problem building it on android/termux/arch.

xuanruiqi commented on 2022-12-01 11:35 (UTC)

That is any strange, and I can't reproduce this bug by any means. Did you try elan toolchain install stable?

facet commented on 2022-11-28 05:16 (UTC)

I cannot set a default toolchain because I cannot install one, every elan install return "binary package was not provided for 'linux'". I don't read upstram docs very carefully, but the same command works for the official version.

xuanruiqi commented on 2022-11-27 14:52 (UTC)

Is there an error message? Did you set the default toolchain? Also, did you consult the upstream docs?

facet commented on 2022-11-26 06:16 (UTC)

Of course, I would like to place packages where they should be, I just have no idea how to use it to install a toolchain. As

elan install leanprover-community/lean:3.49.1

does not work for me, am I missing something?

xuanruiqi commented on 2022-11-13 23:25 (UTC)

Well, that's the expected behavior. You need to install a toolchain and set it to default, and unfortunately there are no binaries for Linux it seems.

If the official script works for you, then you should use it; I just prefer not installing things everywhere in my home directory.

facet commented on 2022-11-08 05:04 (UTC) (edited on 2022-11-08 05:06 (UTC) by facet)

It seems not install a lean as default version, and I get "binary package was not provided for 'linux'" when trying to "elan default stable".

The offical "elan-init" shell script works well.

malet commented on 2022-09-09 19:18 (UTC)

Please update elan to the newest stable release on Github. Changing line 9 in the PKGBUILD to


and line 12 to


suffices to get a working PKGBUILD file for the new version.