idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2025-01-04 14:18:26 +03:00
Code Issues Projects Releases Wiki Activity
1,861 Commits 6 Branches 9 Tags 118 MiB
587f73a256
Commit Graph

601 Commits

Author SHA1 Message Date
Edwin Brady
587f73a256 Make documentation from Makefile 
The documentation is now also linked from
https://www.idris-lang.org/pages/documentation.html
and https://www.idris-lang.org/pages/idris-2-documentation.html
 2021-05-01 17:09:25 +01:00
Edwin Brady
ad78f8210a
Merge pull request #903 from cypheon/mkdoc 
WIP: Generate documentation from source code (aka `--mkdoc` support)
 2021-05-01 16:26:19 +01:00
Edwin Brady
d6d68ff09b
Merge pull request #1195 from buzden/some-funs-to-lazy-list 
[ contrib ] Some functions for lazy list + fix for `foldlM`
 2021-05-01 16:18:24 +01:00
Edwin Brady
7f7b11ed54 Use transforms for fastPack/fastUnpack 
We've had these for a while, used for interface specialisation, but
they're not yet used anywhere else or properly documented. We should
document them soon, but for now, it's a useful performance boost to
always use the fast versions of pack/unpack/concat at runtime.

Also moves a couple to the prelude, to ensure that the fast versions are
defined in the same place as the 'normal' version so that the
transformation will always fire (that is, no need to import Data.String
for the transformation to work).
 2021-04-29 23:17:29 +01:00
