idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-22 11:13:36 +03:00
Code Issues Projects Releases Wiki Activity
2,059 Commits 6 Branches 9 Tags 115 MiB
1875f62248
Commit Graph

2059 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
Niklas Larsson
971104a358
Merge pull request #117 from melted/merge_bootstrap_scripts 
Merge bootstrap for unix and windows
 2020-05-23 15:11:18 +02:00
Niklas Larsson
dbffcce112 Merge bootstrap for unix and windows 2020-05-23 14:51:00 +02:00
Guillaume ALLAIS
9737f863a6 [ typo ] in test coverage007 2020-05-23 13:38:33 +01:00
Edwin Brady
1524b865c0 Remove needless %cg directives 
These now refer to an old library file that is no longer used since the
network library was ported to the new FFI
 2020-05-23 13:06:39 +01:00
Edwin Brady
b263533db4 Merge branch 'ohad-emacs-mode-compatibility' 2020-05-23 12:31:32 +01:00
Edwin Brady
65605d1f93 Remove merge error 2020-05-23 12:31:11 +01:00
Edwin Brady
5b04cc34ae Merge branch 'emacs-mode-compatibility' of https://github.com/ohad/Idris2 into ohad-emacs-mode-compatibility 2020-05-23 12:30:54 +01:00
Edwin Brady
3fa4a9768f Small addition to FAQ on scheme performance 2020-05-23 12:26:05 +01:00
Edwin Brady
0f2236baf3
Merge pull request #115 from melted/actions 
Windows CI
 2020-05-23 12:24:08 +01:00
Edwin Brady
c4b8c90687
Merge pull request #111 from err0r500/minusProofsOnNats 
minus proofs on Nats from Idris1
 2020-05-23 12:23:14 +01:00
Edwin Brady
aeea2b80c9
Merge pull request #109 from ziman/with-disamb 
`with` expressions for name disambiguation
 2020-05-23 12:22:35 +01:00
Edwin Brady
cad0c0e878
Merge branch 'master' into emacs-mode-compatibility 2020-05-23 12:21:03 +01:00
Edwin Brady
7be54ef849
Merge pull request #103 from keram/gambit-blodwen-os 
Define blodwen-os in Gambit support.scm
 2020-05-23 12:18:37 +01:00
Edwin Brady
5cf64499ec
Merge pull request #102 from ziman/101-module-hashes 
Convert to full names before computing hashes
 2020-05-23 12:17:23 +01:00
Niklas Larsson
61ec7757ed
Merge pull request #107 from melted/fix_win_tests 
Fix windows tests
 2020-05-23 13:08:41 +02:00
Edwin Brady
38ad480478 Use name root for generating clauses 
Not the internal name, since that's no use in a program...
Fixes #68
 2020-05-23 12:02:40 +01:00
Edwin Brady
65e3f63598 Make sure literals are normalise on LHS 
The hack (optimisation?) to normalise integer literals when below some
threshold is fine on the RHS, but on the LHS causes problems since we
need them in normal form for pattern matching. Fixes #112
 2020-05-23 11:48:15 +01:00
Niklas Larsson
368fe55515 Add badge 2020-05-23 12:37:51 +02:00
Niklas Larsson
efa7357730 Improve the name of the job 2020-05-23 12:18:42 +02:00
Edwin Brady
eb3cba5f85 Better checking for empty types 
This improves coverage checking, because it can now see that things like
(Z = S x) and (x = S x) are empty. Previously, it only checked that all
possible constructors had a disjoint index. Now, it looks for matches
and checks for disjointness in the matches, which catches a lot more
things especially with equality.
 2020-05-23 11:03:54 +01:00
Niklas Larsson
63e2c2819f Implement Github Actions CI 2020-05-23 11:11:43 +02:00
Niklas Larsson
83b749e4f2 Fix PATH in cmd script 2020-05-23 11:08:25 +02:00
Niklas Larsson
2160d7297c Fix chez014 2020-05-23 11:08:25 +02:00
Niklas Larsson
5d77de178e Escape backslashes when outputting filenames to chez 2020-05-23 11:08:25 +02:00
Niklas Larsson
99f407f1ab Simplify chez017 after changing test runner 2020-05-23 11:08:25 +02:00
Niklas Larsson
755a10056a Be lenient with slashes and backslashes on Windows 2020-05-23 11:08:25 +02:00
Niklas Larsson
59fcf5889c Fix pkg002 on Windows 
allDirs put in a slash at the top level. It should be behind the
drive letter on Windows
 2020-05-23 11:08:25 +02:00
