idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 08:42:11 +03:00
Code Issues Projects Releases Wiki Activity
600 Commits 6 Branches 9 Tags 113 MiB
9ebe6c9cc7
Commit Graph

600 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
a33fc1ec16
Merge pull request #256 from vilunov/repl-package 
"--repl" command for opening a REPL in a package
 2020-06-12 17:50:50 +02:00
Niklas Larsson
232c69de0d
Merge pull request #245 from FrederikVigen/master 
Added fix to recvAll that doesn't use signal (Left 0)
 2020-06-12 17:50:05 +02:00
Tim Süberkrüb
30410eda52 Add fflush to Control.App.FileIO 2020-06-12 17:30:54 +02:00
Tim Süberkrüb
535918a3ac Deduplicate Control.App.FileIO 2020-06-12 17:30:54 +02:00
Tim Süberkrüb
e9a80891b7 Extend Control.App.FileIO 2020-06-12 17:30:54 +02:00
Alex Gryzlov
4fffdec6e8 Merge remote-tracking branch 'upstream/master' 2020-06-12 16:39:37 +02:00
Edwin Brady
6246b8d702
Merge pull request #292 from edwinb/linear-things 
Some small linearity improvements, and linear arrays
 2020-06-12 14:53:34 +01:00
Edwin Brady
84adbe6dc8 Be explicit about multiplicity in Array 
The bootstrap version can't infer it!
 2020-06-12 14:18:57 +01:00
Edwin Brady
c3c556f192 Merge https://github.com/idris-lang/Idris2 into linear-things 2020-06-12 14:16:01 +01:00
Edwin Brady
ec89b97896 Add note to CHANGELOG 2020-06-12 14:12:32 +01:00
Edwin Brady
1c576cb068 Add experimental support for linear arrays 
Backed by Data.IOArray. Also moved the array external primitives to a
separate module Data.IOArray.Prims, since the next step is to add a
linear bounded array type where the bounds checks are done at compile
time, so we'll want to read and write without bounds likes.
 2020-06-12 14:08:00 +01:00
Niklas Larsson
9e4c7c3019
Merge pull request #289 from jfdm/comment-out-unimplemented-proofs-from-data-nat 
Remove unsolved holes from `base`.
 2020-06-12 14:57:12 +02:00
Niklas Larsson
405ebd0095
Merge pull request #287 from jfdm/safe-indexing-of-lists 
Safe indexing of lists
 2020-06-12 14:56:57 +02:00
Edwin Brady
b2c7029b6b Improve inference of linearity in let 
This involves a bit of backtracking in linearity checking, which I'd
prefer to avoid, but it won't hurt in the normal case. If checking a
binder fails due to linearity misuse, try again at linear multiplicity.
 2020-06-12 13:47:15 +01:00
Jan de Muijnck-Hughes
da81146388 Remove unsolved holes from base. 
Having unsolved holes in a 'core' library unneccessarily pollutes the list of holes shown to the user.
Thus, having unfilled holes in a 'core' library is not right.
These constructs can be re-added once the holes have been filled in.
 2020-06-12 13:13:48 +01:00
Jan de Muijnck-Hughes
f7cf2dfb06 Ported safe indexing of Lists from Idris1 prelude. 2020-06-12 13:12:15 +01:00
Niklas Larsson
d86d96f35a
Merge pull request #291 from melted/fix_refl003 
Fix overly nitpicky reflection test
 2020-06-12 13:16:48 +02:00
Niklas Larsson
4b7fbb0371 Fix overly nitpicky reflection test 
See #287
 2020-06-12 12:46:19 +02:00
Edwin Brady
c9b20911e1 Add linear pair/dependent pair to the prelude 
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
 2020-06-12 11:18:12 +01:00
Kamil Shakirov
658953681f Remove hardcoded default 'host' and 'port' parts from command-line help options 2020-06-12 16:12:33 +06:00
Niklas Larsson
49290e44be
Merge pull request #288 from ska80/cmd-default-gc 
Remove hardcoded default CG from command line options
 2020-06-12 12:06:28 +02:00
Kamil Shakirov
4d7e6eef6e Revert TTC changes 2020-06-12 15:36:38 +06:00
Kamil Shakirov
01c79f17d2 Change the TTC version 2020-06-12 15:31:48 +06:00
Kamil Shakirov
90997e9a22 Remove hardcoded default GC from command line options 2020-06-12 15:11:51 +06:00
Alex Gryzlov
cd443f24f6 various stdlib updates 2020-06-11 23:14:11 +02:00
Giuseppe Lomurno
e9d46a2650 Fixed tests 2020-06-11 22:46:36 +02:00
Giuseppe Lomurno
f85800fa76 Show code in errors 2020-06-11 22:46:24 +02:00
Niklas Larsson
7b7415a4e3
Merge pull request #280 from idris-lang/bootstrap_badge 
Add badge for the bootstrap from Idris 1
 2020-06-11 18:54:26 +02:00
