idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-18 16:51:51 +03:00
Code Issues Projects Releases Wiki Activity
3,723 Commits 6 Branches 9 Tags 114 MiB
91d0eb3e31
Commit Graph

251 Commits

Author SHA1 Message Date
Mathew Polzin
aee1cb94ac
Add a new CHANGELOG_NEXT.md file and update documentation around CHANGELOG entries. (#3180) 2024-01-01 21:08:56 -06:00
Joel Berkeley
ee18555869
Add (++) for List variation of All (#3179) 
* Add `(++)` for `All` for `List`

* changelog

* contributors

* review changes

* update comment

* update comment

* match TODO style

* disambiguate the right one

* further comment changes
 2024-01-01 21:03:13 -06:00
Denis Buzdalov
d5d4b2a9ae [ contrib ] Support options parsing errors in a backward-compatible way 2023-12-30 14:22:51 -06:00
Denis Buzdalov
2f2102c413 [ re #3171 ] Correct mistakenly forgotten to be updated changelog 2023-12-29 17:30:15 -06:00
Denis Buzdalov
3fe95d469a [ interpolate ] Implement Interpolation for primitive numeric types 2023-12-29 11:17:31 -06:00
Denis Buzdalov
db4f65bd8d [ refactor ] Move lazy lists from contrib to base 2023-12-29 09:22:03 -06:00
Thomas E. Hansen
124a31243a [ rc ] 0.7.0-rc1 
An actual, proper release candidate this time.
 2023-12-22 14:44:30 +01:00
Thomas E. Hansen
a3b078cb0d [ rc ] For v0.6.9 - to see if the process was right 
Good luck everybody...

v0.6.9 - Nice!  ^^
 2023-12-22 14:44:30 +01:00
Mathew Polzin
4edd690d0e Update CHANGELOG.md 2023-12-21 13:30:30 -06:00
Denis Buzdalov
da916b68d4 [ fix ] Correctly manage the empty file case while reading a file 2023-12-21 13:30:30 -06:00
André Videla
58e5d15662
Merge pull request #3162 from AdamHarries/compilerEnvs 
[fix] correctly pass environment vars to the RefC compiler
 2023-12-20 06:40:16 -05:00
Denis Buzdalov
b495fe83f0 [ fix ] Support waiting for popen2-created processes 
This fixes problem of creation the garbage of zombie processes on POSIX
systems. This also makes behaviour of `popen2` identical in Windows,
namely, all resources are freed only when waiting, giving at the same
time an ability to observe the exit code afterwards.
 2023-12-19 23:03:31 +03:00
Adam Brouwers-Harries
170e52b3c1 [fix] correctly pass environment vars to the RefC compiler 2023-12-12 21:25:47 +00:00
Denis Buzdalov
eddcbcdc75 [ base ] Add modifyRef into the Ref interface 2023-12-08 18:54:57 +00:00
Steve Dunham
59e00c5210
[ test ] clean_names to make test outputs neater (#3156) 2023-12-08 14:10:37 +00:00
Andor Penzes
82e4fd9da7
Add foldrImplGoLemma to Data.Vect (#2835) 
Co-authored-by: CodingCellist <teh6@st-andrews.ac.uk>
 2023-11-30 10:07:41 +00:00
0xd34df00d
6dd25cd9ec [ base ] Add mapPropertyRelevant, tabulate and (++) for Vect's All 2023-11-30 09:53:05 +00:00
Aleksei Volkov
02ea26e803 [ cli ] option to disable CSE 2023-11-30 09:51:55 +00:00
Denis Buzdalov
2c328a51c0 [ elab ] Support more applicative traversals of TTImp 2023-11-09 22:05:36 +00:00
CodingCellist
d80bc1537d
[ base ] Add bindings for ieee Double number consts (#3116) 2023-11-09 14:01:40 +00:00
PHO
7c87005092
Support "make -j" (#3135) 
* Allow Idris2 to bootstrap with "make -j"

"linear" should explicitly depend on "base" so that "base" is built before
"linear", otherwise it can fail with:

> Error: Module Data.Nat not found
>
> Data.Linear.Copies:5:1--5:16
>  1 | module Data.Linear.Copies
>  2 |
>  3 | import Data.Linear.Bifunctor
>  4 | import Data.Linear.Notation
>  5 | import Data.Nat
>      ^^^^^^^^^^^^^^^

* Allow Idris2 to build with "make -j all"

"all: ${TARGET} libs" is bad because it means "${TARGET}" and "libs" can be
built independently. So "make -j" attempts to build them parallelly and
fail.
 2023-11-08 08:18:02 +00:00
Thomas E. Hansen
db87cef0ad [ doc ] Headings for envvars based on use-time 
Some envvars are only used at build-time, some only at runtime, and lots
are used at both. This clearly cagetorises them accordingly in the docs.
 2023-11-01 09:41:22 +00:00
Denis Buzdalov
5f29b0b9c5 [ elab ] Add an ability to inspect in which function we currently are 2023-10-26 15:42:26 +01:00
Denis Buzdalov
50a579fa18 [ elab ] Implement an operation of returning referred defs of a def 2023-10-26 15:42:26 +01:00
Adowrath
ea093ffaed
[ warning ] for incompatible visibilities on forward decls and definitions. (#3063) 2023-10-25 11:24:43 +01:00
Denis Buzdalov
305604d243
[ base ] Implement a bunch of standard interfaces for Data.These (#3117) 
* [ base ] Implement a bunch of standard interfaces for `Data.These`

* [ base ] Add couple of eliminators with default values for `These`
 2023-10-25 11:15:28 +01:00
Denis Buzdalov
2358a74a29 [ base ] Implement Zippable for several standard types + small cleanup 2023-10-16 22:41:55 +01:00
0xd34df00d
7c8076c149 [ base ] Relevant and irrelevant traversals for Data.Vect.Quantifiers.All 2023-10-16 09:49:22 +01:00
Denis Buzdalov
419a440dad
[ impl ] Support default implicits in named implementations (#3100) 2023-10-13 15:26:42 +01:00
0xd34df00d
f2a95071a1
[ base ] Add Data.Vect.Quantifiers.All.remember, the inverse to forget (#3096) 
Co-authored-by: Guillaume Allais <guillaume.allais@ens-lyon.org>
 2023-10-13 15:26:24 +01:00
Stefan Höck
7fbbb030df
[ new ] add Data.List.grouped function (#3089) 2023-10-13 13:48:15 +01:00
Denis Buzdalov
f7d4b7f4ed [ base ] Add a bridge between MonadState and Ref 2023-10-13 13:47:31 +01:00
Denis Buzdalov
6815aefbe0 [ elab ] Implement file operations, e.g. applicable for type providers 2023-10-13 13:26:46 +01:00
Denis Buzdalov
cbbd0c8caa [ elab ] Make %macro-function be callable without the extension 2023-10-11 13:20:12 +01:00
0xd34df00d
8d5caaa137 [ base ] Add anyToFin converting a Vect's Any to its index 2023-10-09 15:03:55 +01:00
Denis Buzdalov
1256ded110 [ elab ] Implement Ord for Count 2023-10-04 16:31:38 +01:00
Denis Buzdalov
276d41d86c [ new ] Implement Sized for Seqs 2023-10-01 07:16:20 +01:00
Denis Buzdalov
3886200d29 [ fix ] Make traverse and friends lazy for LazyList 2023-09-25 19:51:17 +01:00
Denis Buzdalov
6dc06cd67d [ base ] Add update functions to sorted maps 2023-09-23 22:47:05 +01:00
Steve Dunham
e4fe90e1a3 Merge branch 'main' into foo 2023-09-07 20:19:26 -07:00
Ohad Kammar
d3dc9b7c44
[ refactor ] S-Exp protocols to depend on fewer Idris modules (#3060) 2023-08-31 11:53:14 +01:00
Denis Buzdalov
a4ccb27c83 [ base ] Add lists' infix-by functions, complementary to existing ones 2023-08-28 13:53:59 +01:00
russoul
ebbae42c85 Add uncons' to base; rewrite head' and tail' in terms of uncons' 2023-08-23 11:04:23 +01:00
Janus Troelsen
694b1650c8
[ racket ] Add library loading (#3049) 2023-08-23 11:04:01 +01:00
Jens Petersen
48dbc3251b implement DESTDIR support for distros 
both 'make install' and 'idris2 --install*' should respect DESTDIR now
 2023-08-22 16:44:13 +01:00
Steve Dunham
878187d7f7 [ fix ] Totality checker misses indirect references to partial data 2023-08-12 12:57:28 -07:00
Steve Dunham
badf1e98c8 [ base ] Make foldr1 and foldr1By public 2023-08-07 08:10:35 +01:00
Steve Dunham
bde1a66075
[ fix ] Fix pattern match issue with function application in Refl (#3027) 2023-08-04 13:46:04 +01:00
scarf
c7abb148e8
feat: even and odd for Nat and Integral (#3021) 2023-07-31 08:36:40 +01:00
André Videla
1fa638494d
[ new ] Fixity access modifier (#3011) 2023-07-31 08:35:16 +01:00