Search Criteria
Package Details: idris2 0.7.0-2
Package Actions
Git Clone URL: | https://aur.archlinux.org/idris2.git (read-only, click to copy) |
---|---|
Package Base: | idris2 |
Description: | Functional Programming Language with Dependent Types |
Upstream URL: | https://idris-lang.github.io/ |
Licenses: | BSD-3-Clause |
Submitter: | mb64 |
Maintainer: | mb64 (CodingCellist) |
Last Packager: | CodingCellist |
Votes: | 8 |
Popularity: | 0.028074 |
First Submitted: | 2020-05-27 02:28 (UTC) |
Last Updated: | 2025-05-27 15:24 (UTC) |
Dependencies (3)
- chez-schemeAUR (chez-scheme-gitAUR)
- nodejs (nodejs-gitAUR, python-nodejs-wheelAUR, nodejs-lts-hydrogenAUR, nodejs-lts-iron, nodejs-lts-jod) (optional) – for the node backend
- racket (racket-gitAUR, racket-minimal) (optional) – for the racket backend
Latest Comments
1 2 3 Next › Last »
CodingCellist commented on 2025-05-27 15:31 (UTC)
Thank you so much ElkCloner, boletales, and MithicSpirit, and apologies for taking so long to fix this package. Hopefully the new release of the AUR package (not a new Idris2 release unfortunately) works.
Side-note: Most people install via
pack
these days, which thanks to MithicSpirit is also on the AUR. Usingpack
facilitates using the latest Idris2, as well as installing community packages for Idris, so it might be the better way to install for now (although I will try my best to keep this updated+building for people who use it).MithicSpirit commented on 2025-05-09 23:03 (UTC)
@ElkCloner I believe that fix has not been released, so it is not included in this package (yet: hopefully there'll be another release soon).
ElkCloner commented on 2025-05-08 12:36 (UTC)
I think this is not necessary anymore, since the issue with the locale was resolved: https://github.com/idris-lang/Idris2/commit/22c25e945e4c6e36772776290383c351a94c5a92
MithicSpirit commented on 2025-05-07 20:45 (UTC)
It would probably suffice to modify it to
LC_ALL=C make test INTERACTIVE=""
incheck()
.boletales commented on 2025-05-07 06:32 (UTC)
Due to this issue (#3339), you have to set
LC_ALL=C
when you run makepkg.esnos commented on 2024-09-17 08:44 (UTC)
With this package I had same problem as ElkCloner but his solution worked.
Phlimy commented on 2024-09-07 11:09 (UTC) (edited on 2024-09-07 11:10 (UTC) by Phlimy)
Build fails right at the end 🥲
sp1ff commented on 2024-08-01 16:19 (UTC)
Yeah, install is borked for me, too (bad symlink).
ElkCloner commented on 2024-07-17 22:17 (UTC)
After installing the package the
idris2
command doesn't work for me, because/usr/bin/idris2
ends up being a symlink to/home/elk/.cache/yay/idris2/pkg/idris2/usr/lib/bin/idris2
. Shouldn't the last line inpackage()
beln -s "/usr/lib/bin/idris2" "$pkgdir/usr/bin/idris2"
?1 2 3 Next › Last »