Johann Rudloff
8d21a292d0 Add Text.PrettyPrint.Prettyprinter.Render.HTML to contrib as well 2021-04-29 13:49:04 +02:00
G. Allais
96a2809f62
[ fix #1169 ] primitive types are not NTCon (#1340) 2021-04-28 09:33:27 +01:00
stefan-hoeck
0858c26dcf [ refactor ] renamed value to runConst 2021-04-25 10:41:36 +01:00
stefan-hoeck
7863636490 [ new ] add Contravariant interface 2021-04-25 10:41:36 +01:00
stefan-hoeck
047fdb50dd [ new ] missing Identity implementations 2021-04-25 10:41:36 +01:00
stefan-hoeck
cb7add2eca [ new ] add Const applicative functor 2021-04-25 10:41:36 +01:00
Guardian Spirit
15bd6823d2
Add identity cast (#1332) 2021-04-25 09:22:01 +01:00
Ruslan Feizerakhmanov
70158b9dd1
REPL commands: load-package & fuzzy-search (#1318) 
REPL commands: load-package & fuzzy-search
Move REPL-related code over to its own namespace
 2021-04-25 09:13:55 +01:00
Johann Rudloff
489b85aae5 PrettyPrint: Fix SimpleDocTree.fromStream dropping parts of documents 
When flattening the `SimpleDocTree` created from a `SimpleDocStream`, the
first part of a concatenated doc was sometimes dropped, depending on the
result of the recursive call to `flatten`.
 2021-04-25 09:10:22 +01:00
Ohad Kammar
9a445f57e6
[base] Minor: change the order of terms in the IntegerView (#1327) 2021-04-23 14:52:44 +01:00
Denis Buzdalov
583442b359
[ contrib ] Arithmetic on Fin (#830) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-23 12:05:13 +01:00
arty
48dc732788
[ base ] Not (a == b) implies not a == b (#1315) 2021-04-22 13:16:26 +01:00
stefan-hoeck
181b26b250 [ fix ] broken unicode parsing in JSON 2021-04-22 10:59:14 +01:00
Tung Alissa
1bf46bc458
[ REPL ] Improving :doc (fixity, totality, colours) (#1316) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-21 09:39:18 +01:00
Guillaume ALLAIS
96cc7fd273 [ new ] depthFirst, findFile 2021-04-19 10:58:40 +01:00
G. Allais
5946442dc2
[ new ] idris2 --init (#1299) 2021-04-15 14:08:50 +01:00
Zoe Stafford
52af4bf3c7
Add missing modules to contrib.ipkg (#1302) 2021-04-14 22:51:00 +01:00
Niklas Larsson
473b8ee740 Windows test fixes 
Translate node error codes
Strip 'b' from flags
Simplify directory wrangling in chez016
 2021-04-12 18:47:57 +02:00
Niklas Larsson
b32a2593ff Node fixes 
Don't assume that errno exists. There might never have been an error.

Quote executable path to handle path with spaces.
 2021-04-12 16:43:54 +02:00
Niklas Larsson
69c29269ed add tests to Windows CI 2021-04-12 15:48:46 +02:00
Raoul Hidalgo Charman
1211f860b6
Fix issues with use of unix sockets (#1284) 
This change adds logic to set up sockaddr correctly for connect and
bind, handles the AF_UNIX case for getSockAddr and expands the existing
test to cover unix sockets.
 2021-04-12 11:22:45 +01:00
Niklas Larsson
bb59efa395
Merge pull request #1269 from melted/fix_arg_prims 
Replace prim__getArgs with prim__getArgsCount and prim__getArg
 2021-04-11 09:40:56 +02:00
G. Allais
b7bdd0a99f
Various improvements (#1286) 2021-04-09 13:02:37 +01:00
Niklas Larsson
9ffc346ebb
Use file extensions when looking for exes on windows (#1268) 
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
 2021-04-08 21:11:34 +01:00
Ruslan Feizerakhmanov
0cef4e3743 Introduce aliases L0 & L1 as specialised versions of L 2021-04-08 21:11:03 +01:00
Ruslan Feizerakhmanov
8d806552b0 Add explicit names in place of underscores 2021-04-08 21:11:03 +01:00
Ruslan Feizerakhmanov
2548f11d52 Make the SM more explicit 2021-04-08 21:11:03 +01:00
Ruslan Feizerakhmanov
1a7dc83ccb Fix a linearity leak in network; expose error codes to the user 2021-04-08 21:11:03 +01:00
Stefan Höck
61c43e5337
[ new ] Add Bifoldable and Bitraversable interfaces to Prelude (#1265) 2021-04-08 17:25:37 +01:00
Guillaume ALLAIS
23b67d18ab [ lint ] remove trailing whitespace 2021-04-07 16:33:59 +01:00
Niklas Larsson
084997a880 Replace prim__getArgs with prim__getArgsCount and prim__getArg 
This spares us from having to build Idris data structures in the foreign
code.
 2021-04-03 10:45:02 +02:00
Guillaume ALLAIS
5af1efb56e [ refactor ] introduce NonZero 
This has a much better behaviour with respect to proof search and
the coverage checker realising we don't need to consider the Z case
than the `Not (x = Z)` we used earlier.
 2021-03-31 17:59:58 +01:00
Guillaume ALLAIS
09d8e25441 [ refactor ] more efficient implementation of range 2021-03-30 10:51:56 +01:00
Ruslan Feizerakhmanov
802113772f Tune precedence of (===), (~=~) and (<+>) 2021-03-29 11:29:58 +01:00
CodingCellist
ec77ad21ab
[ re #1185 ] Add primitive for obtaining number of processors (#1209) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-03-26 18:27:25 +00:00
stefan-hoeck
6824111fd8 [ performance ] add fastUnlines to base 2021-03-26 12:35:29 +00:00
Zoe Stafford
028f82f70c
Add Data.Monoid.Exponentiation to contrib.ipkg (#1232) 2021-03-26 12:35:19 +00:00
Denis Buzdalov
a6a82a18b5 [ prelude ] foldlM was made to be in the Foldable interface. 2021-03-26 00:59:13 +03:00
Denis Buzdalov
9ee0063a7f [ contrib ] Some useful functions were added for lazy lists. 2021-03-26 00:59:13 +03:00
Alex Gryzlov
71abc8e33b
Add Path@contrib & small changes (#1229) 2021-03-25 16:01:32 +00:00
G. Allais
97fb5d7b94
[ fix #893 ] proof gadget for with clauses (#1222) 2021-03-25 10:02:06 +00:00
Denis Buzdalov
0749165245 [ base ] Properties of indexing after replaceAt were added for Vect 2021-03-18 16:07:48 +00:00
Denis Buzdalov
941e3963fa [ base ] DecEq implementations of Fin and Vect were exported publicly 2021-03-18 16:07:21 +00:00
Andy Lok
da92f9d676
Cleanup List1 (#1091) 2021-03-17 14:07:52 +00:00
Guillaume ALLAIS
80f8a0f8fe [ re #1185 ] add threads option to test runner 2021-03-16 14:03:46 +00:00
Denis Buzdalov
c7f510c9de [ fix ] Change one implementation according to recent lib change 2021-03-15 15:18:16 +00:00