ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-10-26 18:02:24 +03:00
Code Issues Projects Releases Wiki Activity
9,488 Commits 4 Branches 42 Tags 40 MiB
61cf812e97
Commit Graph

9488 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Edwin Brady
61cf812e97 Update version number 2018-05-26 17:55:45 +01:00
Edwin Brady
3b35e39eb9 Fix DecEq implementation on primitives 
We can't just make up any old proof for the not equal case, since it
messes up type checking later! Instead, use a postulate, since we won't
do any calculation with it since it produces a Void.
 2018-05-26 17:03:32 +01:00
Jan de Muijnck-Hughes
88f5c717d8
Merge pull request #4443 from mdimjasevic/tutorial-views 
Fixes a few typos in the tutorial on views
 2018-05-17 12:28:58 +01:00
Marko Dimjašević
93695e26e7 Fixes a few typos in the tutorial on views 2018-05-16 21:17:07 +02:00
Niklas Larsson
597411fca2
Merge pull request #4434 from jacereda/strip-dead 
Strip unreachable code/data
 2018-05-05 22:24:09 +02:00
Jorge Acereda
d13fa5cfb3 Strip unreachable code/data 2018-05-01 23:17:54 +02:00
Niklas Larsson
fb1cc4e1ce
Merge pull request #4431 from jacereda/recv-leak 
Leak when receiving from inactive sender
 2018-04-29 21:04:36 +02:00
Jorge Acereda
2247f69ecb Leak when receiving from inactive sender 2018-04-29 10:30:19 +02:00
Niklas Larsson
33d367de25
Merge pull request #4429 from jacereda/master-unboxed-bits8-bits16 
Unboxed Bits8/Bits16 using Int as the underlying representation
 2018-04-28 11:35:30 +02:00
Jorge Acereda
699090ee72 Undo previous commit mess which contained unrelated code from another branch 2018-04-27 23:56:49 +02:00
Niklas Larsson
48e58063e3
Merge pull request #4430 from jacereda/patch-1 
Typo
 2018-04-27 21:03:43 +02:00
jacereda
acce00767c
Update introduction.rst 
s/introduce/introduces
 2018-04-27 18:38:15 +02:00
Ahmad Salim Al-Sibahi
165c2bd0c0
Merge pull request #4424 from jacereda/printer-depth 
Fix printerdepth handling.
 2018-04-27 11:51:37 +02:00
Ahmad Salim Al-Sibahi
a6e06b53ec
Merge pull request #4427 from clayrat/patch-9 
extend Data.Sign
 2018-04-27 11:48:21 +02:00
Jorge Acereda
e9a31f4c0f Unboxed Bits8/Bits16 using Int as the underlying representation 2018-04-26 21:05:50 +02:00
Edwin Brady
fb301a50dd Forget stylish... again... 
(Sorry!)
 2018-04-26 10:35:28 +02:00
Edwin Brady
778bd174a5 Faster dependency chasing 
Caching dependency data rather than recomputing. This is a fairly big
win when systems start to grow, though probably not noticeable for small
systems. Also fixed a bug where the wrong modification time could be
used for a dependency (not sure why this ever worked...)
 2018-04-25 20:15:10 +02:00
Alex Gryzlov
3505a60a17
extend Data.Sign 
Add negation, multiplication and primitive instances for `Signed`.
 2018-04-23 18:08:30 +03:00
Edwin Brady
64084571d3 Reduce work allNamesIn has to do 
This is a major performance hit when functions get big (especially in do
blocks) and a lot of the work it's doing is not actually necessary since
the primary goal is to find shadowed names. So, only search alternatives
if they are genuine alternatives rather than there for name
disambiguation.

Also reduce the reliance on uniplate a little bit, since this causes
some (smaller) performance problems too.
 2018-04-19 15:42:56 +01:00
Jorge Acereda
9fd28ef42c Fix depth handling 2018-04-19 11:22:46 +02:00
Niklas Larsson
d0e06806a2
Merge pull request #4418 from olegv11/erasure_typo 
Fix typo
 2018-04-12 00:29:06 +02:00
Niklas Larsson
86364fa075
Merge pull request #4417 from steshaw/patch-1 
Typo
 2018-04-12 00:28:00 +02:00
olegv11
454fac3df8 Fix typo 2018-04-11 15:33:33 +03:00
Steven Shaw
dfbd38f3f5
Typo 
Fixed "permanently"
 2018-04-11 16:28:59 +10:00
