idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 10:41:59 +03:00
Code Issues Projects Releases Wiki Activity
2,672 Commits 6 Branches 9 Tags 115 MiB
e8660cab97
Commit Graph

2672 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
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
Ruslan
516cb4a690
Rename lp/loadpackage to package (#2198) 
Also clarifying the doc-string of `:loadpackage`
 2021-12-16 15:58:29 +00:00
Guillaume ALLAIS
6b1c7741e7 [ cleanup ] using whenJust in Driver 
Spotted while reading some unrelated code.
 2021-12-16 15:57:05 +00:00
Guillaume ALLAIS
36918e6186 [ fix ] isImplicit now works for all binders 2021-12-13 20:29:12 +00:00
Balazs Komuves
3463adbc48
[ fix #2032 ] Slow typechecking on Int operation when Data.Fin.fromInteger is in scope (#2189) 2021-12-13 13:47:53 +00:00
octeep
c14ce31db8 Fix compilation on OpenBSD 
Co-authored-by: Johann Rudloff <johann@sinyax.net>

Co-authored-by: Johann Rudloff <johann@sinyax.net>
 2021-12-12 11:42:33 -08:00
Balazs Komuves
6cc20a9974
[ fix #2138] Add an %unhide pragma (#2181) 
* add %unhide pragma

* add a test case

* clean up

* more consistent English usage (+fix some typos)

* add a warning for unhiding not-already-hidden names

* move `unhide` (and `hide`) to the bottom of the source file to avoid having to forward-declare `recordWarning`
 2021-12-11 18:03:36 -08:00
John Mager
9b2811f263 Make RefC search for files in data dirs 
Previously, the RefC files were located in IDRIS2_PREFIX. This is
decoupled to allow users to change the prefix (for ad-hoc library
install locations, for example).
 2021-12-10 14:30:46 +00:00
Balazs Komuves
c3ec522077
[ fix #1404 ] Totality annotation for data type definitions (#2179) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
Co-authored-by: stefan-hoeck <hock@zhaw.ch>
 2021-12-08 16:08:26 +00:00
Kamil Shakirov
ce67a2edd5 [ fix ] Re-add Pretty instances for IntX 2021-12-08 14:58:32 +00:00
Guillaume ALLAIS
dd3df5da98 [ fix ] highlighting 'as' & 'off' keywords 2021-12-07 18:02:59 +00:00
Balazs Komuves
e511bc6884
[ fix #2098 ] Allow unclosed comment blocks (#2173) 2021-12-07 15:46:38 +00:00
Guillaume ALLAIS
6b92fda5bd [ ci ] Add idris2-elab-util to the libs roster 
[ci: libs]
 2021-12-07 15:15:31 +00:00
Guillaume ALLAIS
816240d93e [ cleanup ] lift quoteX patterns to toplevel 2021-12-07 11:00:50 +00:00
Balazs Komuves
5e775aaa41
[ fix #1945 ] Add default support for record fields (#2175) 2021-12-06 21:21:42 +00:00
Balazs Komuves
3f3912e934
[ fix #2065 ] Use postfix projections if prefix ones are off (#2169) 2021-12-06 18:14:13 +00:00
Edwin Brady
e0c916863c
Fix for incremental builds (#2168) 
When we're inlining, since we only have the current module, we might
encounter names we don't have definitions for. In this case, we need to
leave the arity alone, since the module it originates from will have set
it correctly.

This is tricky to test in isolation, and ideally needs something in CI
for a full incremental build (which would have caught the problem!). I
don't have time right now, but let's at least see if this breaks
anything else for now.
 2021-12-04 20:51:59 +00:00
Guillaume ALLAIS
6f3ef813b1 [ refactor ] use a snoclist internally 2021-12-02 12:49:07 +00:00
Guillaume ALLAIS
32140f577f [ fix ] resugaring of snoc lists 2021-12-02 12:49:07 +00:00
Guillaume ALLAIS
5bf88ceedc [ doc ] more documentation for symbols 2021-12-01 13:35:04 +00:00
André Videla
10b9685e4b
Injective interface and its implementations (#2114) 
Co-authored-by: Nick Drozd <nicholasdrozd@gmail.com>
 2021-11-26 10:55:17 +00:00
Denis Buzdalov
f1941cecac [ cleanup ] Remove piece of dead code from prelude 2021-11-26 10:14:47 +00:00
G. Allais
059f74ad0b
[ fix #1861 ] rewrite_impl is linear (#2150) 2021-11-25 17:07:05 +00:00
Guillaume ALLAIS
500df117c1 [ fix #1741 ] Do not replace names in as-patterns 2021-11-25 16:04:44 +00:00
Guillaume ALLAIS
56e599de9c [ re #1987 ] test case 2021-11-25 15:12:54 +00:00
Nick Drozd
9e0676597d Cut relation implicit args 2021-11-25 00:26:57 +00:00
Guillaume ALLAIS
8e8988ff5a [ re #1191 ] test case 2021-11-24 21:15:43 +00:00
Guillaume ALLAIS
662f1eabc5 [ re #215 ] test case 2021-11-24 20:28:07 +00:00
Guillaume ALLAIS
a91fdae426 [ base ] generalise Data.List type signatures 2021-11-24 19:58:35 +00:00
Guillaume ALLAIS
63bf9f2900 [ re #1852 ] Partial fix without the Hole UN refactoring 2021-11-24 10:54:32 +00:00