Package Details: idris2 0.3.0-1

Git Clone URL: https://aur.archlinux.org/idris2.git (read-only, click to copy)
Package Base: idris2
Description: Funtional Programming Lanugage with Dependent Types
Upstream URL: https://www.idris-lang.org/
Licenses: custom
Submitter: mb64
Maintainer: mb64
Last Packager: mb64
Votes: 4
Popularity: 0.31
First Submitted: 2020-05-27 02:28
Last Updated: 2021-01-13 18:58

Dependencies (2)

Required by (0)

Sources (1)

Latest Comments

KozRoss commented on 2020-09-14 18:56

I am now back to the same failing test breaking the build:

chez/chez014: FAILURE Expected: "Received: hello world!\nReceived: echo: hello world!\n1/1: Building Echo (Echo.idr)\nMain> Main> Bye for now!\n" Given: "[server] Failed to bind socket with error: 99\n1/1: Building Echo (Echo.idr)\nMain> Main> Bye for now!\n"

taekyung commented on 2020-09-11 04:02

@KozRoss, I am a maintainer of chez-scheme package and sorry for abrupt name change. Currently I reverted the chez-scheme binary name to scheme, so please re-install chez-scheme and build idris2 again. Sorry.

CodingCellist commented on 2020-09-10 13:53

@KozRoss, this is due to a recent renaming in the chez-scheme package. They renamed the executable from scheme to chez-scheme because someone complained about a clash with MIT/GNU Scheme (which also calls its executable scheme)

Simply changing the PKGBUILD to export SCHEME=chez-scheme doesn't fix the problem as the build then fails with /usr/bin/env: ‘scheme’: No such file or directory. I currently don't know what the best solution would be.

KozRoss commented on 2020-09-07 18:38

I now get a build failure:

make[1]: Entering directory '/tmp/yaourt-tmp-koz/aur-idris2/src/Idris2-0.2.1/support/c' cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o getline.o getline.c cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o idris_buffer.o idris_buffer.c cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o idris_directory.o idris_directory.c cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o idris_file.o idris_file.c cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o idris_net.o idris_net.c cc -Wall -Wall -march=native -O2 -pipe -fno-plt -fPIC -fPIC -O2 -D_FORTIFY_SOURCE=2 -c -o idris_support.o idris_support.c ar rc libidris2_support.a getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o ranlib libidris2_support.a cc -shared -o libidris2_support.so getline.o idris_buffer.o idris_directory.o idris_file.o idris_net.o idris_support.o -Wl,-O1,--sort-common,--as-needed,-z,relro,-z,now make[1]: Leaving directory '/tmp/yaourt-tmp-koz/aur-idris2/src/Idris2-0.2.1/support/c' cp support/c/libidris2_support.so bootstrap/idris2_app sed s/libidris2_support.so/libidris2_support.so/g bootstrap/idris2_app/idris2.ss > bootstrap/idris2_app/idris2-boot.ss sed -i 's|PREFIX|/tmp/yaourt-tmp-koz/aur-idris2/src/Idris2-0.2.1/bootstrap|g' bootstrap/idris2_app/idris2-boot.ss sh ./bootstrap.sh bootstrapping SCHEME=scheme IDRIS2_VERSION=0.2.1 Building idris2-boot from idris2-boot.ss ./bootstrap.sh: line 20: scheme: command not found make: *** [Makefile:146: bootstrap-build] Error 127

KozRoss commented on 2020-08-25 04:40

This currently fails to build due to a failing test:

chez/chez014: FAILURE Expected: "Received: hello world!\nReceived: echo: hello world!\n1/1: Building Echo (Echo.idr)\nMain> Main> Bye for now!\n" Given: "[server] Failed to bind socket with error: 99\n1/1: Building Echo (Echo.idr)\nMain> Main> Bye for now!\n"

ulidtko commented on 2020-08-18 09:25

This patch fixes the package after upstream release 0.2.1.

diff --git i/PKGBUILD w/PKGBUILD
index f1a5ecc..d3fdc5b 100644
--- i/PKGBUILD
+++ w/PKGBUILD
@@ -3,7 +3,7 @@
 # 

 pkgname=idris2
-pkgver=0.2.0
+pkgver=0.2.1
 pkgrel=1
 pkgdesc="Funtional Programming Lanugage with Dependent Types"
 url="https://www.idris-lang.org/"
@@ -11,8 +11,8 @@ license=('custom')
 arch=('x86_64')
 depends=('chez-scheme')
 makedepends=('git')
-source=('https://www.idris-lang.org/idris2-src/idris2-latest.tgz')
-sha256sums=('03869e02cf983947c30fe66660b305114e2d21c96d3dab17efc0c7923d940db6')
+source=("https://www.idris-lang.org/idris2-src/idris2-${pkgver}.tgz")
+sha256sums=('8a32f6e93479deaf7674671ce7f06e5cc3c32afc10dccb96bd0aed34d47e9334')

 _srcname="Idris2-$pkgver"

@@ -41,7 +41,7 @@ package() {

     PREFIX="$pkgdir/usr/lib" make install-idris2
     PREFIX="$pkgdir/usr/lib" make install-support
-    for lib in prelude base network contrib ; do
+    for lib in prelude base contrib network ; do
         cd libs/$lib
         IDRIS2_PREFIX="$pkgdir/usr/lib" ../../build/exec/idris2 --install $lib.ipkg
         cd ../..

The reordering of contrib and network fixes this error in package():

(toplevel):1:1--1:1:Control.Linear.LIO not found
==> ERROR: A failure occurred in package().
    Aborting...