ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-10-26 09:54:23 +03:00
Code Issues Projects Releases Wiki Activity
10,023 Commits 4 Branches 42 Tags 40 MiB
master
Commit Graph

1235 Commits

Author SHA1 Message Date
Niklas Larsson
9662ab5e4a Disable travis for GHC 8.8 (libffi still broken) 
Update changelog

Use GHC 8.8 in Appveyor

Run legacy test commands
 2020-01-25 18:48:50 +01:00
Niklas Larsson
e79aaaae22 Merge remote-tracking branch 'origin/master' into ghc-8.8 2020-01-25 03:58:36 +01:00
Niklas Larsson
b5a6637da8 Rename expected, input and run 
Because cabal's wildcards are broken and doesn't allow
files without file endings.
 2020-01-25 01:44:54 +01:00
Milan Kral
35757f928a
use HTTPS URL instead of HTTP URL when possible 2019-12-19 14:26:41 +01:00
Alex Gryzlov
ab47462405 test for file existence 2019-07-10 23:01:55 +03:00
Alex Gryzlov
f8c53ebb5c fix executor and test output 2019-07-10 17:25:53 +03:00
Alex Gryzlov
f66e8a961e fix Core.Execute and test 2019-07-10 15:59:25 +03:00
Alex Gryzlov
a803df4810 add expected output for the test 2019-07-10 13:23:42 +03:00
Alex Gryzlov
2405b0b425 add fRemove FFI call 2019-07-10 13:21:29 +03:00
Jan de Muijnck-Hughes
8fe28aa163 Amended the test suite to report updated documentation. 2019-05-15 13:47:41 +01:00
Matus Tejiscak
b09150ea66 Update test010. 2019-04-05 11:38:28 +02:00
Niklas Larsson
609f712d6c Fix appveyor 
By upgrading GHC
 2019-03-02 00:31:15 +01:00
Rui Barreiro
8882622421 fix #4656 2019-02-25 18:43:14 +00:00
Niklas Larsson
6c52e1b902 Only check for Node when required 2018-12-11 21:08:18 +01:00
Niklas Larsson
ce61f6073c
Merge pull request #4539 from zgrannan/improve-with-check 
Raise an error if too many "with" arguments are provided
 2018-12-07 16:13:00 +01:00
Ryan Scott
1a7fa350e0 Add regression test for #2349 (#4584) 2018-11-06 13:32:10 +01:00
Zack Grannan
11c1a23497 Raise an error if too many "with" arguments are provided 
Fixes #4238
 2018-08-19 10:00:09 +08:00
Zack Grannan
ab3985ae96 Handle constant negation in parsing phase 2018-08-12 09:31:27 +08:00
howtonotwin
7b38ac27c2 Merge branch 'master' into feature/vect-isos 2018-07-05 00:34:10 -04:00
howtonotwin
1c0bf464f7 Make Iso a record 
This makes it possible to run an Iso on a value directly without
matching on it.
 2018-07-05 00:33:58 -04:00
Silvan Mosberger
c78d5026fd
Set stdout line buffering before building inputs 2018-06-27 19:55:15 +02:00
Edwin Brady
a08a1e6dd3 Change DecEq primitives to use believe_me 
This at least ensures they won't reduce and mess up type checking
elsewhere. Postulates would be better, but the current erasure analysis
can't necessarily identify that they aren't reachable in a higher order
setting.

Re-fixes #4090
 2018-05-29 11:01:14 +01:00
Niklas Larsson
4bef2ee0d4 Update test buffer002 to use valid Int values on 32-bit builds 
Ints on the C backend contain a tag bit so is limited to one bit less than the
long on the platform.

Fixes #4400
 2018-04-02 20:06:16 +02:00
