Commit Graph

1676 Commits

Author SHA1 Message Date
Andy Lok
2ed2f93004
Fix multiline string literals not properly merged (#1158) 2021-03-08 11:28:19 +00:00
Donovan Crichton
8d4e7cc581
List elem extra move/rename (#1165) 2021-03-07 18:00:03 +00:00
Donovan Crichton
06c4daa9bc [ fix ] added Data.Elem.Extra to contrib.ipkg
Added the missing module path in contrib.ipkg.
2021-03-07 11:56:23 +00:00
G. Allais
1d96dd2bd7
[ refactor ] generalise open union machinery (#1157) 2021-03-05 09:28:23 +00:00
Stefan Höck
8d4321eb9a
Add Data.Bits to base (#1033) 2021-03-04 20:59:56 +00:00
Stefan Höck
4c7d0db4bc
[ fix #1148 ] Support hyphenated package names (#1151) 2021-03-04 19:09:15 +00:00
stefan-hoeck
d952741563 [new] instances for SortedMap and Set 2021-03-04 14:54:27 +00:00
Denis Buzdalov
a74d8e6c2d [ doc ] Documentation of package lookup was clarified a bit. 2021-03-04 14:51:57 +00:00
Donovan Crichton
2de2ac2e2c
[ new ] Lemmas: append preserves List membership. (#1152) 2021-03-04 14:50:10 +00:00
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