Niklas Larsson
e4d006a53d
Merge pull request #4413 from jacereda/messaging-leak 
getMsg leak
 2018-04-09 00:57:06 +02:00
Niklas Larsson
9d62d28e38
Merge pull request #4412 from joom/master 
Bump to LTS 11.3 and fingertree-0.1.4.1
 2018-04-09 00:51:18 +02:00
Niklas Larsson
c77938fda2
Merge pull request #4414 from jacereda/initial-message-error 
idris_checkInitMessages() didn't check the init bit properly
 2018-04-09 00:50:09 +02:00
Niklas Larsson
10a91889a1
Merge pull request #4411 from jacereda/inbox-error 
Bad size in inbox allocation, analyzer warning
 2018-04-09 00:43:12 +02:00
Jorge Acereda
764df5fd12 idris_checkInitMessages() didn't check the init bit properly 2018-04-08 20:04:33 +02:00
Jorge Acereda
6a14b2aa8a getMsg leak 2018-04-08 20:01:11 +02:00
Joomy Korkut
b8f34d1d9a Bump to LTS 11.3 and fingertree-0.1.4.1 2018-04-07 23:00:42 -04:00
Jorge Acereda
af281ab9d0 Bad size in inbox allocation, analyzer warning 2018-04-07 18:20:31 +02:00
Niklas Larsson
1a7e2ead41
Merge pull request #4409 from OlingCat/master 
Add code-block mark.
 2018-04-05 00:13:54 +02:00
Niklas Larsson
5f5ad04b71
Merge pull request #4410 from melted/update_travis 
Update travis with newer GHC versions
 2018-04-05 00:12:05 +02:00
Niklas Larsson
beeee848b3 Update travis with newer GHC versions 2018-04-04 22:38:41 +02:00
Niklas Larsson
eb8166ba67
Merge pull request #4406 from melted/buf002 
Update test buffer002 to use valid Int values on 32-bit builds
 2018-04-04 00:04:03 +02:00
Oling Cat
be7eb998f8 Add code-block mark. 2018-04-03 21:38:18 +08:00
Jan de Muijnck-Hughes
ffd720aeec
Merge pull request #4408 from OlingCat/master 
Fix some typos and normalize the use of punctuations.
 2018-04-03 10:10:05 +01:00
Oling Cat
ba99edda96 Merge remote-tracking branch 'idris-lang/master' 2018-04-03 14:38:20 +08:00
Oling Cat
ed93603e74 Fix some typos and normalize the use of punctuations. 
Here are some major changes:

tutorial/packages.rst#L25     add code block mark “::”
tutorial/interp.rst#L109      fix wrong comma: \x,\y. should be  \x. \y.
tutorial/interactive.rst#L67  unified as below: parenthesis to comma
tutorial/interactive.rst#L146 fix typo: “non-empty” should be “empty”
tutorial/syntax.rst#L47       add quotations " in `` ``
tutorial/miscellany.rst#L505  fix a weird sentence
st/composing.rst#L66          fix typo: “idrs” should be “idris”
faq/faq.rst#L240              break long command into several lines for clear
faq/faq.rst#L283              remove extra underline at the end of hyperlink form
 2018-04-03 14:31:32 +08: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
Niklas Larsson
4c5c430e42
Merge pull request #4404 from jacereda/master 
Add myself to CONTRIBUTORS
 2018-04-02 19:24:01 +02:00
Jorge Acereda
b8a1382b44 Add myself to CONTRIBUTORS 2018-04-02 19:21:46 +02:00
Niklas Larsson
40a58fe55d
Update CHANGELOG with the closure work. 2018-04-02 19:17:12 +02:00
Niklas Larsson
c2af016e3b
Merge pull request #4385 from jacereda/smaller-closure 
Smaller closure
 2018-04-02 19:14:40 +02:00
Oling Cat
bc018b16b7 Fix some format. 
faq/faq.rst#L240: break long command into several lines for clear
faq/faq.rst#L283: remove extra underline at the end of hyperlinks form
 2018-04-02 12:55:22 +08:00
Jorge Acereda
3d0168fbd9 Remove arity field from Con struct 2018-04-01 15:51:54 +02:00
Jorge Acereda
ad2a7567ac Use hdr.u16 to store arity 2018-04-01 10:57:55 +02:00
Jorge Acereda
8ce876ced3 Remove _null macro 2018-04-01 10:55:46 +02:00
Jorge Acereda
cdeea74633 Align to pointer size 2018-04-01 10:53:31 +02:00