Package Details: idris2 0.6.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: custom
Submitter: mb64
Maintainer: mb64 (CodingCellist)
Last Packager: CodingCellist
Votes: 6
Popularity: 0.35
First Submitted: 2020-05-27 02:28 (UTC)
Last Updated: 2022-11-11 10:03 (UTC)

Latest Comments

1 2 Next › Last »

zarakshR commented on 2024-03-02 02:47 (UTC) (edited on 2024-03-03 01:09 (UTC) by zarakshR)

I have these tests failing (expected output not matching output) during build. Could this be a problem with my machine, and if not, how would I go about fixing this? -

idris2/interactive034

idris2/literate003

uname -a: Linux thinkpad 6.7.6-arch1-2 #1 SMP PREEMPT_DYNAMIC Thu, 29 Feb 2024 19:08:51 +0000 x86_64 GNU/Linux

/usr/lib/libc.so.6: GNU C Library (GNU libc) stable release version 2.39. Copyright (C) 2024 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. Compiled by GNU CC version 13.2.1 20230801. libc ABIs: UNIQUE IFUNC ABSOLUTE Minimum supported kernel: 4.4.0 For bug reporting instructions, please see: https://gitlab.archlinux.org/archlinux/packaging/packages/glibc/-/issues.


EDIT: I managed to "fix" it by adding: except="base/system_info001 idris2/interactive034 idris2/literate003" to check() in the PKGBUILD

CodingCellist commented on 2022-11-11 10:05 (UTC)

I've created a new release of this package, excluding base/system_info001 from the check() in order to allow people experiencing the issue to hopefully build and install. The underlying problem has been fixed upstream, but won't land here until the next official release : )

CodingCellist commented on 2022-11-01 15:25 (UTC)

@gyscos interesting! Could you please open an issue at https://github.com/idris-lang/Idris2/issues detailing your processor, OS, and the output of the nproc and/or sysctl -n hw.ncpu command(s)? : )

gyscos commented on 2022-11-01 15:12 (UTC)

I am getting consistent test failures for base/system_info001. It says it found 32 processors but expected 24 (indeed I have a ryzen 5900x with 24 threads). All other tests pass fine.

grahamgower commented on 2022-01-31 20:14 (UTC)

The pkgdesc also says "Funtional" which I'm guessing should be spelled with a 'c'. :)

ulidtko commented on 2021-12-28 11:46 (UTC)

Hi @CodingCellist, just noticed a typo in the package Description field: Lanugage → Language

diff --git i/PKGBUILD w/PKGBUILD
index 00dcf07..c7340d9 100644
--- i/PKGBUILD
+++ w/PKGBUILD
@@ -5,7 +5,7 @@
 pkgname=idris2
 pkgver=0.5.1
 pkgrel=2
-pkgdesc="Funtional Programming Lanugage with Dependent Types"
+pkgdesc="Funtional Programming Language with Dependent Types"
 url="https://www.idris-lang.org/"
 license=('custom')
 arch=('x86_64')

Hope that helps :) Merry xmas and happy new year

CodingCellist commented on 2021-11-29 09:37 (UTC)

As of 2021-11-24, the aur chez-scheme package installs Chez Scheme as "chez" rather than "scheme":
https://aur.archlinux.org/packages/chez-scheme/#comment-837425

The latest release of this package (0.5.1-2) now reflects this, meaning installing with an up-to-date chez-scheme aur package should work. If there is a problem, lmk : )

mb64 commented on 2021-09-21 05:24 (UTC)

The latest version includes the idris2api package in the install, as well as installing packages with their source code, with the goal of supporting the new LSP server out of the box. However, this makes the install a lot bigger: it's roughly grown from 28MB to 128MB. If this is a problem for you, LMK.

slbtty commented on 2021-09-13 16:43 (UTC) (edited on 2021-09-13 16:50 (UTC) by slbtty)

According to this line, which was modified a few mouthes ago

https://github.com/idris-lang/Idris2/blob/70ac0f41015bc4f2738df0003651665ba1f5cc0c/src/Compiler/Scheme/Chez.idr#L42

Acceptable scheme names are "chez", "chezscheme", "chezscheme9.5", "scheme".

chez-scheme is not one of them, thus result the build fails.

I think the chez package can safely change name to chezshcme or simply chez now.

KozRoss commented on 2020-09-14 18:56 (UTC)

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"