Package Details: idris2 0.7.0-2

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.021107
First Submitted: 2020-05-27 02:28 (UTC)
Last Updated: 2025-05-27 15:24 (UTC)

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. Using pack 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="" in check().

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 🥲

make[3]: Entering directory '/home/phlimy/.cache/yay/idris2/src/Idris2-0.7.0/libs/prelude'
/home/phlimy/.cache/yay/idris2/src/Idris2-0.7.0/build/exec/idris2 --build prelude.ipkg
/home/phlimy/.cache/yay/idris2/src/Idris2-0.7.0/build/exec/idris2: line 15: /home/phlimy/.cache/yay/idris2/src/Idris2-0.7.0/build/exec/idris2_app/idris2.so: Permission denied

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 in package() be ln -s "/usr/lib/bin/idris2" "$pkgdir/usr/bin/idris2"?

1 2 3 Next › Last »