Edwin Brady
72b68fd813
Merge pull request #1153 from edwinb/delay-localhints
...
Record local hints in delayed elaborators
2021-03-03 15:57:36 +00:00
Edwin Brady
c9de4d9f9f
Remove more trailing whitespace
2021-03-03 14:36:33 +00:00
Edwin Brady
6a29fab245
Remove trailing whitespace in tests
...
Keep the linter happy
2021-03-03 13:55:30 +00:00
Edwin Brady
6887a5f95f
Record local hints in delayed elaborators
...
We might not have set up search problems yet when delaying an
elaborator, so we need to know what the local hints were at the point of
delay.
2021-03-03 13:49:32 +00:00
Edwin Brady
a00fc25109
Merge pull request #1146 from edwinb/fix1140
...
Check current holes only at end of elaboration
2021-03-01 20:51:46 +00:00
Edwin Brady
b782f82667
A bit of tidying
...
`when` is better than if ... else pure ()
2021-03-01 19:55:16 +00:00
Edwin Brady
58fe629d13
Add missing case in ProcessIdr
2021-03-01 19:29:14 +00:00
Edwin Brady
1d965627c9
Check current holes only at end of elaboration
...
Fixes #1140 - when checking holes were solved, we checked all of them,
but there may still be some open if there's a local definition.
2021-03-01 19:11:15 +00:00
Denis Buzdalov
ae43ff688c
[ doc ] Orphaned todo block was removed
2021-03-01 14:50:31 +00:00
Denis Buzdalov
2bb8ff90e2
[contrib] Existing natToFinLTE was reimplemented to have 0 LT argument
2021-03-01 08:31:09 +00:00
G. Allais
cee7e38894
[ new ] Proof search from 'Applications of Applicative Proof Search' ( #1093 )
2021-03-01 08:29:43 +00:00
Denis Buzdalov
7a8c12771b
[ base ] A property of interaction between zipWith and index ( #1128 )
2021-03-01 08:29:17 +00:00
Niklas Larsson
da2ad89252
Merge pull request #910 from cypheon/createdir-permissions
...
Better default permissions for created directories
2021-02-28 17:04:53 +01:00
Edwin Brady
b74e1dc472
Merge pull request #1137 from edwinb/packagepath
...
Add IDRIS2_PACKAGE_PATH environment variable
2021-02-28 15:38:32 +00:00
Edwin Brady
46f994e4c6
Update CHANGELOG
2021-02-28 14:48:37 +00:00
Edwin Brady
03b8198560
Add environment variables to documentation
2021-02-28 14:18:19 +00:00
Edwin Brady
ebbc123b85
Add IDRIS2_PACKAGE_PATH environment variable
...
This tells Idris where to look for packages in addition to the default
places (under $PREFIX and ./depends/). This should allow package
managers a bit more flexibility.
2021-02-28 14:06:10 +00:00
Edwin Brady
5912c1a1df
Merge pull request #1134 from edwinb/versions
...
Version numbers in .ipkg files
2021-02-28 13:45:45 +00:00
Edwin Brady
3a6aa27ba4
Fix package parser error message
...
Thanks to @andylokandy for spotting!
Co-authored-by: Andy Lok <andylokandy@hotmail.com>
2021-02-28 12:56:11 +00:00
Edwin Brady
4726c32d94
Add --ignore-missing-ipkg flag
...
When bootstrapping, we're building things without packages being
available, so we can't expect to find them when looking for
dependencies. So, we find them another way, with an environment
variable. This flag is to tell Idris not to worry about missing
dependencies in this situation.
We also need to update the bootstrapping code, to deal with the new
version number format and new flag in the ipkg files for the libraries.
I think it's still safe to build from the previous version though - lets
see if CI agrees!
2021-02-27 19:39:47 +00:00
Edwin Brady
d617290dd5
Update packaging documentation
2021-02-27 18:20:55 +00:00
Edwin Brady
37cc095f7a
Merge github.com:idris-lang/Idris2 into versions
2021-02-27 18:00:18 +00:00
Edwin Brady
1d8166b1b2
Version number constraints in 'depends' field
...
Now reporting an error if we can't find a package that satisfies the
constraints. The version number field can still be a string (as it used
to be) but will give a deprecation warning - and the old style version
string wasn't used anyway.
Version constraints can have an upper and/or lower bound, which can be
inclusive or not.
2021-02-27 17:58:52 +00:00
Edwin Brady
1052c41a3c
Use version number field in ipkg
...
Packages are now installed in a directory with their version number.
On adding a package directory, we now look in a local 'depends'
directory first (to allow packages to be installed locally to another
project) before the global install directory.
Dependencies can have version bounds (details yet to be implemented) and
we pick the package with the highest version number that matches.
2021-02-27 14:15:19 +00:00
André Videla
aa27ccbdb6
Merge pull request #1097 from andylokandy/multiline
...
Implement multi-line string
2021-02-26 21:50:54 +00:00
Andy Lok
75b41bc8b7
Remove FIXME
...
Signed-off-by: Andy Lok <andylokandy@hotmail.com>
2021-02-27 02:42:42 +08:00
Denis Buzdalov
9b5a773376
Double fixity/priority definition of >> in a single file was removed
2021-02-26 14:20:49 +00:00
Kamil Shakirov
3ec64a7cfc
[docs] Mention external code generators
2021-02-26 13:18:45 +00:00
G. Allais
59de5f1326
[ fix #762 ] Different case tree building strategy ( #1125 )
2021-02-26 09:33:07 +00:00
claymager
33e336ad27
Give App1 implementation of (>>) ( #1122 )
2021-02-25 17:09:24 +00:00
Andy Lok
7630aaea5b
address comment
2021-02-25 22:12:21 +08:00
Z-snails
f334a050b7
Lazy annotations ( #1113 )
2021-02-25 13:44:06 +00:00
Andy Lok
01c5011653
improve error report
2021-02-25 20:14:26 +08:00
Andy Lok
5fed5c2b7a
Merge branch 'master' of https://github.com/idris-lang/Idris2 into multiline
2021-02-25 19:52:42 +08:00
Andy Lok
8c23f5944b
address comment
2021-02-25 18:43:42 +08:00
Jan de Muijnck-Hughes
bf2e15699e
updated protocol with versioning and version changes.
2021-02-25 10:18:47 +00:00
Jan de Muijnck-Hughes
4d36b754c6
initial dump of IDE protocol documentation from Idris1.
2021-02-25 10:18:47 +00:00
G. Allais
fcd834c423
[ fix #110 ] Check the LHS' head is not shadowed ( #1121 )
2021-02-25 08:51:27 +00:00
Guillaume ALLAIS
da88b80481
[ fix #794 ] missing cases in recoverable
2021-02-24 20:25:04 +00:00
Denis Buzdalov
874496e1ae
[base] Constructor's injectivity proofs for Exists and Subset ( #1118 )
...
Co-authored-by: G. Allais <guillaume.allais@ens-lyon.org>
2021-02-24 19:11:41 +00:00
Denis Buzdalov
69be8f2102
[base] bimap functions were added for dependent pairs.
2021-02-24 16:41:33 +00:00
G. Allais
d2eeb7ce86
[ fix #758 ] desugar non-binding sequencing in do blocks to (>>) ( #1095 )
2021-02-24 11:07:16 +00:00
Guillaume ALLAIS
9be15e7e61
[ re #1106 ] Give more details about directory-related failures
2021-02-23 13:52:20 +00:00
Donovan Crichton
06fe9e3152
[ fix #978 ] Mention Editor Plugins in README ( #1111 )
2021-02-23 11:54:26 +00:00
Mark Barbone
0f7fa149c7
Make zip infixr 6
2021-02-23 10:54:28 +00:00
Denis Buzdalov
95af3cf4be
More compose instances and one usage of them ( #1089 )
2021-02-23 10:53:43 +00:00
Guillaume ALLAIS
00067e8151
[ fix #637 ] force indentation after a with
2021-02-23 10:52:22 +00:00
G. Allais
c10c1d65a5
[ fix #1022 ] detect more impossible cases ( #1108 )
2021-02-23 10:51:38 +00:00
Andy Lok
775d7b4bdb
Add test for escaping NL
2021-02-23 13:10:36 +08:00
Andy Lok
626cfa8e19
Add comment
2021-02-23 02:16:31 +08:00