Niklas Larsson
09ea6af22f Fix chez017 for Windows 2020-05-23 11:08:25 +02:00
Niklas Larsson
e30f7ef3ed Fix chez016 on windows 2020-05-23 11:08:25 +02:00
Niklas Larsson
04d6e5ee68 Allow errors when installing cmd file 
It will not be present on a fresh bootstrap yet.
 2020-05-23 11:08:25 +02:00
Niklas Larsson
77df65012c Fix Path ambiguity 2020-05-23 11:08:25 +02:00
Niklas Larsson
2b8f570ae9 Add cmd file to install on windows 2020-05-23 11:08:25 +02:00
Matthieu JACQUOT
f84850ea36 add minus proofs on Nats from Idris1 2020-05-22 22:39:09 +02:00
Edwin Brady
840e020d8c Some FAQ updates 2020-05-22 21:17:37 +01:00
Matus Tejiscak
1de9c54506 Bump ttcVersion. 2020-05-22 21:07:47 +02:00
Matus Tejiscak
394047906d Fix porting errors. 2020-05-22 20:29:56 +02:00
Matus Tejiscak
74dd653fc5 Apply the patch from idris2-boot. 2020-05-22 20:26:10 +02:00
Edwin Brady
38c9633b66 Update generated racket 2020-05-22 18:16:18 +01:00
Edwin Brady
824b661cd5 Update bootstrap scheme 
The library code uses a new feature, and it needs to be able to build
with the bootstrap code (though, fortunately, not with idris2-boot)
 2020-05-22 18:06:04 +01:00
Ohad Kammar
507ace21cc Merge branch 'master' of github.com:idris-lang/Idris2 into emacs-mode-compatibility 2020-05-22 18:06:01 +01:00
Ohad Kammar
ad315343ef Add missing case in IDE/SyntaxHighlighting 2020-05-22 18:05:13 +01:00
Edwin Brady
0958f1fd8b Keep inlining %tcinlines under let 
This fixes a productivity issue with map in the parser library
 2020-05-22 17:52:20 +01:00
Edwin Brady
69ec410890 Add AllGuarded flag for functions 
This is added to functions which are guaranteed to be productive. The
check is currently very conservative - just added when every clause is
constructor headed (or headed by an AllGuarded function), and there are
no other function applications.
 2020-05-22 17:27:18 +01:00
Edwin Brady
a5c2c211a1 Add %tcinline flag to high level syntax 
This allows a function to be inlined for totality checking purposes
only. So, for example, (>>=) might be a function, but if it evaluates to
something constructor guarded in some context, then it might still be
productive.
 2020-05-22 16:01:47 +01:00
Edwin Brady
088bb52f58 Some productivity checker fixes 
Getting there... it still needs to be a bit cleverer at allowing
"obviously productive" functions before we can switch it on though.
 2020-05-22 15:08:42 +01:00
Edwin Brady
b6a3c51129 A bit of shuffling in the CHANGEGLOG 2020-05-22 14:21:48 +01:00
Edwin Brady
6494241c11 Remove some noise from error messages 
There's no point in wrapping all the case blocks, since this is an
internal detail, and it distracts from the proper location of the error.
 2020-05-22 14:19:54 +01:00
Edwin Brady
b27a835e58 Recoverability wasn't quite right 
It needs to take into account that solving other names might cause
unification errors to succeed, so only give up if there's conflicting
concrete constructors
 2020-05-22 14:02:12 +01:00
Edwin Brady
6d946fed7f Evaluate with tcinline under Delay 
If we never evaluate under Delay at all, we won't inline interface
methods, which means productive things defined in an interface can never
be today. So, make sure to set the tcinline flag before quoting the
Delayed closure.
 2020-05-22 13:30:07 +01:00
Edwin Brady
d0af73a295 Abandon delayed operators if unrecoverable 
If we're delaying because of a unification failure, there's no point in
trying again. This can massively speed up (or maybe I should say "unslow
down") error reporting if there's ambiguity because the elaborator won't
be exploring some paths which can never succeed.
 2020-05-22 13:25:08 +01:00