mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-09 21:01:12 +03:00
Flush standard out after writing prompt to it
On Unix-like operating systems stdio.h is usually line-buffered. As putStr uses fputs(3) from stdio.h internally, output will be written to standard out after a newline character is written to the buffer. Since the prompt does not contain a newline, it will only be written to standard output after the user presses return. I encountered this issue on Alpine Linux which uses musl libc (instead of glibc). However, I believe this issue is likely also reproducible with glibc. This commit fixes this issue by flushing standard output after writing the prompt to it. Surprisingly, `src/Idris/IDEMode/REPL.idr` already does this correctly, `src/Idris/REPL.idr` does not though.
This commit is contained in:
parent
b207c0c718
commit
c725b11c89
@ -1004,6 +1004,7 @@ mutual
|
||||
= do ns <- getNS
|
||||
opts <- get ROpts
|
||||
coreLift_ (putStr (prompt (evalMode opts) ++ show ns ++ "> "))
|
||||
coreLift_ (fflush stdout)
|
||||
inp <- coreLift getLine
|
||||
end <- coreLift $ fEOF stdin
|
||||
if end
|
||||
|
@ -1,4 +1,5 @@
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 127]
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> [0, 1, 2, 4, 8, 16, 32, 64, 127]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32767]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483647]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32768, 65536, 131072, 262144, 524288, 1048576, 2097152, 4194304, 8388608, 16777216, 33554432, 67108864, 134217728, 268435456, 536870912, 1073741824, 2147483648, 4294967296, 8589934592, 17179869184, 34359738368, 68719476736, 137438953472, 274877906944, 549755813888, 1099511627776, 2199023255552, 4398046511104, 8796093022208, 17592186044416, 35184372088832, 70368744177664, 140737488355328, 281474976710656, 562949953421312, 1125899906842624, 2251799813685248, 4503599627370496, 9007199254740992, 18014398509481984, 36028797018963968, 72057594037927936, 144115188075855872, 288230376151711744, 576460752303423488, 1152921504606846976, 2305843009213693952, 4611686018427387903]
|
||||
@ -58,5 +59,4 @@
|
||||
[0, 8, 16]
|
||||
[0, 16, 32]
|
||||
[0, 32, 64, 33]
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,35 +1,5 @@
|
||||
empty: []
|
||||
one
|
||||
|
||||
two
|
||||
three lines in
|
||||
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
empty: []
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
1/1: Building ReadFilePage (ReadFilePage.idr)
|
||||
Main> Main> Bye for now!
|
||||
empty: []
|
||||
Main> empty: []
|
||||
one
|
||||
|
||||
two
|
||||
@ -58,4 +28,34 @@ three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
Main> empty: []
|
||||
one
|
||||
|
||||
two
|
||||
three lines in
|
||||
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
empty: []
|
||||
one
|
||||
two
|
||||
three lines in
|
||||
four
|
||||
five lines total
|
||||
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
|
||||
1/1: Building Total (Total.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
|
||||
1/1: Building Pythag (Pythag.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
|
||||
Main> Bye for now!
|
||||
|
@ -1,6 +1,6 @@
|
||||
94
|
||||
94
|
||||
188
|
||||
188
|
||||
1/1: Building IORef (IORef.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 94
|
||||
94
|
||||
188
|
||||
188
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
100
|
||||
1/1: Building Buffer (Buffer.idr)
|
||||
Main> 100
|
||||
94
|
||||
94.42
|
||||
"Hello"
|
||||
@ -18,5 +19,4 @@ total size = 20
|
||||
00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 00 ................
|
||||
|
||||
total size = 80
|
||||
1/1: Building Buffer (Buffer.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
(3 ** [2, 4, 6])
|
||||
1/1: Building Filter (Filter.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> (3 ** [2, 4, 6])
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
"Nat"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> "Nat"
|
||||
"List of Nat"
|
||||
"List of Something else"
|
||||
"List of Something else"
|
||||
@ -9,8 +10,7 @@
|
||||
"List of Int"
|
||||
43
|
||||
42
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> Main> Main.strangeId is total
|
||||
Main> Main.strangeId is total
|
||||
Main> Main.strangeId': strangeId' _
|
||||
Main> Bye for now!
|
||||
1/1: Building TypeCase2 (TypeCase2.idr)
|
||||
|
@ -1,5 +1,5 @@
|
||||
"Function from Nat to Nat"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> "Function from Nat to Nat"
|
||||
"Function from Nat to Vector of 0 Int"
|
||||
"Function on Type"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,5 +1,5 @@
|
||||
1
|
||||
1
|
||||
1
|
||||
1/1: Building Nat (Nat.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 1
|
||||
1
|
||||
1
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
42
|
||||
ällo
|
||||
1/1: Building uni (uni.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 42
|
||||
ällo
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
9
|
||||
1/1: Building CB (CB.idr)
|
||||
Main> 9
|
||||
Callback coming
|
||||
In callback
|
||||
24
|
||||
@ -7,5 +8,4 @@ In callback with (1, 2)
|
||||
3
|
||||
9
|
||||
'k'
|
||||
1/1: Building CB (CB.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
5
|
||||
"12"
|
||||
True
|
||||
False
|
||||
1/1: Building bangs (bangs.idr)
|
||||
Main> Just 7
|
||||
Main> Just 7
|
||||
Main> Main> Main> Main> Main> Bye for now!
|
||||
Main> 5
|
||||
Main> "12"
|
||||
Main> True
|
||||
Main> False
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
|
||||
[Just 1, Just 2, Just 3, Just 4, Just 5]
|
||||
1/1: Building array (array.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
|
||||
[Just 1, Just 2, Just 3, Just 4, Just 5]
|
||||
Main> Bye for now!
|
||||
|
@ -1,5 +1,5 @@
|
||||
Made it!
|
||||
1/1: Building Struct (Struct.idr)
|
||||
Main> Made it!
|
||||
(40, 30)
|
||||
"Here": (40, 30)
|
||||
1/1: Building Struct (Struct.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
Received: hello world!
|
||||
Received: echo: hello world!
|
||||
1/1: Building Echo (Echo.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Received: hello world!
|
||||
Received: echo: hello world!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
|
||||
[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
|
||||
1/1: Building Numbers (Numbers.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
|
||||
[8650625671965379659, 5435549321212129090, 8650625671965378905, 365458446121836181, 357]
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
Running Chez program located in folder with spaces
|
||||
1/1: Building Main (Main.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Running Chez program located in folder with spaces
|
||||
Main> Bye for now!
|
||||
|
@ -1,7 +1,7 @@
|
||||
File Exists
|
||||
1/1: Building dir (dir.idr)
|
||||
Main> File Exists
|
||||
False
|
||||
True
|
||||
Just "__PWD__testdir"
|
||||
1/1: Building dir (dir.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
hello
|
||||
|
@ -1,6 +1,6 @@
|
||||
test test
|
||||
1/1: Building File (File.idr)
|
||||
Main> test test
|
||||
unfinished lineabc
|
||||
def
|
||||
File Not Found
|
||||
1/1: Building File (File.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,6 +1,6 @@
|
||||
ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17
|
||||
2
|
||||
ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
1/1: Building partial (partial.idr)
|
||||
Main> Main> Main> Main> Main> Bye for now!
|
||||
Main> ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17
|
||||
Main> 2
|
||||
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
Main> Bye for now!
|
||||
|
@ -1,5 +1,5 @@
|
||||
opened
|
||||
1/1: Building Popen (Popen.idr)
|
||||
Main> opened
|
||||
closed
|
||||
Idris 2
|
||||
1/1: Building Popen (Popen.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,8 @@
|
||||
1
|
||||
1/1: Building Bits (Bits.idr)
|
||||
Main> ["1", "200", "248", "1", "255", "200", "254"]
|
||||
Main> ["True", "False"]
|
||||
Main> ["255", "65535", "4294967295", "18446744073709551615"]
|
||||
Main> 1
|
||||
200
|
||||
True
|
||||
200
|
||||
@ -11,8 +15,4 @@ False
|
||||
65535
|
||||
4294967295
|
||||
18446744073709551615
|
||||
1/1: Building Bits (Bits.idr)
|
||||
Main> ["1", "200", "248", "1", "255", "200", "254"]
|
||||
Main> ["True", "False"]
|
||||
Main> ["255", "65535", "4294967295", "18446744073709551615"]
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,9 +1,9 @@
|
||||
Hello
|
||||
1/1: Building usealloc (usealloc.idr)
|
||||
Main> Hello
|
||||
Hello
|
||||
Done
|
||||
Free X
|
||||
Freeing 0 Hello
|
||||
Free Y
|
||||
Freeing 1 Hello
|
||||
1/1: Building usealloc (usealloc.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,7 +1,7 @@
|
||||
Hello
|
||||
1/1: Building File (File.idr)
|
||||
Main> Hello
|
||||
'I'
|
||||
dris!
|
||||
|
||||
No exceptions occurred
|
||||
1/1: Building File (File.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
True
|
||||
1/1: Building Envy (Envy.idr)
|
||||
Main> True
|
||||
HI
|
||||
True
|
||||
HI
|
||||
@ -6,5 +7,4 @@ True
|
||||
EH
|
||||
True
|
||||
Nothing there
|
||||
1/1: Building Envy (Envy.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
500500
|
||||
1/1: Building runst (runst.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 500500
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
hiya
|
||||
1/1: Building StringParser (StringParser.idr)
|
||||
Main> hiya
|
||||
2
|
||||
Parse failed at position 0: satisfy
|
||||
Parse failed at position 0: Not good
|
||||
@ -13,5 +14,4 @@ False
|
||||
['a', 'b', 'c', 'd']
|
||||
()
|
||||
Parse failed at position 0: Purposefully changed OK to Fail
|
||||
1/1: Building StringParser (StringParser.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,7 +1,7 @@
|
||||
5678
|
||||
1/1: Building ExpressionParser (ExpressionParser.idr)
|
||||
Main> 5678
|
||||
-3
|
||||
262145
|
||||
10
|
||||
7
|
||||
1/1: Building ExpressionParser (ExpressionParser.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
["123", "123", "123", "123", "123"]
|
||||
1/1: Building BitCasts (BitCasts.idr)
|
||||
Main> ["123", "123", "123", "123", "123"]
|
||||
["1234", "1234", "1234", "1234"]
|
||||
["1234567", "1234567", "1234567"]
|
||||
["134", "134", "134", "134"]
|
||||
@ -7,5 +8,4 @@
|
||||
["134", "134"]
|
||||
["134"]
|
||||
["237", "65517", "4294967277", "18446744073709551597"]
|
||||
1/1: Building BitCasts (BitCasts.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
-9223372036854775808
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> -9223372036854775808
|
||||
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 127]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32767]
|
||||
@ -39,5 +40,4 @@
|
||||
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
|
||||
[9223372036854775796, 11, 10, 9, 15, 0]
|
||||
[-9223372036854775798, -11, -12, -9, -15, -2, 9223372036854775797, 10, 11, 9, 0]
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
-9223372036854775808
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> -9223372036854775808
|
||||
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 127]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32767]
|
||||
@ -39,5 +40,4 @@
|
||||
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
|
||||
[9223372036854775796, 11, 10, 9, 15, 0]
|
||||
[-9223372036854775798, -11, -12, -9, -15, -2, 9223372036854775797, 10, 11, 9, 0]
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
MkInUnit 0.25 _
|
||||
MkNewtype 123.456
|
||||
1/1: Building DoubleLit (DoubleLit.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> MkInUnit 0.25 _
|
||||
MkNewtype 123.456
|
||||
Main> Bye for now!
|
||||
|
@ -1,5 +1,5 @@
|
||||
foo
|
||||
foo
|
||||
bar
|
||||
Main> Main> Main> Main> Main> "bar"
|
||||
Main> Main> Bye for now!
|
||||
Main> Main> Main> foo
|
||||
Main> foo
|
||||
Main> "bar"
|
||||
Main> bar
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
[1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
|
||||
1/1: Building Total (Total.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [1, 2, 2, 4, 3, 6, 4, 8, 5, 10]
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
[(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
|
||||
1/1: Building Pythag (Pythag.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [(3, (4, 5)), (6, (8, 10)), (5, (12, 13)), (9, (12, 15)), (8, (15, 17)), (12, (16, 20)), (15, (20, 25)), (7, (24, 25)), (10, (24, 26)), (20, (21, 29)), (18, (24, 30)), (16, (30, 34)), (21, (28, 35)), (12, (35, 37)), (15, (36, 39)), (24, (32, 40)), (9, (40, 41)), (27, (36, 45)), (30, (40, 50)), (14, (48, 50)), (24, (45, 51)), (20, (48, 52)), (28, (45, 53)), (33, (44, 55)), (40, (42, 58)), (36, (48, 60)), (11, (60, 61)), (39, (52, 65)), (33, (56, 65)), (25, (60, 65)), (16, (63, 65)), (32, (60, 68)), (42, (56, 70)), (48, (55, 73)), (24, (70, 74)), (45, (60, 75)), (21, (72, 75)), (30, (72, 78)), (48, (64, 80)), (18, (80, 82)), (51, (68, 85)), (40, (75, 85)), (36, (77, 85)), (13, (84, 85)), (60, (63, 87)), (39, (80, 89)), (54, (72, 90)), (35, (84, 91)), (57, (76, 95)), (65, (72, 97)), (60, (80, 100)), (28, (96, 100)), (20, (99, 101)), (48, (90, 102)), (40, (96, 104)), (63, (84, 105)), (56, (90, 106)), (60, (91, 109)), (66, (88, 110)), (36, (105, 111)), (15, (112, 113)), (69, (92, 115)), (80, (84, 116)), (45, (108, 117)), (56, (105, 119)), (72, (96, 120)), (22, (120, 122)), (27, (120, 123)), (75, (100, 125)), (44, (117, 125)), (35, (120, 125)), (78, (104, 130)), (66, (112, 130)), (50, (120, 130)), (32, (126, 130)), (81, (108, 135)), (64, (120, 136)), (88, (105, 137)), (84, (112, 140)), (55, (132, 143)), (100, (105, 145)), (87, (116, 145)), (24, (143, 145)), (17, (144, 145)), (96, (110, 146)), (48, (140, 148)), (51, (140, 149)), (90, (120, 150)), (42, (144, 150)), (72, (135, 153)), (93, (124, 155)), (60, (144, 156)), (85, (132, 157)), (84, (135, 159)), (96, (128, 160)), (36, (160, 164)), (99, (132, 165)), (119, (120, 169)), (65, (156, 169)), (102, (136, 170)), (80, (150, 170)), (72, (154, 170)), (26, (168, 170)), (52, (165, 173)), (120, (126, 174)), (105, (140, 175)), (49, (168, 175)), (78, (160, 178)), (108, (144, 180)), (19, (180, 181)), (70, (168, 182)), (33, (180, 183)), (111, (148, 185)), (104, (153, 185)), (60, (175, 185)), (57, (176, 185)), (88, (165, 187)), (114, (152, 190)), (95, (168, 193)), (130, (144, 194)), (117, (156, 195)), (99, (168, 195)), (75, (180, 195)), (48, (189, 195)), (28, (195, 197)), (120, (160, 200)), (56, (192, 200))]
|
||||
Main> Bye for now!
|
||||
|
@ -1,6 +1,6 @@
|
||||
94
|
||||
94
|
||||
188
|
||||
188
|
||||
1/1: Building IORef (IORef.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 94
|
||||
94
|
||||
188
|
||||
188
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
100
|
||||
1/1: Building Buffer (Buffer.idr)
|
||||
Main> 100
|
||||
94
|
||||
94.42
|
||||
"Hello"
|
||||
@ -6,5 +7,4 @@
|
||||
65535
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
[0, 94, 0, 0, 0, 65, 65, 65, 65, 0, 123, 20, 174, 71, 225, 154, 87, 64, 0, 0, 72, 101, 108, 108, 111, 32, 116, 104, 101, 114, 101, 33, 255, 255, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
|
||||
1/1: Building Buffer (Buffer.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,3 +1,3 @@
|
||||
(3 ** [2, 4, 6])
|
||||
1/1: Building Filter (Filter.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> (3 ** [2, 4, 6])
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
"Nat"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> "Nat"
|
||||
"List of Nat"
|
||||
"List of Something else"
|
||||
"List of Something else"
|
||||
@ -9,8 +10,7 @@
|
||||
"List of Int"
|
||||
43
|
||||
42
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> Main> Main.strangeId is total
|
||||
Main> Main.strangeId is total
|
||||
Main> Main.strangeId': strangeId' _
|
||||
Main> Bye for now!
|
||||
1/1: Building TypeCase2 (TypeCase2.idr)
|
||||
|
@ -1,5 +1,5 @@
|
||||
"Function from Nat to Nat"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> "Function from Nat to Nat"
|
||||
"Function from Nat to Vector of 0 Int"
|
||||
"Function on Type"
|
||||
1/1: Building TypeCase (TypeCase.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,5 +1,5 @@
|
||||
1
|
||||
1
|
||||
1
|
||||
1/1: Building Nat (Nat.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 1
|
||||
1
|
||||
1
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
42
|
||||
ällo
|
||||
1/1: Building uni (uni.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 42
|
||||
ällo
|
||||
Main> Bye for now!
|
||||
|
@ -1,8 +1,8 @@
|
||||
5
|
||||
"12"
|
||||
True
|
||||
False
|
||||
1/1: Building bangs (bangs.idr)
|
||||
Main> Just 7
|
||||
Main> Just 7
|
||||
Main> Main> Main> Main> Main> Bye for now!
|
||||
Main> 5
|
||||
Main> "12"
|
||||
Main> True
|
||||
Main> False
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
[Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
|
||||
[Just 1, Just 2, Just 3, Just 4, Just 5]
|
||||
1/1: Building array (array.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Just "Hello", Just "World", Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing, Nothing]
|
||||
[Just 1, Just 2, Just 3, Just 4, Just 5]
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,4 @@
|
||||
[3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
|
||||
[8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102]
|
||||
1/1: Building Numbers (Numbers.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> [3518437212345678901234567890560, 1537557061795061679839506167983751, 3518437212345678901234567889686, 8051343735344802977653473432, 339]
|
||||
[8650625671965379659, 5435549321212129090, 8650625671965378905, 22945956689563340, 102]
|
||||
Main> Bye for now!
|
||||
|
@ -1,7 +1,7 @@
|
||||
File Exists
|
||||
1/1: Building dir (dir.idr)
|
||||
Main> File Exists
|
||||
False
|
||||
True
|
||||
Just "__PWD__testdir"
|
||||
1/1: Building dir (dir.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
hello
|
||||
|
@ -1,6 +1,6 @@
|
||||
test test
|
||||
1/1: Building File (File.idr)
|
||||
Main> test test
|
||||
unfinished lineabc
|
||||
def
|
||||
File Not Found
|
||||
1/1: Building File (File.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,6 +1,6 @@
|
||||
ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17
|
||||
2
|
||||
ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
1/1: Building partial (partial.idr)
|
||||
Main> Main> Main> Main> Main> Bye for now!
|
||||
Main> ERROR: Unhandled input for Main.foo at partial.idr:4:1--4:17
|
||||
Main> 2
|
||||
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
Main> ERROR: Unhandled input for Main.lookup' at partial.idr:19:1--19:40
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,8 @@
|
||||
1
|
||||
1/1: Building Bits (Bits.idr)
|
||||
Main> ["1", "200", "248", "1", "255", "200", "254"]
|
||||
Main> ["True", "False"]
|
||||
Main> ["255", "65535", "4294967295", "18446744073709551615"]
|
||||
Main> 1
|
||||
200
|
||||
True
|
||||
200
|
||||
@ -11,8 +15,4 @@ False
|
||||
65535
|
||||
4294967295
|
||||
18446744073709551615
|
||||
1/1: Building Bits (Bits.idr)
|
||||
Main> ["1", "200", "248", "1", "255", "200", "254"]
|
||||
Main> ["True", "False"]
|
||||
Main> ["255", "65535", "4294967295", "18446744073709551615"]
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
["123", "123", "123", "123", "123"]
|
||||
1/1: Building BitCasts (BitCasts.idr)
|
||||
Main> ["123", "123", "123", "123", "123"]
|
||||
["1234", "1234", "1234", "1234"]
|
||||
["1234567", "1234567", "1234567"]
|
||||
["134", "134", "134", "134"]
|
||||
@ -7,5 +8,4 @@
|
||||
["134", "134"]
|
||||
["134"]
|
||||
["237", "65517", "4294967277", "18446744073709551597"]
|
||||
1/1: Building BitCasts (BitCasts.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,7 +1,7 @@
|
||||
ok
|
||||
ok
|
||||
ok
|
||||
ok
|
||||
ok
|
||||
1/1: Building Casts (Casts.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> ok
|
||||
ok
|
||||
ok
|
||||
ok
|
||||
ok
|
||||
Main> Bye for now!
|
||||
|
@ -1,4 +1,5 @@
|
||||
-9223372036854775808
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> -9223372036854775808
|
||||
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 127]
|
||||
[0, 1, 2, 4, 8, 16, 32, 64, 128, 256, 512, 1024, 2048, 4096, 8192, 16384, 32767]
|
||||
@ -39,5 +40,4 @@
|
||||
[340282366920938463463374607431768211444, 11, 10, 9, 15, 0]
|
||||
[9223372036854775796, 11, 10, 9, 15, 0]
|
||||
[-9223372036854775798, -11, -12, -9, -15, -2, 9223372036854775797, 10, 11, 9, 0]
|
||||
1/1: Building BitOps (BitOps.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> Bye for now!
|
||||
|
@ -1,6 +1,6 @@
|
||||
0
|
||||
0
|
||||
0
|
||||
0
|
||||
1/1: Building Fix1037 (Fix1037.idr)
|
||||
Main> Main> Bye for now!
|
||||
Main> 0
|
||||
0
|
||||
0
|
||||
0
|
||||
Main> Bye for now!
|
||||
|
Loading…
Reference in New Issue
Block a user