idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 15:07:37 +03:00
Code Issues Projects Releases Wiki Activity
1,768 Commits 5 Branches 9 Tags 96 MiB
96cc7fd273
Commit Graph

1768 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Guillaume ALLAIS
96cc7fd273 [ new ] depthFirst, findFile 2021-04-19 10:58:40 +01:00
Jan de Muijnck-Hughes
0c64225521 Report time taken to check totality. 2021-04-19 10:30:36 +01:00
Guillaume ALLAIS
688e5c586c [ test ] Note that we cannot turn the whole check off 
If we were to turn the whole check off instead of just making it
(not incase || isJust (isLHS mode)) then Issue962-case would fail
because `c` would get defaulted to `Integer` and not the `Int` that
is expected.
 2021-04-16 18:12:40 +01:00
Guillaume ALLAIS
f6f2f5f5c6 [ fix #962 ] solve defaults on LHS even in case 2021-04-16 18:12:40 +01:00
Guillaume ALLAIS
9f5cacf31e [ fix ] debugging printing 2021-04-16 18:12:40 +01:00
Jan de Muijnck-Hughes
b68fa077af Added some light formatting to presentation of times for the compiler. 2021-04-16 15:11:16 +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
299a31de5b
Merge pull request #1296 from melted/windows_ci_test 
add tests to Windows CI
 2021-04-12 20:07:17 +02: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
Denis Buzdalov
2287a7ff35 [ refactoring ] Some equivalent changes, mostly code styling nicened 2021-04-12 15:21:33 +01: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
John Mager
c3ff63ae5f Use absolute path to pass around Idris executable 
Rather than tracking how far we are from the project root in the various
Makefile commands, it's much easier to reference the build target with
with an absolute path.
 2021-04-11 20:52:36 +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
Niklas Larsson
f81ccec40a Fix Racket blodwen-arg for real 2021-04-10 11:16:14 +02:00
Niklas Larsson
e117ab1c1c Add back the exe as first arg on Racket 2021-04-09 22:46:32 +02:00
Sören Tempel
c725b11c89 Flush standard out after writing prompt to it 
On Unix-like operating systems stdio.h is usually line-buffered. As
putStr uses fputs(3) from stdio.h internally, output will be written to
standard out after a newline character is written to the buffer. Since
the prompt does not contain a newline, it will only be written to
standard output after the user presses return. I encountered this issue
on Alpine Linux which uses musl libc (instead of glibc). However, I
believe this issue is likely also reproducible with glibc. This commit
fixes this issue by flushing standard output after writing the prompt to
it. Surprisingly, `src/Idris/IDEMode/REPL.idr` already does this
correctly, `src/Idris/REPL.idr` does not though.
 2021-04-09 15:17:00 +01:00
claymager
b207c0c718
Multiple build commands (#1287) 2021-04-09 13:09:24 +01: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
John Mager
c4efa0d29f Ignore some REPL options in package commands 2021-04-07 20:45:18 +01:00
Guillaume ALLAIS
23b67d18ab [ lint ] remove trailing whitespace 2021-04-07 16:33:59 +01:00
Georgi Lyubenov
0bbc3cf42b Update section on custom code gens in updates.rst 
It is now possible to write your own code generation.
 2021-04-07 16:28:46 +01:00
Andor Penzes
b0d6793cfb
[ doc ] Custom backend cookbook (#1237) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-07 16:24:39 +01:00
Denis Buzdalov
533af9dac6 Update readme badges to point to the currently relevant workflows. 2021-04-07 14:46:09 +01:00
Denis Buzdalov
d77c4f1fdf
Ignore the root lib dir (#1278) 2021-04-07 13:55:04 +01:00
Ohad Kammar
b65907f770
Support Multi-declarations (#1280) 2021-04-07 12:21:17 +01:00
Kamiλ Shakirov
2ac4bea220
[ install ] Check if 'realpath' exists for Chez and Racket backends (#1210) 2021-04-06 15:42:04 +01:00
Mathew Polzin
178f26ec17
[ re #1162 ] Test without install (#1240) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-04-05 11:27:56 +01:00
Edwin Brady
7714bdf3fd
Merge pull request #1275 from edwinb/fix1274 
Use correct multiplicity in scope of lets
 2021-04-04 19:17:36 +01:00
Edwin Brady
12f40f538f Use correct multiplicity in scope of lets 
The scope should be checked at the same multiplicity as the enclosing
expression.
 2021-04-04 18:10:34 +01:00
Edwin Brady
add3e08512
Merge pull request #1273 from edwinb/nfthreshold 
Add heuristic for when to normalise metavars
 2021-04-04 17:09:38 +01:00
Edwin Brady
922074b0aa Add heuristic for when to normalise metavars 
If they're big, they take a long time to instantiate, and if they
consist of a lot of functions, chances are that normalising them will
make them much smaller. This significantly improves type checking
performance for some programs with lots of type level computation going
on.

The threshold is set with %nf_metavar_threshold, but the default value
of 50 is probably fine. Set it to 0 to always normalise metavar
solutions, or something higher than 1000 to essentially never do it.
It's roughly a count of nodes in the typechecked syntax tree under the
first function application.
 2021-04-04 15:56:15 +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
Niklas Larsson
2ba7230b19
Merge pull request #1267 from melted/refc_idris_build 
Fix escaping in C backend
 2021-04-03 10:38:33 +02:00
Niklas Larsson
0314ff66ef Fix escaping in C backend 
Use unicode escapes. Insert trailing doublequotes to terminate
(otherwise hexchars will be considered part of escape)
 2021-04-02 22:35:17 +02:00
Niklas Larsson
b2f08c0e81
Merge pull request #1264 from melted/refc_idris_build 
Fixes from trying to compile idris with the refc backend
 2021-04-02 17:04:50 +02:00
Niklas Larsson
e49916cea9 Fixes from trying to compile idris with the refc backend 
* fix doublequoting in constArray
* substitute tildes in names
* Add negate functions
* Add string comparisons

Several things remain, notably missing _argList functions.
 2021-04-02 15:02:40 +02:00
Kamil Shakirov
b27001136b [ tests ] Ignore test artifacts 2021-04-01 10:06:14 +01:00
Guillaume ALLAIS
99b87c8156 [ fix #1248 ] Bring qualified names back for data & record types 2021-03-31 23:17:53 +01:00
Atomotron
a1e7221c32
[ fix #1200 ] Switch scheme backend to flonum functions (#1203) 
Co-authored-by: Guillaume ALLAIS <guillaume.allais@ens-lyon.org>
 2021-03-31 23:17:41 +01:00
Kamil Shakirov
43d0b94567 [ docs ] Update Control.App docs 2021-03-31 18:01:39 +01: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