Search Criteria
Package Details: elan-lean 3.1.0-1
Package Actions
| Git Clone URL: | https://aur.archlinux.org/elan-lean.git (read-only, click to copy) |
|---|---|
| Package Base: | elan-lean |
| Description: | A Lean version manager |
| Upstream URL: | https://github.com/leanprover/elan |
| Licenses: | MIT, Apache |
| Conflicts: | lean-bin, lean-community, lean-git, lean4 |
| Provides: | lean-community |
| Submitter: | xuanruiqi |
| Maintainer: | xuanruiqi |
| Last Packager: | xuanruiqi |
| Votes: | 5 |
| Popularity: | 0.084244 |
| First Submitted: | 2021-01-30 07:36 (UTC) |
| Last Updated: | 2024-02-29 13:58 (UTC) |
Dependencies (3)
- curl (curl-quiche-gitAUR, curl-gitAUR, curl-http3-ngtcp2AUR, curl-c-aresAUR)
- xz (xz-gitAUR)
- cargo (rust-nightly-binAUR, cargo-gitAUR, rustup-gitAUR, rust, rustup) (make)
Required by (2)
- lean-game-maker-git (requires lean-community)
- python-mathlibtools (requires lean-community) (optional)
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:
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 installreturn "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
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.