idris-lang / idris2 Goto Github PK
View Code? Open in Web Editor NEWA purely functional programming language with first class types
Home Page: https://idris-lang.org/
License: Other
A purely functional programming language with first class types
Home Page: https://idris-lang.org/
License: Other
Issue by jeetu7
Friday Apr 17, 2020 at 09:56 GMT
Originally opened as edwinb/Idris2-boot#294
MarcelineVQ (at IRC) pointed at the Agda browsable source code. Agda stdlib example . This looks good for browsing source code, wherein we can go through various variables and jump across the code for declarations/definitions etc. Also, we can discuss various approaches for doing the same here.
Issue by arabelladonna
Sunday Apr 05, 2020 at 20:29 GMT
Originally opened as edwinb/Idris2-boot#267
Opening a new issue as directed to here: https://github.com/edwinb/Idris2/issues/78#issuecomment-609474846
My attempts to build Idris 2 in the MSYS2 MinGW64 terminal are failing when linking libidris_rts
. I've tried both the 0.1.0 release and the repo. I've tried make install
, make install-fromc
, and make idris2
. All end in the same error, which can be seen below.
EDIT: Forgot to mention that I've also tried building with GCC, which also failed, and that I'm using clang 9.0.1.
Using make idris2
:
$ make idris2
Using Idris 1 version: 1.3.2
Building Idris 2 version: 0.1.0-59503712f
idris --build idris2.ipkg
Entering directory `.\src'
Leaving directory `.\src'
make -C dist
make[1]: Entering directory '/d/code/github/idris2/dist'
make -C rts
make[2]: Entering directory '/d/code/github/idris2/dist/rts'
make[2]: Nothing to be done for 'build'.
make[2]: Leaving directory '/d/code/github/idris2/dist/rts'
clang idris2.c -o idris2 -I rts -L rts -lidris_rts -lgmp -lm
D:\Applications\msys64\mingw64\bin\ld: D:\Applications\msys64\tmp\idris2-06e9d9.o:idris2.c:(.text+0x811cbb): undefined reference to `__imp_listen'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$buf_htonl[buf_htonl]+0x1c): undefined reference to `__imp_htonl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$buf_ntohl[buf_ntohl]+0x1c): undefined reference to `__imp_ntohl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_socket[idrnet_socket]+0x24): undefined reference to `__imp_WSAStartup'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_socket[idrnet_socket]+0x56): undefined reference to `__imp_socket'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_getaddrinfo[idrnet_getaddrinfo]+0x69): undefined reference to `__imp_getaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_bind[idrnet_bind]+0x72): undefined reference to `__imp_getaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_bind[idrnet_bind]+0x93): undefined reference to `__imp_bind'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_connect[idrnet_connect]+0x72): undefined reference to `__imp_getaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_connect[idrnet_connect]+0x91): undefined reference to `__imp_connect'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_connect[idrnet_connect]+0xa5): undefined reference to `__imp_freeaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sockaddr_ipv4[idrnet_sockaddr_ipv4]+0x2a): undefined reference to `__imp_inet_ntop'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sockaddr_ipv4_port[idrnet_sockaddr_ipv4_port]+0xa): undefined reference to `__imp_ntohs'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_accept[idrnet_accept]+0x16): undefined reference to `__imp_accept'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_send[idrnet_send]+0x28): undefined reference to `__imp_send'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_send_buf[idrnet_send_buf]+0x3e): undefined reference to `__imp_htonl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_send_buf[idrnet_send_buf]+0x6f): undefined reference to `__imp_send'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recv[idrnet_recv]+0x48): undefined reference to `__imp_recv'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recv_buf[idrnet_recv_buf]+0x18): undefined reference to `__imp_recv'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recv_buf[idrnet_recv_buf]+0x34): undefined reference to `__imp_ntohl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto[idrnet_sendto]+0x76): undefined reference to `__imp_getaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto[idrnet_sendto]+0xb1): undefined reference to `__imp_sendto'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto[idrnet_sendto]+0xbe): undefined reference to `__imp_freeaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto_buf[idrnet_sendto_buf]+0x83): undefined reference to `__imp_getaddrinfo'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto_buf[idrnet_sendto_buf]+0xa2): undefined reference to `__imp_htonl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_sendto_buf[idrnet_sendto_buf]+0xe4): undefined reference to `__imp_sendto'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recvfrom[idrnet_recvfrom]+0xa2): undefined reference to `__imp_recvfrom'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recvfrom_buf[idrnet_recvfrom_buf]+0x92): undefined reference to `__imp_recvfrom'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_recvfrom_buf[idrnet_recvfrom_buf]+0xb2): undefined reference to `__imp_ntohl'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$idrnet_get_recvfrom_port[idrnet_get_recvfrom_port]+0x13): undefined reference to `__imp_ntohs'
D:\Applications\msys64\mingw64\bin\ld: rts/libidris_rts.a(idris_net.o):idris_net.c:(.text$clean_sockets[clean_sockets]+0x3): undefined reference to `__imp_WSACleanup'
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [Makefile:7: idris2] Error 1
make[1]: Leaving directory '/d/code/github/idris2/dist'
make: *** [Makefile:75: idris2-fromc] Error 2
Issue by andrevidela
Friday Jan 24, 2020 at 23:25 GMT
Originally opened as edwinb/Idris2-boot#187
steps to reproduce (on Mac OS 10.15.2)
make install
it works
make -C libs/prelude install IDRIS2=../../idris2
../../idris2 --install prelude.ipkg
Uncaught error: File error (prelude): File Read Error
make[1]: *** [install] Error 1
make: *** [install-libs] Error 2
I can reproduce the problem with those steps as well:
make idris2
cd libs/prelude
../../idris2 --install prelude.ipkg
The error is the same.
I checked my permissions are correct (even with chmod 777
) and tried running as sudo and the result is the same.
Any ideas?
Issue by ohad
Tuesday Apr 21, 2020 at 09:37 GMT
Originally opened as edwinb/Idris2-boot#302
I thought we discussed/reported this at some point, but I can't find the report/fix.
$ cat Irrel.idr
0
foo : (0 b : Bool) -> Bool
foo b = b
0
bar : Bool
bar = q
where
q : Bool
q = foo True
0
baz : Bool
baz = let q : Bool
q = foo True in
q
$ idris2 -c Irrel.idr
1/1: Building Irrel (Irrel.idr)
1/1: Building Irrel (Irrel.idr)
Irrel.idr:10:9--12:1:While processing right hand side of bar at Irrel.idr:7:1--12:1:
While processing right hand side of bar,q at Irrel.idr:10:5--12:1:
Main.foo is not accessible in this context
Irrel.idr:15:15--15:24:While processing right hand side of bar at Irrel.idr:14:1--19:1:
While processing right hand side of bar,q at Irrel.idr:15:11--15:24:
Main.foo is not accessible in this context
Issue by locallycompact
Wednesday Apr 15, 2020 at 10:31 GMT
Originally opened as edwinb/Idris2-boot#285
Hi, getting this when I try to build idris2, on NixOS under nix-shell -p clang -p gmp -p 'idrisPackages.with-packages(with idrisPackages; [contrib])' -p chez
chez/chez007: success
chez/chez008: success
chez/chez009: success
Exception: (while loading libcb.so) libcb.so: cannot open shared object file: No such file or directory
chez/chez010: FAILURE
Issue by petithug
Sunday Mar 29, 2020 at 17:54 GMT
Originally opened as edwinb/Idris2-boot#246
This is a corner case, but an annoying one when migrating idris1 files to literate idris2 files.
Crete two files with the same name, different content, but one with the ".idr" extension and the other with the ".lidr" extension.
Loading each file in the REPL will create different build/ content.
When loading the ".lidr" file, the ".idr file is used instead, and build/ contains the same content than for the ".idr" file.
Issue by zenntenn
Saturday Aug 10, 2019 at 17:07 GMT
Originally opened as edwinb/Idris2-boot#78
Using Idris 1.3.2, and msys64, on Windows 10.
I was able to resolve the issues in https://github.com/edwinb/Idris2/issues/41, but now I'm getting stuck on the make network
step, after completing make idris2
, make prelude
and make base
.
C:\Users\joshua.hillerup\Source\Idris\Idris2>make network
make -C libs/prelude IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
../../idris2 --build prelude.ipkg
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
make -C libs/network IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cc -c -o idris_net.o idris_net.c
cc -o idris_net.so -shared idris_net.o -lws2_32
creating 'build' directory
../../idris2 --build network.ipkg
1/3: Building Network.Socket.Data (Network/Socket/Data.idr)
2/3: Building Network.Socket.Raw (Network/Socket/Raw.idr)
3/3: Building Network.Socket (Network/Socket.idr)
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make -C libs/network test IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cp idris_net.so libidris_net.so # to make C linker happy
cc -o network-tests -L. -I. test.c -lidris_net
test.c:3:10: fatal error: netinet/in.h: No such file or directory
3 | #include <netinet/in.h>
| ^~~~~~~~~~~~~~
compilation terminated.
make[1]: *** [Makefile:52: test] Error 1
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make: *** [Makefile:31: network] Error 2
Note: I do have netinet\in.h in my path, it's the first path entry even just to be sure.
Also, I added the -lws2_32 switch myself. Without it it fails earlier, with this error:
C:\Users\joshua.hillerup\Source\Idris\Idris2>make network
make -C libs/prelude IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
../../idris2 --build prelude.ipkg
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/prelude'
make -C libs/network IDRIS2=../../idris2
make[1]: Entering directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
cc -c -o idris_net.o idris_net.c
cc -o idris_net.so -shared idris_net.o
idris_net.o:idris_net.c:(.text+0xb): undefined reference to `__imp_WSACleanup'
idris_net.o:idris_net.c:(.text+0x39): undefined reference to `__imp_WSAStartup'
idris_net.o:idris_net.c:(.text+0xa5): undefined reference to `__imp_htonl'
idris_net.o:idris_net.c:(.text+0x121): undefined reference to `__imp_ntohl'
idris_net.o:idris_net.c:(.text+0x1cf): undefined reference to `__imp_socket'
idris_net.o:idris_net.c:(.text+0x25b): undefined reference to `__imp_getaddrinfo'
idris_net.o:idris_net.c:(.text+0x27c): undefined reference to `__imp_getaddrinfo'
idris_net.o:idris_net.c:(.text+0x2ed): undefined reference to `__imp_bind'
idris_net.o:idris_net.c:(.text+0x337): undefined reference to `__imp_getsockname'
idris_net.o:idris_net.c:(.text+0x380): undefined reference to `__imp_getsockname'
idris_net.o:idris_net.c:(.text+0x3b9): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x3d4): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x44f): undefined reference to `__imp_connect'
idris_net.o:idris_net.c:(.text+0x468): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x47f): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x4f6): undefined reference to `__imp_inet_ntop'
idris_net.o:idris_net.c:(.text+0x52a): undefined reference to `__imp_ntohs'
idris_net.o:idris_net.c:(.text+0x585): undefined reference to `__imp_accept'
idris_net.o:idris_net.c:(.text+0x5ca): undefined reference to `__imp_send'
idris_net.o:idris_net.c:(.text+0x657): undefined reference to `__imp_send'
idris_net.o:idris_net.c:(.text+0x6dd): undefined reference to `__imp_recv'
idris_net.o:idris_net.c:(.text+0x74c): undefined reference to `__imp_recv'
idris_net.o:idris_net.c:(.text+0x87e): undefined reference to `__imp_sendto'
idris_net.o:idris_net.c:(.text+0x891): undefined reference to `__imp_freeaddrinfo'
idris_net.o:idris_net.c:(.text+0x933): undefined reference to `__imp_sendto'
idris_net.o:idris_net.c:(.text+0xa12): undefined reference to `__imp_recvfrom'
idris_net.o:idris_net.c:(.text+0xb0e): undefined reference to `__imp_recvfrom'
idris_net.o:idris_net.c:(.text+0xbea): undefined reference to `__imp_ntohs'
collect2.exe: error: ld returned 1 exit status
make[1]: *** [Makefile:39: idris_net.so] Error 1
make[1]: Leaving directory '/c/Users/joshua.hillerup/Source/Idris/Idris2/libs/network'
make: *** [Makefile:30: network] Error 2
Issue by vfrinken
Wednesday Apr 15, 2020 at 21:08 GMT
Originally opened as edwinb/Idris2-boot#288
I would like to have an efficient way to access elements in records and nested sub-records, lust like in Idris 1. This works for updating elements { ... = ...}
, resp. {... $= ...}
, but simply extracting the wanted element doesn't work. In short, I would like this:
record NestedRecord where
constructor MkNestedRecord
subElement : Nat
record MyRecord where
constructor MkMyRecord
nested : NestedRecord
getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = record {nested->subElement} myRec
Issue by vfrinken
Friday Apr 10, 2020 at 23:17 GMT
Originally opened as edwinb/Idris2-boot#275
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
import Decidable.Equality
data MyDATA = ABC | DEF
DecEq MyDATA where
decEq ABC ABC = Yes Refl
decEq ABC DEF = No (\Refl impossible)
decEq DEF ABC = No (\Refl impossible)
decEq DEF DEF = Yes Refl
type checking without problems
Idris: File loaded successfully
like Idris 1
Parse error: Not the end of a block entry (next tokens: [symbol (, symbol \, identifier Refl, impossible, symbol ), identifier decEq, identifier DEF, identifier ABC, symbol =, identifier No])
Issue by kvackkvack
Thursday Mar 19, 2020 at 22:11 GMT
Originally opened as edwinb/Idris2-boot#236
f : { a, b : Type } -> Either a b -> Either b a
f {a=b} x = x
f (Right x) = Left x
f (Left x) = Right x
Something like:
When unifying Either b1 b and Either b b1
Mismatch between:
b1
and
b
(duplicate b renamed to b1 to avoid name clash)
When unifying Either b b and Either b b
Mismatch between:
b
and
b
Issue by petithug
Sunday Mar 29, 2020 at 18:16 GMT
Originally opened as edwinb/Idris2-boot#249
When using AddClause on an interface implementation, the operator clauses are invalid.
Loading the following in the REPL and executing ":ac 4 Eq"
data Blah : Type where
MkBlah : Blah
Eq Blah where
data Blah : Type where
MkBlah : Blah
Eq Blah where
(/=) x y = ?something_rhs
data Blah : Type where
MkBlah : Blah
Eq Blah where
/= x y = ?/=_rhs
Issue by vladciobanu
Wednesday Aug 14, 2019 at 10:32 GMT
Originally opened as edwinb/Idris2-boot#83
The REPL seems to be able to generate the definition for specialized linear map definition for List
, but if we add a second recursive parameter (such as required for a binary tree), then generate definition loops forever.
Please see https://gist.github.com/vladciobanu/a9509be6e005312af698a03d324cc0d9 for a trivial reproduction example. The code includes the List
version to showcase the differences.
Generate the correct implementation, or at least report it can't.
Infinite loop.
Possibly related, but unsure. Let me know if I should create a different issue for this.
If I change the definition of Tree
to
data Tree a = TNil | Node a (List' (Tree a))
mapTree : ((1 x : a) -> b) -> (1 t : Tree a) -> Tree b
and try to generate its map function, I get:
mapTree f TNil = TNil
mapTree f (Node x y) = mapTree f (Node x (Cons TNil y))
If I change the definition to
data Tree a = NNode a (List' (Tree a))
Then it reports it can't find a definition for the same mapTree
, although we can write:
mapTree f (Node x xs) = Node (f x) (mapList (mapTree f) xs)
Issue by wchresta
Thursday Oct 31, 2019 at 01:49 GMT
Originally opened as edwinb/Idris2-boot#149
The module Compiler.Common
exposes the tmpName
function creating a new temporary file.
According to GNU manpage 3 for tmpnam(3), this function should never be used:
Never use this function. Use mkstemp(3) or tmpfile(3) instead.
Compiler.Common.tmpName
is not implemented using tmpnam
Compiler.Common.tmpName
is implemented using tmpnam
Issue by ohad
Saturday Oct 26, 2019 at 21:04 GMT
Originally opened as edwinb/Idris2-boot#140
I'm not sure this is really a language problem, maybe a feature request?
Potentially related to #139.
Also, the example below is not realistic (because of the go_figure
hole), it's just there to illustrate the problem in a short example.
Foo.idr
foo : Nat -> Bool
foo n = case compare n Z of
LT => False
_ => True
foo_true : (n : Nat) -> foo n = True
foo_true n with (compare n Z)
foo_true n | LT = ?go_figure -- That's fine
foo_true n | _ = ?hole -- That's not
$ idris2 Foo.idr
Foo> :t hole
n : Nat
-------------------------------------
hole : True = True
n : Nat
-------------------------------------
hole : (case _ of { LT => False ; _ => True }) = True
We can, of course, prove the foo_true
lemma (modulo go_figure
) by exhausting all the other cases:
foo_true' : (n : Nat) -> foo n = True
foo_true' n with (compare n Z)
foo_true' n | LT = ?go_figure' -- That's fine
foo_true' n | GT = Refl
foo_true' n | EQ = Refl
But it would be nicer to follow the same pattern that execution takes.
Issue by petithug
Sunday Mar 29, 2020 at 18:07 GMT
Originally opened as edwinb/Idris2-boot#247
When using AddClause on an interface implementation, the clause should be indented.
Loading the following in the REPL and executing ":ac 4 Show"
data Blah : Type where
MkBlah : Blah
Show Blah where
data Blah : Type where
MkBlah : Blah
Show Blah where
showPrec d x = ?showPrec_rhs
data Blah : Type where
MkBlah : Blah
Show Blah where
showPrec d x = ?showPrec_rhs
Issue by ohad
Monday Oct 21, 2019 at 19:43 GMT
Originally opened as edwinb/Idris2-boot#129
I'm not sure this is a bug, it's possible my types are not quite right, or that I've used access modifiers the wrong way.
Download the attached unstable-import.zip and unpack, and build it.
$ unzip unstable-import.zip
Archive: unstable-import.zip
inflating: PreorderReasoning.idr
inflating: VectReasoning.idr
inflating: Carriers.idr
inflating: Signatures.idr
inflating: Algebras.idr
inflating: Presentations.idr
inflating: Models.idr
inflating: Frex.idr
inflating: Monoids.idr
inflating: Powers.idr
inflating: CMonoids.idr
inflating: CMonoids/Axioms.idr
inflating: CMonoids/Nat.idr
inflating: CMonoids/Semiring.idr
inflating: CMonoids/Free.idr
$ idris2 -c CMonoids.idr
Build should complete successfully:
$ idris2 -c CMonoids.idr
1/15: Building PreorderReasoning (PreorderReasoning.idr)
2/15: Building VectReasoning (VectReasoning.idr)
3/15: Building Carriers (Carriers.idr)
4/15: Building Signatures (Signatures.idr)
5/15: Building Algebras (Algebras.idr)
6/15: Building Presentations (Presentations.idr)
7/15: Building Models (Models.idr)
8/15: Building Frex (Frex.idr)
9/15: Building Monoids (Monoids.idr)
10/15: Building CMonoids.Axioms (CMonoids/Axioms.idr)
11/15: Building CMonoids.Nat (CMonoids/Nat.idr)
12/15: Building Powers (Powers.idr)
13/15: Building CMonoids.Semiring (CMonoids/Semiring.idr)
14/15: Building CMonoids.Free (CMonoids/Free.idr)
15/15: Building CMonoids (CMonoids.idr)
$
...
15/15: Building CMonoids (CMonoids.idr)
CMonoids.idr:31:39--32:1:While processing type of CMonoids.CMonoid_free_up_uniqueness at CMonoids.idr:23:1--32:1:
When unifying U (Alg b) and U (Alg b)
Mismatch between:
S (S Z)
and
Z
so far so good, but if you edit CMonoids.idr
and change line 16 onward as follows, moving the import of CMonoids.Semiring
two imports down:
--import CMonoids.Semiring
import public CMonoids.Axioms
import public CMonoids.Nat
import CMonoids.Semiring
import public CMonoids.Free
then everything type-checks fine:
$ idris2 -c CMonoids.idr
15/15: Building CMonoids (CMonoids.idr)
$
This can also be expected if somehow these modules exported an ambiguity in definitions, but I think they don't.
Issue by vfrinken
Wednesday Apr 15, 2020 at 22:14 GMT
Originally opened as edwinb/Idris2-boot#289
The lastest idris build doesn't pass all tests for me.
I did
git pull && make clean && make && make install
and it failed some tests, (idris2/basic029
for example, but also other tests)
...
Building Idris 2 version: 0.1.0-048bce23a
...
...
...
idris2/basic027: success
idris2/basic028: success
idris2/basic029: FAILURE
Golden value differs from actual value.
diff --git a/tests/idris2/basic029/expected b/tests/idris2/basic029/expected
index c08a343..a81f1cf 100644
--- a/tests/idris2/basic029/expected
+++ b/tests/idris2/basic029/expected
@@ -1,6 +1,7 @@
1/1: Building Params (Params.idr)
-Main> 2
-Main> 0
-Main> 1
-Main> 1
+Error in TTC file: TTC data is in an older format, file: ["Prelude"], expected version: 21, actual version: 20
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add
+Main> (interactive):1:1--1:8:Undefined name add
Issue by ohad
Wednesday Nov 06, 2019 at 08:29 GMT
Originally opened as edwinb/Idris2-boot#150
Might be related to #113 .
$ cat Bar.idr
X : Nat
X = let a : Nat
a = 0
in a
$ idris2 -c Bar.idr
1/1: Building Bar2 (Bar.idr)
$
Bar.idr:4:9--4:9:Parse error: Couldn't parse declaration (next tokens: [in, identifier a, end of input])
If we dis-indent the in
keyword, it parses fine:
$ cat Bar2.idr
X : Nat
X = let a : Nat
a = 0
in a
$ idris2 -c Bar2.idr
1/1: Building Bar2 (Bar2.idr)
$
Issue by ohad
Saturday Oct 05, 2019 at 05:32 GMT
Originally opened as edwinb/Idris2-boot#113
Sorry if this is a feature!
Type-check the following declarations:
x1 : Nat
x1 =
let u =
S
Z
in
1
x2 : Nat
x2 =
let u =
S Z
in
1
x3 : Nat
x3 =
let u =
S Z
in
1
x4 : Nat
x4 =
let u = S Z
in
1
x5 : Nat
x5 =
let u =
S Z
in
1
These should all type-check.
The following don't type-check, with the below errors:
x1 : Nat
x1 =
let u =
S
Z
in
1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])
x2 : Nat
x2 =
let u =
S Z
in
1
Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [let, identifier u, symbol =, identifier S, identifier Z, in, literal 1, end of input])
x3 : Nat
x3 =
let u =
S Z
in
1
Foo.idr:21:7--22:7:While processing right hand side of Main.x4 at Foo.idr:20:1--42:1:
No type declaration for Main.u
The following type-check
x4 : Nat
x4 =
let u = S Z
in
1
x5 : Nat
x5 =
let u =
S Z
in
1
Issue by MarcelineVQ
Saturday Apr 25, 2020 at 00:09 GMT
Originally opened as edwinb/Idris2-boot#320
It would be useful to have a way, in patterns, to check for the presence of a constructor without regard to its arguments.
Currently given
data Tree : Type -> Type where
Tip : Tree a
Node : (v : a) -> (l : Tree a) -> (r : Tree a) -> Tree a
in a pattern match in Idris where we don't use the values in Node we would write (Node _ _ _)
to match the Node constructor.
In Haskell one can do the same, but can also write Node{}
.
(Node _ _ _)
and Node{}
are equivalent but the latter more strongly expresses a complete disinterest for any information other than that we have a Node.
This is particularly useful for places where you just want to satisfy some NonEmpty property for your value. For example given
data NonEmpty : Tree a -> Type where
IsNonEmpty : NonEmpty (Node v l r)
maxView : (t : Tree a) -> {auto ok : NonEmpty t} -> (a, Tree a)
maxView (Node v l Tip) = (v,l)
maxView (Node v l r@(Node _ _ _)) =
let (x,r') = maxView r in (x, Node v l r')
Currently if we want idris to infer a NonEmpty where we need it we might write
case t of
Tip => ?foo
n@(Node _ _ _) => maxView n
compared to
case t of
Tip => ?foo
n@Node{} => maxView n
and even maxView could make use of this since it also only needs to know that it has a Node, not what the Node contains
maxView (Node v l r@Node{}) =
It doesn't seem like a big addition but these savings add up due to making for more direct code, you are stating just one time to the reader and compiler "I don't make use of Node's values here" instead of stating it once for each field of Node.
edwin mentions on irc:
<edwinb> I thought about that [this feature] a while ago, and the reason I didn't is that, in Haskell, it's consistent with the record syntax, but in Idris there's nothing for it to be consistent with
<edwinb> it might still be a reasonable special case. It is useful.
With that in mind I'd love to hear some syntax suggestions (and opinions) for this feature, e.g. matching a Node without regard to its contents and calling it n
could look like:
n@Node{}
n@Node(..)
n@Node()
n@Node#
n&Node
Issue by ska80
Monday Mar 16, 2020 at 13:13 GMT
Originally opened as edwinb/Idris2-boot#233
Heap.idr
:
data Heap : Type -> Type where
Empty : Ord elem => Heap elem
Node : Ord elem => Int -> elem -> Heap elem -> Heap elem -> Heap elem
merge : Heap elem -> Heap elem -> Heap elem
merge heap Empty = heap
merge Empty heap = heap
merge h1@(Node _ elem1 left1 right1) h2@(Node _ elem2 left2 right2) =
if elem1 <= elem2
then makeT elem1 left1 (merge right1 h2)
else makeT elem2 left2 (merge h1 right2)
where
rank : Heap elem -> Int
rank Empty = 0
rank (Node r _ _ _) = r
makeT : elem -> Heap elem -> Heap elem -> Heap elem
makeT x left right = if rank left >= rank right
then Node (rank right + 1) x left right
else Node (rank left + 1) x right left
$ idris2 --check Heap.idr
1/1: Building Heap (Heap.idr)
1/1: Building Heap (Heap.idr)
Heap.idr:19:34--20:29:While processing right hand side of Main.merge at Heap.idr:8:1--21:1:
While processing right hand side of 1148:makeT at Heap.idr:18:5--21:1:
Multiple solutions found in search. Possible correct results:
conArg
conArg
Issue by malte-v
Saturday Apr 18, 2020 at 07:29 GMT
Originally opened as edwinb/Idris2-boot#297
Currently using the arrow keys just prints ANSI sequences, which is different from the Idris 1 REPL.
Enter the Idris 2 REPL and use the arrow keys.
It cycles through the recently used commands.
Escape sequences get printed.
Issue by nicolabotta
Thursday Aug 01, 2019 at 16:20 GMT
Originally opened as edwinb/Idris2-boot#71
The program
import Data.Fin
import Data.Vect
tail : {0 A : Type} -> {n : Nat} -> (Fin (S n) -> A) -> (Fin n -> A)
tail f = f . FS
toVectFun : {0 A : Type} -> {n : Nat} -> (Fin n -> A) -> Vect n A
toVectFun {n = Z} _ = Nil
toVectFun {n = S m} f = (f FZ) :: (toVectFun (tail f))
N : Nat
N = ...
xs : Vect (S N) Nat
xs = toVectFun {n = S N} finToNat
main : IO ()
main = putStrLn ("xs(" ++ show N ++ ") = " ++ show (index (fromInteger (natToInteger N)) xs))
type checks and executes in more than quadratic time in N
in idris 2:
N = 20, user time = 0.78s
N = 40, user time = 2.57s
N = 80, user time = 14.49s
N = 160, user time = segfault
N = 320, user time = segfault
For "large" values of N
, it segfaults. In idris 1, the correspondent program also does not run in linear time
N = 100, user time = 3.3s
N = 200, user time = 4.9s
N = 400, user time = 10.1s
N = 800, user time = 36.4s
N = 1600, user time = 197.6s
, but it does not segfault and is faster. What is the expected complexity of the program? Shouldn't building the vector and reading its last component be linear operations in N
?
Issue by ohad
Saturday Oct 26, 2019 at 20:37 GMT
Originally opened as edwinb/Idris2-boot#139
Sorry about the title, I'm not sure how to best title this bug
Foo.idr
:
foo1 : List a -> List a -> List a
foo1 [] right = []
foo1 left [] = []
foo1 (x::xs) (y::ys) = []
empty1 : (left, right : List a) -> foo1 left right = []
empty1 [] right = Refl
empty1 left [] = ?hole1
empty1 (x::xs) (y::ys) = Refl
foo2 : List a -> List a -> List a
foo2 left [] = []
foo2 [] right = []
foo2 (x::xs) (y::ys) = []
empty2 : (left, right : List a) -> foo2 left right = []
empty2 [] right = ?hole2
empty2 left [] = Refl
empty2 (x::xs) (y::ys) = Refl
The difference between foo1
and foo2
is the order of the top two clauses.
$ idris2 Foo.idr
Foo> :t hole1
0 a : Type
left : List a
-------------------------------------
hole1 : [] = []
Foo> :t hole2
0 a : Type
right : List a
-------------------------------------
hole2 : [] = []
Foo> :t hole1
0 a : Type
left : List a
-------------------------------------
hole1 : (foo1 left []) = []
Foo> :t hole2
0 a : Type
right : List a
-------------------------------------
hole2 : (foo2 [] right) = []
Idris1 exhibits the same behaviour.
Issue by fabianhjr
Wednesday Apr 22, 2020 at 01:23 GMT
Originally opened as edwinb/Idris2-boot#307
module Test
interface Simple a where
op : a -> a -> a
interface Simple a => Constraint a where
square : a -> a
square x = x `op` x
-- And
[NamedSimple1] Simple Bool where
op True True = True
op _ _ = False
-- Or
[NamedSimple2] Simple Bool where
op False False = False
op _ _ = True
[Constrainted1] Constraint Bool using NamedSimple1 where
[Constrainted2] Constraint Bool using NamedSimple2 where
Should typecheck and use their corresponding implementations
Test.idr:21:1--23:1:While processing right hand side of Constrainted2 at Test.idr:21:1--23:1:
Multiple solutions found in search. Possible correct results:
NamedSimple1
NamedSimple2
Issue by berewt
Friday Apr 24, 2020 at 09:06 GMT
Originally opened as edwinb/Idris2-boot#319
In some cases (can't be more precise about the context unfortunately) the implementation of a typeclass with several parameters doesn't work, the compiler mixes up the parameter order.
It can be resolve by making the parameters explicit in the signatures of the functions of the typeclass, but they have to be declared in a specific order.
Try to compile this file
public export
interface IxFunctor (f : (lbl : Type) -> (pre : List lbl) -> (post : List lbl) -> Type -> Type)
where
map : (a -> b) -> f ty pre post a -> f ty pre post b
public export
interface (IxFunctor f) =>
IxApplicative (f : (lbl : Type) -> (pre : List lbl) -> (post : List lbl) -> Type -> Type)
where
pure : {st : List lbl} -> a -> f lbl st st a
(<*>) : f lbl pre inter (a -> b) -> f lbl inter post a -> f lbl pre post b
data Dummy : (lbl : Type) -> (pre, post : List lbl) -> Type -> Type where
AmIDumb : a -> Dummy b pre post a
IxFunctor Dummy where
map func (AmIDumb x) = AmIDumb (func x)
IxApplicative Dummy where
pure x = ?pure_rhs
(<*>) mf mx = ?app_rhs
It should compile.
Test.idr:23:1--38:1:While processing right hand side of IxApplicative implementation at Test.idr:23:1--38:1 at Test.idr:23:1--38:1:
When unifying Dummy lbl post a inter and Dummy lbl inter post a
When unifying Dummy lbl st st a and Dummy lbl st a st
Mismatch between:
st
and
a
Issue by jeetu7
Friday Apr 17, 2020 at 10:07 GMT
Originally opened as edwinb/Idris2-boot#295
This issue pertains to the mechanism for genreating html documentation automatically from source idr files. It might be something like hackage/haddock or python-sphinx-autodoc. Here we can document the approaches and progress till we have something implemented. Afterwards, further sub-issuse can be created.
The documentation extracted can be linked with browsable docs of the source code. #294
Issue by nicolabotta
Tuesday Oct 29, 2019 at 07:48 GMT
Originally opened as edwinb/Idris2-boot#146
Is there a way of accessing these values in Idris 2? Something like Numeric.IEEE
in Haskell? At lest epsilon
, infinity
and NaN
are badly needed, e.g., to implement interval arithmetics! Thanks, Nicola
Issue by petithug
Sunday Mar 29, 2020 at 18:10 GMT
Originally opened as edwinb/Idris2-boot#248
AddClause on an interface implementati9on should add all the clauses.
See also #247.
Loading the following in the REPL and executing ":ac 4 Show"
data Blah : Type where
MkBlah : Blah
Show Blah where
data Blah : Type where
MkBlah : Blah
Show Blah where
showPrec d x = ?showPrec_rhs
show x = ?show_rhs
data Blah : Type where
MkBlah : Blah
Show Blah where
showPrec d x = ?showPrec_rhs
Issue by ohad
Saturday Oct 26, 2019 at 22:51 GMT
Originally opened as edwinb/Idris2-boot#141
Sorry this is not minimal. If I have a better idea on what's happening under the hood, I'll try to minimize.
Foo.idr
infix 10 @@
-- DIY "with (...) proof p" construct
(@@) : (f : a -> b) -> (x : a) -> (u : b ** f x = u)
(@@) f x = ( f x ** Refl)
bar : a -> b -> (a,b)
bar x y = (x,y)
gnat : Nat -> Nat -> Nat
gnat m n with (S @@ n, m)
gnat m n | ((l ** pf), k) with (plus k l)
gnat m n | ((l ** pf), k) | z = ?help
$ idris2 Foo.idr
Foo> :t help
l : Nat
n : Nat
pf : (S n) = l
k : Nat
m : Nat
z : Nat
-------------------------------------
help : Nat
1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data/List/Foo.idr:13:18--13:20:With clause does not match parent
There's nothing wrong with the top two lines in the with
block:
gnat : Nat -> Nat -> Nat
gnat m n with (S @@ n, m)
gnat m n | ((l ** pf), k) {--with (plus k l)
gnat m n | ((l ** pf), k) | z--} = ?help
1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data.List.Foo> :t help
l : Nat
n : Nat
pf : (S n) = l
k : Nat
m : Nat
-------------------------------------
help : Nat
and dropping the dependent pair is also fine:
gnat : Nat -> Nat -> Nat
gnat m n with (S n, m)
gnat m n | ((l ), k) with (plus k l)
gnat m n | ((l ), k) | z = ?help
1/1: Building Data.List.Foo (Data/List/Foo.idr)
Data.List.Foo> :t help
n : Nat
m : Nat
z : Nat
l : Nat
k : Nat
-------------------------------------
help : Nat
Issue by fabianhjr
Tuesday Apr 21, 2020 at 20:32 GMT
Originally opened as edwinb/Idris2-boot#306
module Test
interface Interface1 a where
x : Bool
interface Interface2 a where
y : Bool
interface (Interface1 a, Interface2 a) => InterfaceMix a where
z : Bool
z = x || y
Typecheck
Test.idr:11:7--11:9:While processing right hand side of Default implementation of z at Test.idr:11:3--13:1:
Can't find an implementation for Interface1 ?a
Issue by MarcelineVQ
Saturday Apr 25, 2020 at 20:46 GMT
Originally opened as edwinb/Idris2-boot#324
Idris 2, version 0.1.0-19426ecd1
I've included a lambda of case and a lambdacase to show it's not specific to one.
foo1 : ()
foo1 = (\dx => case dx of () => ()) ()
foo2 : ()
foo2 = (\case () => ()) ()
Typechecking completes.
1/1: Building Case (Case.idr)
Case.idr:2:8--4:1:While processing right hand side of foo1 at Case.idr:2:1--4:1:
Can't solve constraint between:
?delayTy [no locals in scope]
and
()
Case.idr:5:8--11:1:While processing right hand side of foo2 at Case.idr:5:1--11:1:
Can't solve constraint between:
?delayTy [no locals in scope]
and
()
Error(s) building file tests/idris2/case001/Case.idr: tests/idris2/case001/Case.idr:2:1--4:1:When elaborating right hand side of Main.foo1:
tests/idris2/case001/Case.idr:2:8--4:1:?Main.{delayTy:170}_[$resolved1135] and $resolved1132 are not equal
tests/idris2/case001/Case.idr:5:1--11:1:When elaborating right hand side of Main.foo2:
tests/idris2/case001/Case.idr:5:8--11:1:?Main.{delayTy:181}_[$resolved1135] and $resolved1132 are not equal
Issue by vfrinken
Tuesday Mar 24, 2020 at 04:39 GMT
Originally opened as edwinb/Idris2-boot#238
If I have 2 structs in C
typedef struct{
int * a;
int b;
int * c;
}ExtraStruct;
typedef struct{
ExtraStruct extra;
int x;
int y;
} TestStruct;
TestStruct * getTestStruct(){
TestStruct * ts = (TestStruct*)malloc(sizeof(TestStruct));
ts -> x = 1234567890;
ts -> y = -1;
return ts;
}
and corresponding types in idris
ExtraStruct : Type
ExtraStruct = Struct "ExtraStruct" [("a", Int), ("b", Int), ("c", Int)]
TestStruct : Type
TestStruct = Struct "TestStruct" [("extra", ExtraStruct), ("x", Int), ("y", Int)]
I'm not able to read the correct values from an instance of TestStruct
using a show function like this
Show TestStruct where
show ts =
let x : Int = getField ts "x"
y : Int = getField ts "y"
in
"x: " ++ (show x) ++ ", y: " ++ (show y)
And example is here https://github.com/vfrinken/nestedStructsIdris2.git
x: 1234567890, y: -1
x: 0, y: 1234567890
Issue by gallais
Saturday Apr 04, 2020 at 08:34 GMT
Originally opened as edwinb/Idris2-boot#264
Very easy to reproduce this internal error:
touch Test
idris2 Test
gives us:
Uncaught error: INTERNAL ERROR: build/ttc/Test.ttc: File Not Found
Issue by MarcelineVQ
Thursday Apr 23, 2020 at 18:12 GMT
Originally opened as edwinb/Idris2-boot#315
Duplicate pattern cases have a very unclear error message.
Ran into this while writing a tree but the simpler case is shown here.
typecheck:
module Main
foo1 : Maybe a -> ()
foo1 Nothing = ()
foo1 Nothing = ()
foo2 : Maybe a -> ()
foo2 d = case d of
Nothing => ()
Nothing => ()
Expect to see an error about an unreachable case or a duplicate case for both foo versions.
Even once we have coverage checking and these were labeled partial
an unreachable case warning/error seems like a good idea.
Test.idr:3:1--4:1:Attempt to match on erased argument ? in foo1
Test.idr:8:10--10:16:Attempt to match on erased argument ? in case block in foo2
Issue by edwinb
Thursday Jul 18, 2019 at 17:58 GMT
Originally opened as edwinb/Idris2-boot#30
If you have a feature request or proposal, or if you're looking for a place to get started contributing to Idris 2, please take a look at https://github.com/idris-lang/Idris2/wiki/Contributions-wanted, or at https://github.com/idris-lang/Idris2/blob/master/CONTRIBUTING.md
At the moment, since it's (mostly) only me working on the project, in about half my time, this is mainly in an effort to prevent the issue tracker for getting out of control, and making sure that I can keep on top of the most important bugs.
Please feel free to discuss proposals via the wiki or the mailing list, however!
Issue by ohad
Friday Oct 18, 2019 at 12:17 GMT
Originally opened as edwinb/Idris2-boot#127
Take a file that takes idris2 a while to type-check, say Foo.idr
.
While idris2 is type-checking, make a change in the file and save before idris2 finishes.
Reload the file.
Main> :r
1/1 Building Main (Foo.idr)
Main>
Main> :r
Main>
I think this is because the timestamp on the last change to this file is taken after type-checking finishes, and it should be taken before type-checking starts.
Issue by msmorgan
Tuesday Oct 22, 2019 at 00:44 GMT
Originally opened as edwinb/Idris2-boot#130
Since Idris 2 will be a "major version" release, I'm wondering if it would be acceptable to change the type of Data.So.choose. The current signature is surprising, since usually the Left variant of an Either is used for the error type, and Right is used for success. It's odd to see the negation of the boolean input be the Right variant.
Before: choose : (b : Bool) -> Either (So b) (So (not b))
After: choose : (b : Bool) -> Either (So (not b)) (So b)
Because this is a type-level change, existing programs using Data.So would fail to compile in Idris 2. Usually the fix will be to swap the Left and Right identifiers in a case expression.
Issue by Phiroc
Thursday Apr 02, 2020 at 18:44 GMT
Originally opened as edwinb/Idris2-boot#258
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
[ [(i,0),(0,i)] | i <- [1..10] ]
in Idris REPL
[[(1, 0), (0, 1)],
[(2, 0), (0, 2)],
[(3, 0), (0, 3)],
[(4, 0), (0, 4)],
[(5, 0), (0, 5)],
[(6, 0), (0, 6)],
[(7, 0), (0, 7)],
[(8, 0), (0, 8)],
[(9, 0), (0, 9)],
[(10, 0), (0, 10)]] : List (List (Integer, Integer))
(interactive):1:24--1:32:Can't find an implementation for Range Type
Issue by clayrat
Sunday Jul 28, 2019 at 00:28 GMT
Originally opened as edwinb/Idris2-boot#56
(This is more of a feature request, but it's been a long-standing stumbling block for me in Idris 1, and I hope it's fairly uncontroversial)
module Temp
import Data.Vect
All : (a : i -> Type) -> Type
All a {i} = {j : i} -> a j
Vect' : Type -> Nat -> Type
Vect' = flip Vect
infixr 1 :->
(:->) : (a, b : i -> Type) -> (i -> Type)
(:->) a b i = a i -> b i
showAll : All (Vect' Integer :-> Vect' String)
showAll = map show
justShowAll : Maybe (All (Vect' Integer :-> Vect' String))
justShowAll = Just ?hole
justShowAll = Just $ \{j} => map show
There doesn't seem to be a way to introduce the implicit to finish filling the hole.
Issue by abailly
Saturday Oct 05, 2019 at 09:48 GMT
Originally opened as edwinb/Idris2-boot#116
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
Create file Data/List/Extra.idr
containing:
module Data.List.Extra
public export
find : (a -> Bool) -> List a -> Maybe a
find p [] = Nothing
find p (x::xs) =
if p x then
Just x
else
find p xs
create a test.idr
file with:
module test
import Data.List.Extra as E
foo : List Nat -> Nat -> Maybe Nat
foo list bound = E.find (\ n => n < bound) list
Load test.idr
in the real and evaluate call to foo [0 .. 5 ] 2
Should output Just Z
outputs:
> foo [ 0 .. 5 ] 2
find Nat (\n => (== (compare n (S (S Z))) LT)) [Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z))), S (S (S (S (S Z))))]
When inlining the find
function in the test.idr
file, it works as expected.
Issue by Phiroc
Saturday Apr 04, 2020 at 06:07 GMT
Originally opened as edwinb/Idris2-boot#263
If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!
filter (\ARG => ARG < 3) [0, 1, 2, 3, 4]
[0, 1, 2] : List Integer
(interactive):1:1--1:41:Undefined name filter
Issue by fabianhjr
Wednesday Apr 22, 2020 at 20:45 GMT
Originally opened as edwinb/Idris2-boot#313
Load the following into a repl idris2 Test.idr
module Test
data TNat = TZ | TS TNat
data IsZero : TNat -> Type where
ItIsZero : IsZero TZ
isZero : (n: TNat) -> {ok: IsZero n} -> Bool
isZero _ = True
isZero' : (n: TNat) -> {auto ok: IsZero n} -> Bool
isZero' _ = True
Test> isZero TZ
True
Test> isZero (TS TZ)
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test> isZero' TZ
True
Test> isZero' (TS TZ)
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test>
Bye for now!
Test> isZero TZ
True
Test> isZero (TS TZ)
True <<<<<
Test> isZero' TZ
True
Test> isZero' (TS TZ)
(interactive):1:1--1:16:Can't find an implementation for IsZero (TS TZ)
Test>
Bye for now!
Aparently it is treating the evaluation of isZero
as having a hole:
test : Bool
test = isZero (TS TZ)
Test.idr:12:8--13:1:Unsolved holes:
Test.{ok:174} introduced at Test.idr:12:8--13:1
Issue by ohad
Saturday Oct 05, 2019 at 08:04 GMT
Originally opened as edwinb/Idris2-boot#114
Sorry this is a large program. I'm happy to try to cut it down to a minimal example, but I really have no clue where to start. If you have a suggestion, let me know.
Download segfaulting-frex.zip
$ unzip segfaulting-frex.zip
Archive: segfaulting-frex.zip
inflating: Carriers.idr
inflating: Signatures.idr
inflating: Algebras.idr
inflating: Presentations.idr
inflating: Models.idr
inflating: Powers.idr
inflating: Frex.idr
inflating: Monoids.idr
inflating: CMonoids.idr
$ idris2 CMonoids.idr
1/9: Building Carriers (Carriers.idr)
2/9: Building Signatures (Signatures.idr)
3/9: Building Algebras (Algebras.idr)
4/9: Building Presentations (Presentations.idr)
5/9: Building Models (Models.idr)
6/9: Building Powers (Powers.idr)
7/9: Building Frex (Frex.idr)
8/9: Building Monoids (Monoids.idr)
9/9: Building CMonoids (CMonoids.idr)
Welcome to Idris 2 version 0.0.0. Enjoy yourself!
CMonoids> :t zero_preservation
To display the context and expected type of the hole.
Segmentation fault (core dumped)
The offending hole zero_preservation
is part of this definition (CMonoids.idr:133
):
CMonoid_free_extend_zero_preservation
: (n : Nat) -> (b : Model CMonoid_Th)
-> (f : Fin n -> U b) ->
let a : Model CMonoid_Th
a = Free_CMonoid_struct n in
let h : Vect n Nat -> U b
h = CMonoid_free_extend_struct n (Alg b) f in
h ( algop _ (Alg a) CMONOID_ZERO) = algop _ (Alg b) CMONOID_ZERO
CMonoid_free_extend_zero_preservation n b f =
rewrite CMonoid_free_zero_representation n in
?zero_preservation
Issue by maxdeviant
Saturday Apr 11, 2020 at 14:57 GMT
Originally opened as edwinb/Idris2-boot#276
I was thinking of starting work on a JavaScript backend for Idris2.
I have some preliminary work (AST and codegen) completed on my fork, but I wanted to check in before getting too deep into this.
I just saw this commit which states "This is step 0 towards pluggable back ends". Would it be better to wait until pluggable backends are in place before even thinking about a JS backend?
Also, a more general question, are other backends (like a JS one) intended to be in-tree? Or would they be handled out-of-tree?
Issue by ice1000
Sunday Apr 05, 2020 at 02:32 GMT
Originally opened as edwinb/Idris2-boot#266
Master version of Idris2, getting this:
Exception: (while loading libcb.so) libcb.so: cannot open shared object file: No such file or directory
chez/chez010: FAILURE
Expected:
"9\nCallback coming\nIn callback\n24\nCallback coming\nIn callback with (1, 2)\n3\n9\n'k'\n1/1: Building CB (CB.idr)\nMain> Main> Bye for now!\n"
Given:
"1/1: Building CB (CB.idr)\nMain> Main> Bye for now!\n"
chez/chez011: success
chez/chez012: success
Exception: (while loading libstruct.so) libstruct.so: cannot open shared object file: No such file or directory
chez/chez013: FAILURE
Expected:
"(40, 30)\n\"Here\": (40, 30)\nMade it!\n1/1: Building Struct (Struct.idr)\nMain> Main> Bye for now!\n"
Given:
"1/1: Building Struct (Struct.idr)\nMain> Main> Bye for now!\n"
chez/chez014: success
200/202 tests successful
Makefile:4: recipe for target 'test' failed
make[1]: *** [test] Error 1
make[1]: Leaving directory '/home/ice1000/git-repos/idris2/tests'
Makefile:123: recipe for target 'test' failed
make: *** [test] Error 2
Where should I obtain libcb.so
and libstruct.so
? I'm using Chez scheme 9.5
Issue by jbsolomon
Thursday Feb 27, 2020 at 00:51 GMT
Originally opened as edwinb/Idris2-boot#201
Hi,
I built Idris2 from source on 28b7c62 without using Make or MSYS2 by simply writing YafflePaths.idr
by hand, uncommenting opts = "--partial-eval -O2 --cg-opt -lws2_32"
in idris2.ipkg
, and running idris --build idris2.ipkg
.
Edit: I realize now that the missing libs is already mentioned in the Idris repo:
https://github.com/idris-lang/Idris-dev/wiki/Windows-Binaries#troubleshooting
The rest of my comments deal with building Prelude and the rest of the base libs.
Issue by nicolabotta
Tuesday Jul 30, 2019 at 17:12 GMT
Originally opened as edwinb/Idris2-boot#68
I am not sure how to reproduce this in a small, self-contained example but you should be able to download https://gitlab.pik-potsdam.de/botta/Idris2Libs and then do:
idris2 FiniteAsSigmaType/Properties.idr
in the root directory of Idris2Libs. This should work fine. However, doing
idris2 FiniteAsInterface/Properties.idr
should yield
14/16: Building FiniteAsInterface.Finite (FiniteAsInterface/Finite.idr)
15/16: Building FiniteAsInterface.Operations (FiniteAsInterface/Operations.idr)
16/16: Building FiniteAsInterface.Properties (FiniteAsInterface/Properties.idr)
FiniteAsInterface/Properties.idr:24:16--24:35:While processing right hand side of FiniteAsInterface.Properties.toVectComplete at FiniteAsInterface/Properties.idr:23:1--34:1:
While processing type of 2356:s1 at FiniteAsInterface/Properties.idr:24:3--25:3:
Sorry, I can't find any elaboration which works. All errors:
If Fin.Operations.toVect: Cycle detected in solution of metavariable $resolved2372
If FiniteAsInterface.Operations.toVect: Cycle detected in solution of metavariable $resolved2372
Welcome to Idris 2 version 0.0. Enjoy yourself!
FiniteAsInterface.Properties>
This is strange because the type of s1
in FiniteAsInterface.Properties.toVectComplete
is the same as the type of s1
in FiniteAsSigmaType.Properties.toVectComplete
.
If you think it's worth, I can try to build a self-contained example of this behavior.
Issue by evertedsphere
Monday Apr 13, 2020 at 15:00 GMT
Originally opened as edwinb/Idris2-boot#278
This seems fairly simple, and I intend to add support for this myself. The easiest way, if not the "correct" one, is to add a dummy backend that pretty-prints the CompileExpr it receives to a file.
Issue by ohad
Wednesday Aug 21, 2019 at 07:21 GMT
Originally opened as edwinb/Idris2-boot#91
run idris2 totality.idr
where totality.idr is:
total
foo : a
foo = foo
- + Errors (1)
`-- totality.idr line 3 col 0:
Main.foo is possibly not total due to recursive path Main.foo --> Main.foo
$ idris2 totality.idr
1/1: Building totality (totality.idr)
Welcome to Idris 2 version 0.0. Enjoy yourself!
Main> :total foo
Main.foo is not terminating due to recursive path Main.foo
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.