Niklas Larsson
e91c33b31c
Add badge for the bootstrap from Idris 1 2020-06-11 18:53:19 +02:00
Niklas Larsson
9906cab7b6
Merge pull request #279 from melted/clean_buffer 
Remove unused functions from idris_buffer.c
 2020-06-11 18:23:15 +02:00
Niklas Larsson
aea0c1fd15 Remove unused functions from idris_buffer.c 2020-06-11 17:35:29 +02:00
Edwin Brady
361d2e4d88
Merge pull request #275 from idris-lang/issue-270 
[ re #270 ] Mention the target type of the auto search
 2020-06-11 16:14:16 +01:00
Edwin Brady
0a985a2815
Merge pull request #278 from edwinb/buffer-prims 
Make buffers more primitive
 2020-06-11 16:03:45 +01:00
Niklas Larsson
0a4667c589
Merge pull request #277 from melted/fix_autocrlf 
Disable autocrlf on WIndows CI
 2020-06-11 16:37:59 +02:00
Niklas Larsson
5858365f18 Disable autocrlf on WIndows CI 2020-06-11 16:25:48 +02:00
Edwin Brady
07ae16123c Only open in binary mode on windows 2020-06-11 14:53:54 +01:00
Jinwoo Lee
5eb86af435 Add some comments about TakeN in chapter 10. 
The `rest` argument must be made explicit. Related to
https://github.com/idris-lang/Idris2/issues/253.
 2020-06-11 14:51:06 +01:00
Edwin Brady
4b1667fdcf Open files in binary mode 
Needed for windows, and harmless on Unix (Idris 1 did it this way).
 2020-06-11 14:35:26 +01:00
Guillaume ALLAIS
43738c172d [ re #270 ] Mention the target type of the auto search 2020-06-11 14:28:34 +01:00
Guillaume ALLAIS
f3c0e89ae8 [ re #238 ] Adding --no-index and --word-diff=color 
Without --no-index, git compares the files with their state in HEAD.
But we want to compare them to each other! This explain why we were
getting no output whatsoever.

With --word-diff=color, we can easily spot the small changes anywhere in
a line.
 2020-06-11 14:23:47 +01:00
Niklas Larsson
7194ad11af
Merge pull request #273 from melted/full_bootstrap 
Add a bootstrap from Idris 1 CI script
 2020-06-11 15:13:57 +02:00
Niklas Larsson
015f195b87
Merge pull request #272 from melted/fix_primitive_bootstrap 
Use 2^64 constant instead of calculation
 2020-06-11 15:13:40 +02:00
Edwin Brady
0a246af449 Make Buffer more primitive 
Meaning that the FFI is aware of it, so you can send arbitrary byte data
to foreign calls. Fixes #209

This means that we no longer need the hacky way of reading and writing
binary data via scheme, so can have a more general interface for reading
and writing buffer data in files.

It will also enable more interesting high level interfaces to binary
data, with C calls being used where necessary.

Note that the Buffer primitive are unsafe! They always have been, of
course... so perhaps (later) they should have 'unsafe' as part of their
name and better high level safe interfaces on top.

This requires updating the scheme to support Buffer as an FFI primitive,
but shouldn't affect Idris2-boot which loads buffers its own way.
 2020-06-11 14:05:52 +01:00
Niklas Larsson
b5f67b94ae Use constants instead of calculation for upper bounds 
Add wrapping to 8-bit adding.

This is a workaround to fix the bootstrap
Fixes #268
 2020-06-11 14:23:41 +02:00
Jan de Muijnck-Hughes
49b4f97c5d Added some modest improvements to code. 2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
ef85348de8 Update src/Text/Literate.idr 
Improve efficiency of lexer for code lines.

Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2020-06-11 12:51:47 +01:00
Jan de Muijnck-Hughes
63e127094e Improved parsing for literate modes. 
The tokenizer for literate modes was incorretly detecting code lines in text.
This PR fixes that, and allows for empty code lines.
 2020-06-11 12:51:47 +01:00
Niklas Larsson
fc322bd699 Add a bootstrap from Idris 1 CI script 2020-06-11 12:20:50 +02:00
Edwin Brady
d71bfef73f
Merge pull request #266 from edwinb/vis-case-with 
Propagate visibility appropriately to case/with
 2020-06-10 13:53:17 +01:00
Edwin Brady
df3449f44b Fix the other clashing test output 
I don't understand the difference here - there's probably a commit I
hadn't merged earlier that affected the name generation.
 2020-06-10 13:08:50 +01:00