Jorge Acereda
139ebb724c Use $CC instead of gcc 2018-03-29 19:38:56 +02:00
David Christiansen
9fc97f9b4e Add test from the pull request for Elab.tryCatch 2018-03-18 00:44:17 -07:00
Ahmad Salim Al-Sibahi
0cad6c7507 Fix package test 2018-03-03 17:13:47 +01:00
Ahmad Salim Al-Sibahi
cc7ef9adaf
Remove old eliminator generation and induction tactic (#4351) 
* Remove old eliminator generation and induction tactic

* Run stylize
 2018-02-25 20:26:29 +01:00
martinbaker
fab2841112 fix for odd-even bug in random (#4339) 
* fix for odd-even bug in random

* edit CHANGELOG and remove TODO

* modify tests to conform to new random values

* fix effects003
 2018-02-22 10:37:46 +01:00
yanok
3be1766bd7 Fix looped temporary allocations in mini-GMP (#4324) 
* Bump mini-gmp to the libgmp-6.1 version

* Add a test for #4311.

* Avoid looped temporary allocation in mini-gmp

Backport of https://gmplib.org/repo/gmp/rev/164971d5c8d0

mpn_div_qr_1_preinv function is called in a loop while converting mpz_t to a
string. Looped allocation causes garbage collection while still in mpz_get_str
for big enough numbers, which may cause wrong results or crashes.

Fixes #4311.
 2018-02-19 13:24:27 +01:00
Trevon Sutton
a6037b9143 Fin.restrict fix (#4337) 
* Explicitly pass bounds to `Fin.fromInteger` from `Fin.restrict`
 2018-02-18 16:50:58 +01:00
Ilya Yanok
1d19304dec Add test for REPL reporting abnormal :exec results 
Check if REPL produces an error message if program compiled as a result of
performing ':exec' terminate abnormally.
 2018-02-06 17:56:33 +01:00
Guillaume Allais
377d87ab17 [ fix #4255 ] Not silently accepting invalid options 
squashing various attempts into one commit.

Not using the 'output' file as, looking at various pkg00N,
this does not seem to be needed.

Also moving pkg009 to pkg010 to avoid conflicts with master

Finally, stylize wants some imports moved around
 2018-01-27 08:34:50 +01:00
Ahmad Salim Al-Sibahi
843348e9c6
Merge pull request #4303 from yanok/master 
Small fix for #4282 and #4299
 2018-01-26 07:48:52 +01:00
Ahmad Salim Al-Sibahi
7e876c07d0
Merge pull request #4306 from gallais/module-name 
[ fix #4304 ] Make the Module Name parser explicit
 2018-01-26 07:48:35 +01:00
Guillaume Allais
c80f9fa71e [ fix ] handle empty NS + test case 2018-01-26 00:09:28 +01:00
Edwin Brady
db69077885 Fix binding rules in patterns 
Names should only be implicitly bound in patterns if they begin with a
lower case letter or _ (as in types), and we've always documented this
but never actually enforced it! This has led to some mysterious and
undetected bugs in Idris programs.

This is likely to break some code (sorry) given that I've had to update
a few tests to follow the new rules. However, the code it breaks is code
that shouldn't have worked in the first place!
 2018-01-25 21:09:40 +00:00
Edwin Brady
5205520f2b Add mysteriously missing bits of regression002 
I've no idea...
 2018-01-25 11:34:39 +00:00
Ilya Yanok
a6d701ac5f Add tests for #4282 and #4299 2018-01-24 20:47:04 +01:00
Edwin Brady
c60a22b2c9 Fix tests (buffer002, regression002) 
Writing out the double data depends on the endianness of the machine, so
it might fail surprisingly. All we're really interested in is that it
reads the data back correctly, so display the buffer before setting the
double.
 2018-01-22 13:23:14 +00:00
Edwin Brady
578134cda6 Get and set Double in Data.Buffer 2018-01-22 12:49:05 +00:00
Edwin Brady
6dca7b8a18 Remove pointless logging directives in regression2 2018-01-22 09:30:05 +00:00
Edwin Brady
fc261d6e07 Add missing test file 2018-01-22 09:29:12 +00:00
Edwin Brady
06db7dc171 Fix corner case with dot patterns 
They need to be solvable by unification with another pattern, so it's no
good if the metavariable in the argument position just solves directly
with what the programmer gave.

Fixes #3839
 2018-01-09 16:53:11 +00:00
Melvar Chen
d1fae54cd2
Merge pull request #4260 from Melvar/let-alternatives 
Add alternatives syntax to `let` in `do` blocks
 2018-01-04 23:31:09 +01:00
Edwin Brady
30505c1d1d Merge branch 'master' of github.com:idris-lang/Idris-dev 2017-12-29 20:45:20 +00:00
Edwin Brady
9c8b3d4eb5 Add some buffer primitives 2017-12-29 18:44:01 +00:00
Melvar Chen
b17c6342fe Update the test for let- and bind-alternatives 2017-12-22 07:26:52 +01:00
Jason Felice
117a8ecb54 Merge remote-tracking branch 'upstream/master' into pretty-warnings 2017-12-21 08:33:41 -05:00
Ahmad Salim Al-Sibahi
54049341df
Merge pull request #4226 from XeFias/contrib_ST_File 
First attempt at implementing ST alternative for File.idr in Effects.
 2017-12-14 16:39:20 +01:00
Michael Morgan
b95c90783f fix broken tests caused by mod precedence 
Raising the precedence of `mod` broke a few tests. This commit fixes those tests.
 2017-12-11 16:08:22 -06:00