idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Code Issues Projects Releases Wiki Activity
2,951 Commits 6 Branches 9 Tags 115 MiB
4ba651bb8e
Commit Graph

2951 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
teggot
c47b392d08
[ fix #2208 ] Add interactive commands to help message (#2209) 2022-01-25 12:38:49 +00:00
G. Allais
ec5afa5065
[ libs ] move propaganda out of contrib (#2213) 2022-01-25 12:25:55 +00:00
Stefan Höck
f1d56a4e0f
[ syntax ] Namespaced idiom brackets (#2284) 2022-01-24 16:18:36 +00:00
James Cook
e82600c4d6
[ opt ] transform rule making List.length tail-recursive. (#2100) 2022-01-24 16:12:29 +00:00
octeep
f137d96cd6 update refc/buffer to check how many bytes have been read 2022-01-24 15:58:32 +00:00
Mathew Polzin
35a84e505d
[fix #2033] determining when to rebuild modules (#2188) 2022-01-21 10:26:20 +00:00
stefan-hoeck
b50ecb7bc2 [ fix ] add let in JS array conversion 2022-01-21 09:55:34 +00:00
Guillaume Allais
877025d524 [ fix ] properly decorating pragmas / keywords 2022-01-20 17:55:09 +00:00
stefan-hoeck
1b3be25075 [ breaking, totality ] fGetLine should be covering 2022-01-20 17:48:11 +00:00
Jason Dagit
50c5be30d7 RefC: add test for issue1778 2022-01-20 14:10:57 +00:00
Jason Dagit
89aa6e5e6c RefC: Better detection for tail calls in cases 2022-01-20 14:10:57 +00:00
Zoe Stafford
5e42bbfcc9
Merge pull request #2274 from octeep/main 
make readBufferData return the number of bytes that have been read
 2022-01-20 13:11:13 +00:00
Robert Wright
dc25e8f694 Rename RefC extension function stubs 2022-01-20 11:27:30 +00:00
Robert Wright
d85016b64d Add Fin modular arithmetic Num instance 2022-01-20 10:13:20 +00:00
Mathew Polzin
6f405c9e91
[ new ] Add fixities' FC to the syntax info. (#2264) 2022-01-20 10:08:41 +00:00
Mathew Polzin
e7ed760016
[ new ] optional language version field to ipkg files. (#2256) 2022-01-20 10:05:53 +00:00
Stefan Höck
ca5b1ba094
[ totality ] Data.String.words should be total (#2262) 2022-01-20 09:58:50 +00:00
MarcelineVQ
6d10ca09b4 [ base ] add Show for Ordering 2022-01-19 22:12:36 +00:00
octeep
f7bcd1f0b2 make readBufferData return the number of bytes that have been read 2022-01-19 17:35:14 +00:00
Robert Wright
76d1936fad Add Singleton type 2022-01-19 14:22:40 +00:00
Mathew Polzin
4220c644cf
Add a few missing NodeJS FFI functions to System (#2271) 
* support for system command via node backend.

* Add env var set/unset

* fix env unset function

* Update libs/base/System.idr

* modify system test to cover node and chez.

* Add base tests for env get/set
 2022-01-18 22:43:03 -08:00
Guillaume Allais
ffff9bc2e1 [ new ] die 2022-01-18 18:44:36 +00:00
Trevor Arjeski
0d58282087
Update typedd.rst - Exercise 2 of 8.2.5 (#2266) 2022-01-16 23:56:38 -08:00
Edwin Brady
26a47ddafe
Make prim_js2idris_array iterative (#2267) 
I was getting a stack overflow on the tailrec002 test, caused by this
primitive being recursive. I've made it iterative. I'm no JS expert but
I've tested its behaviour against the old version.
 2022-01-16 19:15:26 +00:00
Zoe Stafford
3ef46f639e
Merge pull request #2260 from vincentdehaan/fix-docs 
Minor fix in documentation
 2022-01-11 22:27:06 +00:00
Vincent de Haan
3a38424e69 Minor fix in documentation 2022-01-11 22:36:22 +01:00
Jason Dagit
1d7207fe05
[ fix #2202 ] Use SnocList in parser state to avoid quadratic slowdown (#2203) 
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
 2022-01-11 16:06:19 +00:00
Daniel Kröni
99615c2877 Added the shiftr function clause for Integer. 2022-01-11 09:54:08 +00:00
Zoe Stafford
8e55c32694
Merge pull request #2254 from dunhamsteve/tcbug_test 
[ tests ] Add test case for #2243
 2022-01-08 20:51:52 +00:00
Steven Dunham
e8660cab97 [ tests ] Add test case for #2243 2022-01-07 21:53:46 -08:00
Ellis Kesterton
f93e1c4eac
Change associativity for System.Path operators (#2240) 
Co-authored-by: eayus <erk@st-andrews.ac.uk>
 2022-01-06 18:23:51 +00:00
stefan-hoeck
5ef38dc3c2 [ fix ] mutual tail recursion 2022-01-06 10:45:34 +00:00
Mathew Polzin
1b4811b1ed
[cleanup] Unhide string module (#2230) 
* unhide string lines/unlines functions and clean up a bit.
* skip the extra newline now that unlines adds one at the end.
 2022-01-06 10:34:15 +00:00
Ohad Kammar
ade8034bd1
[ refactor ] More IDE protocol (#2238) 2022-01-06 10:09:29 +00:00
Jan de Muijnck-Hughes
b99d05115b
[ CHANGELOG ] Fix CHANGELOG. (#2251) 
* [ CHANGELOG ] Fix CHANGELOG.

Apparently, the older version of record syntax has now been deprectated.

This was not reflected in the CHANGELOG, and the CHANGELOG entry for an earlier version of Idris2 was erroneously updated to use the new syntax.

THis commit fixes the CHANGELOG.
 2022-01-05 07:51:49 -08:00
Nick Drozd
ec5f40eec7
Injective follow-up (#2155) 2022-01-05 09:40:23 +00:00
Ohad Kammar
079c032036
Fix markdown linting (#2241) 
Fix terminology spelling to adhere to the new super-linter

Co-authored-by: Ohad Kammar <ohad.kammar@ed.ac.uk>
 2022-01-01 11:04:12 +00:00
John Mager
77f4cdeedb [ nix ] fix bitrot 
- `idris2 --version` correctly displays hash again

- `idris2 --install <ipkg>` defaults to $HOME/idris2 instead of a
  literal `~/.idris2`.

- allows building in Nix on latest MacOS
 2021-12-31 09:16:35 -08:00
Ellis Kesterton
f016a81e37
Add 'tryParse' function to 'System.Path' (#2234) 2021-12-30 16:23:45 -08:00
Mathew Polzin
266e06cab7
[cleanup] Small round of unused import culling. (#2231) 
* small round of unused import culling.

* and also the libraries.
 2021-12-29 20:42:29 -08:00
Las Safin
ef8f52fd79 Use chez-racket from mainline Nixpkgs 2021-12-29 18:33:05 -08:00
Attila Lendvai
4a75d71c02 [ ci ] update previous version to v0.5.1, and super-linter to v4.8.5 
The current super-linter v3 line is broken due to a failed backport,
they recommend to use the v4 line:
https://github.com/github/super-linter/issues/2253

Pick a specific version, so that such transient linter bugs won't
camouflage as Idris CI failures.
 2021-12-27 18:04:25 -08:00
Jason Dagit
78ff2059f3 system_info_os001: Add all the OSs that System.Info.os knows about 2021-12-25 21:52:21 -08:00
Jason Dagit
6388c75fe0 idris_system: include sys wait 2021-12-25 21:50:56 -08:00
Denis Buzdalov
7834539240
[ re #238 ] Fix program error condition of git diff call in Golden (#2119) 
* [ fix ] Fix returned status of the `system` function

* [ re #238 ] Fix program error condition of `git diff` call in `Golden`

According to documentation, not only negative exit code means error
 2021-12-22 13:33:37 -08:00
Zoe Stafford
a6efadefbc
Merge pull request #2212 from alissa-tung/main 
[ nodejs ] add pid
 2021-12-22 17:21:12 +00:00
alissa-tung
158cb1c75e [ nodejs ] pid 2021-12-22 22:25:21 +08:00
Ohad Kammar
3c532ea35d
[ refactor ] IDE protocol as a separate module hierarchy (#2171) 2021-12-16 22:09:00 +00:00
Denis Buzdalov
a09c5082c5
[ base ] Use Fin n as index in Bits (#2192) 2021-12-16 18:26:52 +00:00
teggot
d3aed0404c
[ fix #1959 ] use modern record update syntax (#2196) 2021-12-16 18:23:18 +00:00